Abstract Regular Model Checking

Regular Tree Model Checking Ahmed Bouajjani, Peter Habermehl 1 LIAFA, University Paris 7, Case 7014, 2, place Jussieu, F-75251 Paris Cedex 05, France Adam Rogalewicz, Tom´aˇs Vojnar 2 FIT, Brno University of Technology, Boˇzetˇechova 2, CZ-61266, Brno, Czech Republic Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the sobstract regular m...

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar
• Keywords: CAV 2004, Formal Methods, Model Checking, Regular Tree Model, Tree Automata