并发系统性质验证的一种形式化方法* (1999年)

采用Manna和Pnueli提出的命题线性时态逻辑PLTL作为并发系统的形式化规约语言、用PLTL公式描述系统的性质，给出并发系统性质验证的一种模型检验算法。