e-space
Manchester Metropolitan University's Research Repository

    Discrete linear temporal logic with current time point clusters, deciding algorithms

    Rybakov, Vladimir V. (2008) Discrete linear temporal logic with current time point clusters, deciding algorithms. Logic and Logical Philosophy, 17 (1-2). pp. 143-161. ISSN 1425-3305

    [img]
    Preview
    Published Version
    Available under License Creative Commons Attribution No Derivatives.

    Download (709kB) | Preview

    Abstract

    The paper studies the logic TL(N2+−wC) – logic of discrete linear time with current time point clusters. Its language uses modalities 3+(possible in future) and 3− (possible in past) and special temporal operations, – 2+w (weakly necessary in future) and 2−w (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(N2+−wC ), so we prove that TL(N2+−wC ) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules in special reduced normal form, and, then, on checking validity of such rules in models of single exponential size in the rules. Also we consider the admissibility problem for TL(N2+−wC ) and show how to reduce the problem for dmissibility to the decidability of TL(N2+−wC ) itself using definable universal modalities.

    Impact and Reach

    Statistics

    Activity Overview
    6 month trend
    5Downloads
    6 month trend
    254Hits

    Additional statistics for this dataset are available via IRStats2.

    Altmetric

    Actions (login required)

    View Item View Item