论文部分内容阅读
分别阐述了基于Manna-Pnueli框架的命题线性时态逻辑PLTL和基于共享变量方式的并发程序(转换图)模型,并给出该模型与转换系统之间的对应关系;将时态逻辑与公平转移系统FTS相结合来描述并发程序及其性质(公平性、安全性及活性);指出了时态逻辑具备其它形式化方法(FSM、Petri网)所没有的一些优势。