Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Algorithmic metatheorems for decidable LTL model checking over infinite systems
Authors: Anthony Lin ; Leonid Libkin
Date:Oct 2009
Publication Type:Conference Paper Publication Status:Submitted
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(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.
Links To Paper
Bibtex format
author = { Anthony Lin and Leonid Libkin },
title = {Algorithmic metatheorems for decidable LTL model checking over infinite systems},
book title = {},
year = 2009,
month = {Oct},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh