Computer Science – Logic in Computer Science
Scientific paper
2009-10-26
Computer Science
Logic in Computer Science
Conference submission
Scientific paper
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 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(Fs,Gs) 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.
Libkin Leonid
To Anthony Widjaja
No associations
LandOfFree
Algorithmic metatheorems for decidable LTL model checking over infinite systems does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Algorithmic metatheorems for decidable LTL model checking over infinite systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Algorithmic metatheorems for decidable LTL model checking over infinite systems will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-563443