Manchester Metropolitan University's Research Repository

Linear temporal logic with until and before on integer numbers, deciding algorithms

Rybakov, Vladimir V. (2006) Linear temporal logic with until and before on integer numbers, deciding algorithms. ISSN 1611-3349

Full text not available from this repository.


As specifications and verifications of concurrent systems employ Linear Temporal Logic (LTL), it is increasingly likely that logical consequence in LTL will be used in description of computations and parallel reasoning. We consider the linear temporal logic extending the standard LTL by operations (before) and (previous). Two sorts of problems are studied: (i) satisfiability and (ii) description of logical consequence in via admissible logical consecutions (inference rules). The model checking for LTL is a traditional way of studying such logics. Most popular technique based on automata was developed by M.Vardi (cf. [39, 6]). Our paper uses a reduction of logical consecutions and formulas of LTL to consecutions of a uniform form consisting of formulas of temporal degree 1. Based on technique of Kripke structures, we find necessary and sufficient conditions for a consecution to be not admissible in . This provides an algorithm recognizing consecutions (rules) admissible in by Kripke structures of size linear in the reduced normal forms of the initial consecutions. As an application, this algorithm solves also the satisfiability problem for .

Impact and Reach


Activity Overview

Additional statistics for this dataset are available via IRStats2.


Actions (login required)

View Item View Item