时态逻辑与并发程序

分别阐述了基于Ｍａｎｎａ－Ｐｎｕｅｌｉ框架的命题线性时态逻辑ＰＬＴＬ和基于共享变量方式的并发程序（转换图）模型，并给出该模型与转换系统之间的对应关系；将时态逻辑与公平转移系统ＦＴＳ相结合来描述并发程序及其性质（公平性、安全性及活性）；指出了时态逻辑具备其它形式化方法（ＦＳＭ、Ｐｅｔｒｉ网）所没有的一些优势。

Temporal Logic and Concurrent Program

At first , temporal logic based on Manna Pnueli framework and concurrent program(transition diagrams) model based on shared variable are introduced, and mapping the model into basic transition systems; second,describing concurrent program and their properties(fairness, safety, liveness) by combing temporal logic with FTS model; at last,we point out temporal logic are more suitable than FSM and Petri net for specifies concurrent program.