Name
Abstract | ||
|---|---|---|
Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets. This is a surprising result since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-72734-7_13 | LFCS |
Keywords | Field | DocType |
decidable temporal logic,repeating values,infinitary satisfiability,petri net,freeze operator,temporal property,freeze quantifier,past-time operator,past-time temporal operator,linear-time temporal logic,infinite set,spatio-temporal logic,temporal logic,satisfiability | Computation tree logic,Discrete mathematics,Temporal logic of actions,Interval temporal logic,Computer science,Multimodal logic,Decidability,Linear temporal logic,Finitary,Temporal logic | Conference |
Volume | ISSN | Citations |
4514 | 0302-9743 | 10 |
PageRank | References | Authors |
0.69 | 21 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stéphane Demri | 1 | 832 | 60.65 |
| Deepak D'souza | 2 | 239 | 17.90 |
| Régis Gascon | 3 | 76 | 5.23 |