Temporal logic with operators for counting modulo n.

A class of extensions of the Linear-time Propositional Temporal Logic (LPTL) is presented. The class of new logics, TL sup n, constitute an infinite hierarchy of logics each of which is more expressive than LPTL. The logic TL sup n is defined in terms of new operators m over U (Until-m), m over G (Forever- m) and O sup m (Next-m), (for any natural number m = n); these introduce the notion of counting modulo m. For example m over Gf is true on a sequence sigma provided f is true on every m-th tail of sigma. Given a TL sup n formula f, we construct a Buchi automation Uf which is a model generator for f. (The language defined by U sub f is precisely the set of models of f.) As in LPTL (identically equal TL sup 1), the time complexity for constructing U sub f, as well as a decision procedure for f, are each one exponent in the size of f.