Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems

Anthony Widjaja To, Leonid Libkin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

By algorithmic metatheorems for a model checking problem P over infinite-state systems we mean generic results that can be used to infer decidability (possibly complexity) of P not only over a specific class of infinite systems, but over a large family of classes of infinite systems. Such results normally start with a powerful formalism F of infinite-state systems, over which P is undecidable, and assert decidability when is restricted by means of an extra "semantic condition" C. We prove various algorithmic metatheorems for the problems of model checking LTL and its two common fragments LTL(F-s, G(s)) and LTLdet over the expressive class of word/tree automatic transition systems, which are generated by synchronized finite-state transducers operating on finite words and trees. We present numerous applications, where we derive (in a unified manner) many known and previously unknown decidability and complexity results of model checking LTL and its fragments over specific classes of infinite-state systems including pushdown systems; prefix-recognizable systems; reversal-bounded counter systems with discrete clocks and a free counter; concurrent pushdown systems with a bounded number of context-switches; various subclasses of Petri nets; weakly extended PA-processes; and weakly extended ground-tree rewrite systems. In all cases, we are able to derive optimal (or near optimal) complexity. Finally, we pinpoint the exact locations in the arithmetic and analytic hierarchies of the problem of checking a relevant semantic condition and the LTL model checking problems over all word/tree automatic systems.

Original languageEnglish
Title of host publicationFOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS
EditorsL Ong
Place of PublicationBERLIN
PublisherSpringer-Verlag GmbH
Pages221-236
Number of pages16
ISBN (Print)978-3-642-12031-2
Publication statusPublished - 2010
Event13th International Conference on Foundations of Software Science and Computational Structures/Joint European Conferences on Theory and Practice of Software - Paphos
Duration: 20 Mar 201028 Mar 2010

Conference

Conference13th International Conference on Foundations of Software Science and Computational Structures/Joint European Conferences on Theory and Practice of Software
CityPaphos
Period20/03/1028/03/10

Cite this