文件名称：temporal logic of actions
文件大小：485KB
文件格式：PDF
更新时间：2012-03-19 22:53:20
TLA
行文的时序逻辑，LESLIE LAMPORT的经典著作，模型检测的基础理论。 The temporal logic of actions (TLA) is a logic for specifying and reasoning about concurrent systems. Systems and their properties are represented in the same logic, so the assertion that a system meets its specification and the assertion that one system implements another are both expressed by logical implication. TLA is very simple; its syntax and complete formal semantics are summarized in about a page. Yet, TLA is not just a logician’s toy; it is extremely powerful, both in principle and in practice. This report introduces TLA and describes how it is used to specify and verify concurrent algorithms. The use of TLA to specify and reason about open systems will be described elsewhere.