Name
Abstract | ||
|---|---|---|
In this work, the notion of provability for first order linear temporal logic over finite time structures, FO-LTLfin, is studied. We show that the validity problem for such a logic is not recursively enumerable, hence FO-LTLfin 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 them 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 prepositional 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 constrsiints", i.e. linear inequalities on time points. Branch closure is reduced to unsatisfiability over the integers of the set of temporal constreiints in the branch. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-48242-3_5 | LPAR |
Keywords | Field | DocType |
first order linear temporal,temporal interval,finite time structure,temporal constrsiints,temporal constreiints,order linear temporal logic,finite time structures,underlying time frame,time point,temporal model,denoting time point,bound k,first order,linear temporal logic | Integer,Discrete mathematics,Interval temporal logic,Recursively enumerable language,Algorithm,Linear temporal logic,Temporal logic,Linear inequality,Recursion,Mathematics,Bounded function | Conference |
ISBN | Citations | PageRank |
3-540-66492-0 | 19 | 1.09 |
References | Authors | |
15 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Serenella Cerrito | 1 | 139 | 13.72 |
| Marta Cialdea Mayer | 2 | 274 | 28.25 |
| Sébastien Praud | 3 | 19 | 1.43 |