×

Algorithmic improvements in regular model checking. (English) Zbl 1278.68150

Hunt, Warren A.jun. (ed.) et al., Computer aided verification. 15th international conference, CAV 2003, Boulder, CO, USA, July 8–12, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40524-0/pbk). Lect. Notes Comput. Sci. 2725, 236-248 (2003).
Summary: Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems, whose states can be represented as finite strings of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. In earlier papers, we have developed methods for computing the transitive closure (or the set of reachable states) of the transition relation, represented by a regular length-preserving transducer. In this paper, we present several improvements of these techniques, which reduce the size of intermediate approximations of the transitive closure: One improvement is to pre-process the transducer by bi-determinization, another is to use a more powerful equivalence relation for identifying histories (columns) of states in the transitive closure. We also present a simplified theoretical framework for showing soundness of the optimization, which is based on commuting simulations. The techniques have been implemented, and we report the speedups obtained from the respective optimizations.
For the entire collection see [Zbl 1027.00031].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
PDFBibTeX XMLCite
Full Text: DOI