Distributed Versions of Linear Time Temporal Logic: A Trace Perspective

  • P. S. Thiagarajan
  • Jesper G. Henriksen

Abstract

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.
Published
1998-01-08
How to Cite
Thiagarajan, P., & Henriksen, J. (1998). Distributed Versions of Linear Time Temporal Logic: A Trace Perspective. BRICS Report Series, 5(8). https://doi.org/10.7146/brics.v5i8.19280