Publication Details

Abstract Regular Tree Model Checking

BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular Tree Model Checking. In: Proceedings of 7th International Workshop on Verification of Infinite-State Systems -- INFINITY 2005. Aarhus: Basic Research in Computer Science, Computer Science Departments of the Aarlborg and Aarhus Universities, 2005, pp. 15-24. ISSN 0909-3206.
Czech title
Abstraktní regulární model checking nad stromy
Type
conference paper
Language
english
Authors
Bouajjani Ahmed (UPAR7)
Habermehl Peter (UPAR7)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

formal verification, model checking, symbolic verification, regular model checking, the abstrack-check-refine paradigm, finite tree automata

Abstract

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 so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which arise naturally in a lot of modelling and verification contexts. In particular, we first propose abstractions of tree automata based on collapsing their states having an equal language of trees up to some bounded height. Then, we propose an abstraction based on collapsing states having a non-empty intersection (and thus ``satisfying'') the same bottom-up tree ``predicate'' languages. Finally, we show on several examples that the methods we propose give us very encouraging verification results.

Published
2005
Pages
15-24
Journal
BRICS Notes Series, vol. 2005, no. 4, ISSN 0909-3206
Proceedings
Proceedings of 7th International Workshop on Verification of Infinite-State Systems -- INFINITY 2005
Conference
7th International Workshop on Verification of Infinite-State Systems -- INFINITY 2005, San Francisco, California, US
Publisher
Basic Research in Computer Science, Computer Science Departments of the Aarlborg and Aarhus Universities
Place
Aarhus, DK
BibTeX
@INPROCEEDINGS{FITPUB7817,
   author = "Ahmed Bouajjani and Peter Habermehl and Adam Rogalewicz and Tom\'{a}\v{s} Vojnar",
   title = "Abstract Regular Tree Model Checking",
   pages = "15--24",
   booktitle = "Proceedings of 7th International Workshop on Verification of Infinite-State Systems -- INFINITY 2005",
   journal = "BRICS Notes Series",
   volume = 2005,
   number = 4,
   year = 2005,
   location = "Aarhus, DK",
   publisher = "Basic Research in Computer Science, Computer Science Departments of the Aarlborg and Aarhus Universities",
   ISSN = "0909-3206",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7817"
}
Back to top