e-space
Manchester Metropolitan University's Research Repository

    Decidability w.r.t. logical consecutions of linear temporal logic extended by since and previous

    Rybakov, Vladimir V. (2007) Decidability w.r.t. logical consecutions of linear temporal logic extended by since and previous. Fundamenta Informaticae, 81 (1-3). pp. 297-313. ISSN 1875-8681

    File not available for download.

    Abstract

    This paper aims to prove that the linear temporal logic LTLu,sn, n-1(N) , which is an extension of the standard linear temporal logic LTL by operations Since and Previous (LTL itself, as standard, uses only Until and Next) and is based on the frame of all natural numbers N, as generating Kripke/Hintikka structure, is decidable w.r.t. admissible consecutions (inference rules). We find an algorithm recognizing consecutions admissible in LTLu,sn, n-1(N) . As a consequence this algorithm solves satisfiability problem and shows that LTLu,sn, n-1(N) itself is decidable, despite LTLu,sn, n-1(N) does not have the finite model property.

    Impact and Reach

    Statistics

    Activity Overview
    6 month trend
    0Downloads
    6 month trend
    274Hits

    Additional statistics for this dataset are available via IRStats2.

    Repository staff only

    Edit record Edit record