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.
Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity
Czech Technical University in Prague（布拉格捷克理工大学）；Technion – Israel Institute of Technology（以色列理工学院）；Charles University, Prague（布拉格查理大学）；University of Warsaw（华沙大学）
LTL Model-Checking for Dynamic Pushdown Networks Communicating via Locks
动态下推网络（Dynamic Pushdown Network，DPN）是一组下推系统（Pushdown Systems，PDS），其中每个进程都可以动态地创建新的PDS实例。DPN是具有（可能是递归的）过程调用和线程创建的多线程程序的自然模型。使用锁扩展DPN允许进程彼此同步。因此，带锁的DPN是一种很好的形式主义，可以对通过锁进行同步的多线程程序进行建模。因此，为带锁的DPN提供模型检验算法是很重要的。在这项工作中，我们认为模型检验的DPN与锁对单索引的LTL属性的形式V fi s. t。fi是在PDS i上解释的LTL公式。我们考虑模型检验问题w.r.t.简单赋值（即，配置是否满足原子命题仅取决于其控制位置和持有的锁）和w.r.t.定期评估（即，满足原子命题的配置集合是配置的规则集合）。我们证明了这些模型检验问题是可判定的。
