A Decidable Temporal Logic of Repeating Values

14 years 5 months ago

Download www.lsv.ens-cachan.fr

Various logical formalisms with the freeze quantiﬁer 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 inﬁnite 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 ﬁnitary and inﬁnitary satisﬁability by reduction into the veriﬁcation 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 quantiﬁer.

Stéphane Demri, Deepak D'Souza, Régi

Real-time Traffic