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. ISSN 1425-3305

Full text not available from this repository.

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

Downloads
Activity Overview
0Downloads
197Hits

Additional statistics for this dataset are available via IRStats2.

Actions (login required)

View Item View Item