Distributed Versions of Linear Time Temporal Logic: A Trace Perspective

P. S. Thiagarajan, Jesper G. Henriksen


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.

Full Text:


DOI: http://dx.doi.org/10.7146/brics.v5i8.19280
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library