LTL Can Be More Succinct

It is well known that modelchecking and satisfiability of Linear Temporal Logic (LTL) are

Pspace

-complete. Wolper showed that with grammar operators, this result can be extended to increase the expressiveness of the logic to all regular languages. Other ways of extending the expressiveness of LTL using modular and group modalities have been explored by Baziramwabo, McKenzie and Thérien, which are expressively complete for regular languages recognized by solvable monoids and for all regular languages, respectively. In all the papers mentioned, the numeric constants used in the modalities are in unary notation. We show that in some cases (such as the modular and symmetric group modalities and for threshold counting) we can use numeric constants in binary notation, and still maintain the

Pspace

upper bound. Adding modulo counting to LTL[F] (with just the unary future modality) already makes the logic

Pspace

-hard. We also consider a restricted logic which allows only the modulo counting of length from the beginning of the word. Its satisfiability is

$\Sigma^P_3$

-complete.