2010 | OriginalPaper | Buchkapitel
LTL Can Be More Succinct
verfasst von : Kamal Lodaya, A V Sreejith
Erschienen in: Automated Technology for Verification and Analysis
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.