Decision problems over infinite graphs : higher order pushdown systems and synchronized products
Stefan Wöhrle, Wolfgang H Thomas · RWTH Publications (RWTH Aachen) · 2005
The extension of formal verification methods to infinite models requires classes of graphs which are finitely representable and for which the model checking problem is decidable. We consider three approaches to define classes of finitely representable graphs: internal representations as configuration graphs of higher-order pushdown systems, transformational representations by application of operations which preserve the decidability of the model checking problem, and by composition from components using synchronized products. In the first part of the thesis we show that the hierarchy of higher-order pushdown graphs coincides with the Caucal hierarchy of graphs. We thus obtain transformational representations of higher-order pushdown graphs and can conclude that they enjoy a decidable monadic second-order theory. In the second part of the thesis investigate synchronized products of finitely representable infinite graphs and show that the decidability of an extension of first-order logic with reachability predicates is preserved under the formation of finitely synchronized products. This result is complemented by undecidability results for extensions of the admissible product operations as well as the expressive power of the logic under consideration.