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. In: First International Symposium on Computer Science in Russia (CSR 2006), 8th June 2006 - 12th June 2006, St. Petersburg, Russia.

    File not available for download.


    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
    6 month trend
    6 month trend

    Additional statistics for this dataset are available via IRStats2.


    Actions (login required)

    View Item View Item