文章基本信息

标题：Distributed Versions of Linear Time Temporal Logic: A Trace Perspective
本地全文：下载
作者：P. S. Thiagarajan ; Jesper G. Henriksen
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1998
卷号：5
期号：8
出版社：Aarhus University
摘要：Linear time Temporal Logic (LTL) as proposed by Pnueli [37] has become a well established tool for specifying the dynamic behaviour of distributed systems. A basic feature of LTL is that its formulas are interpreted over sequences. Typically, such a sequence will model a computation of a system; a sequence of states visited by the system or a sequence of actions executed by the system during the course of the computation. A system is said to satisfy a specification expressed as an LTL formula in case every computation of the system is a model of the formula. A rich theory of LTL is now available using which one can effectively verify whether a nite state system meets its specification [51]. Indeed, the verification task can be automated (for instance using the software packages SPIN [21] and FormalCheck [2]) to handle large systems of practical interest.