Distributed Versions of Linear Time Temporal Logic: A Trace Perspective
AbstractLinear time Temporal Logic (LTL) as proposed by Pnueli  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 . Indeed, the verification task can be automated (for instance using the software packages SPIN  and FormalCheck ) to handle large systems of practical interest.
How to Cite
Thiagarajan, P. S., & Henriksen, J. G. (1998). Distributed Versions of Linear Time Temporal Logic: A Trace Perspective. BRICS Report Series, 5(8). https://doi.org/10.7146/brics.v5i8.19280
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.