We propose an extension, called L+p , of the temporal logic LTL, which enables talking about finitely many register values: the models are infinite words over tuples of integers (resp. real numbers). The formulas of L+p are flat: on the left of an until, only atomic formulas or LTL formulas are allowed. We prove, in the spirit of the correspondence between automata and temporal logics, that the models of a L+p formula are recognized by a piecewise flat counter machine; for each state q, at most one loop of the machine on q may modify the register values.
Emptiness of (piecewise) flat counter machines is decidable (this follows from a result in [8]). It follows that satisfiability and model-checking the negation of a formula are decidable for L+p . On the other hand, we show that inclusion is undecidable for such languages. This shows that validity and model-checking positive formulas are undecidable.
