Open AccessDistributed Versions of Linear Time Temporal Logic: A Trace Perspective
Author(s) -
P. S. Thiagarajan,
Jesper G. Henriksen
Publication year - 1998
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v5i8.19280
Subject(s) - linear temporal logic , trace (psycholinguistics) , computation , computer science , temporal logic , sequence (biology) , state (computer science) , feature (linguistics) , linear logic , theoretical computer science , programming language , algorithm , task (project management) , linguistics , philosophy , biology , genetics , management , economics
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.