论文部分内容阅读
PSL（property specification language）是一种用于描述并行系统的属性规约语言，包括线性时序逻辑FL（foundation language）和分支时序逻辑OBE（optional branching extension）两部分．由于OBE就是CTL（computation tree logic），并且具有时钟声明的公式很容易改写成非时钟公式，因此重点研究了非时钟FL逻辑．为便于进行模型检验，每个FL公式必须转化成为一种可验证形式，通常是自动机（非确定自动机）．构造非确定自动