In this work, the notion of provability for first order linear temporal logic over finite time structures, FO-LTL fin, is studied. We show that the validity problem for such a logic is not recursively enumerable, hence FO-LTL fin is not recursively axiomatizable. This negative result however does not hold in the case of bounded validity, that is truth in all temporal models where the object domain is possibly infinite, but the underlying sequence of time points does not exceed a given size. A formula is defined to be k-valid if it is true in all temporal models whose underlying time frame is not greater than k, where k is any fixed positive integer. In this work a tableau calculus is defined, that is sound and complete with respect to k-validity, when given as input the initial formula and the bound k on the size of the temporal models. The main feature of the system, extending the propositional calculus defined in [7], is that of explicitly denoting time points and having tableau nodes labelled by either expressions intuitively stating that a formula holds in a given temporal interval, or “temporal constraints”, i.e. linear inequalities on time points. Branch closure is reduced to unsatisfiability over the integers of the set of temporal constraints in the branch.

Cerrito, S., Cialdea, M., Praud, S. (1999). First Order Linear Temporal Logic over Finite Time Structures. In Logic for Programming and Automated Reasoning (pp.62-76). Berlin Heidelberg : Springer [10.1007/3-540-48242-3_5].

First Order Linear Temporal Logic over Finite Time Structures

CIALDEA, Marta;
1999-01-01

Abstract

In this work, the notion of provability for first order linear temporal logic over finite time structures, FO-LTL fin, is studied. We show that the validity problem for such a logic is not recursively enumerable, hence FO-LTL fin is not recursively axiomatizable. This negative result however does not hold in the case of bounded validity, that is truth in all temporal models where the object domain is possibly infinite, but the underlying sequence of time points does not exceed a given size. A formula is defined to be k-valid if it is true in all temporal models whose underlying time frame is not greater than k, where k is any fixed positive integer. In this work a tableau calculus is defined, that is sound and complete with respect to k-validity, when given as input the initial formula and the bound k on the size of the temporal models. The main feature of the system, extending the propositional calculus defined in [7], is that of explicitly denoting time points and having tableau nodes labelled by either expressions intuitively stating that a formula holds in a given temporal interval, or “temporal constraints”, i.e. linear inequalities on time points. Branch closure is reduced to unsatisfiability over the integers of the set of temporal constraints in the branch.
1999
978-3-540-66492-5
Cerrito, S., Cialdea, M., Praud, S. (1999). First Order Linear Temporal Logic over Finite Time Structures. In Logic for Programming and Automated Reasoning (pp.62-76). Berlin Heidelberg : Springer [10.1007/3-540-48242-3_5].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11590/181576
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 26
  • ???jsp.display-item.citation.isi??? ND
social impact