×

Monadic logic of order over naturals has no finite base. (English) Zbl 1056.03007

Temporal Logic (TL), originally proposed by A. Pnueli, is a convenient framework for specifying properties of reactive systems. Properties are described by formulas built from atoms using Boolean connectives and modalities (temporal connectives). The semantics of TL is usually expressed in terms of formulas of the Monadic Logic of Order (MLO). Therefore, different temporal logics appear to be a convenient way to use fragments of MLO. For instance, Kamp’s theorem states that the temporal logic having ‘Until’ and ‘Since’ as only temporal modalities is expressively complete for the first-order fragment of MLO.
The paper addresses the question whether there exists a temporal logic with a finite number of temporal modalities which is expressively equivalent to MLO, and provides a negative answer to the question. In particular, the authors consider a property Mult-\(p(X)\) which holds true at a point iff there exists only one point in the future (with respect to the considered point) where \(X\) holds true, and this point is placed (in the future) at a distance which is a multiple of \(p\) plus one. The negative result is proved by showing that for any temporal logic with a finite number of temporal modalities there is a natural \(p\) such that Mult-\(p(X)\) cannot be expressed in such a temporal logic. The proof exploits two pumping lemmas based on standard automata theory techniques.

MSC:

03B44 Temporal logic
03B70 Logic in computer science
PDFBibTeX XMLCite
Full Text: DOI Link