×

Regular tree model checking. (English) Zbl 1010.68087

Brinksma, Ed (ed.) et al., Computer aided verification. 14th international conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2404, 555-568 (2002).
Summary: In this paper, we present an approach for algorithmic verification of infinite-state systems with a parameterized tree topology. Our work is a generalization of regular model checking, where we extend the work done with strings toward trees. States are represented by trees over a finite alphabet, and transition relations by regular, structure preserving relations on trees. We use an automata theoretic method to compute the transitive closure of such a transition relation. Although the method is incomplete, we present sufficient conditions to ensure termination.
We have implemented a prototype for our algorithm and show the result of its application on a number of examples.
For the entire collection see [Zbl 0993.00049].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata

Citations:

Zbl 0993.00049
PDFBibTeX XMLCite
Full Text: Link