Abstract Regular Tree Model Checking

Abstract Regular Tree Model Checking

Peer-reviewed article not indexed in WoS or Scopus

Regular (tree) model checking (RMC)  is a promising generic method for formal verification of infinite-state systems. Itencodes configurations of systems as words or trees over a suitablealphabet, possibly infinite sets of configurations as finite word ortree automata, and operations of the systems being examined as finiteword or tree transducers. The reachability set is then computed by arepeated application of the transducers on the automata representingthe currently known set of reachable configurations. In order tofacilitate termination of RMC, various acceleration schemas have beenproposed. One of them is a combination of RMC with theabstract-check-refine paradigm yielding the so-called abstract regularmodel checking (ARMC). ARMC has originally been proposed for wordautomata and transducers only and thus for dealing with systems withlinear (or easily linearisable) structure. In this paper, we propose ageneralisation of ARMC to the case of dealing with trees which arisenaturally in a lot of modelling and verification contexts. In particular, we first proposeabstractions of tree automata based on collapsing their states havingan equal language of trees up to some bounded height. Then, we proposean 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 giveus very encouraging verification results.

Regular (tree) model checking (RMC)  is a promising generic method for formal verification of infinite-state systems. Itencodes configurations of systems as words or trees over a suitablealphabet, possibly infinite sets of configurations as finite word ortree automata, and operations of the systems being examined as finiteword or tree transducers. The reachability set is then computed by arepeated application of the transducers on the automata representingthe currently known set of reachable configurations. In order tofacilitate termination of RMC, various acceleration schemas have beenproposed. One of them is a combination of RMC with theabstract-check-refine paradigm yielding the so-called abstract regularmodel checking (ARMC). ARMC has originally been proposed for wordautomata and transducers only and thus for dealing with systems withlinear (or easily linearisable) structure. In this paper, we propose ageneralisation of ARMC to the case of dealing with trees which arisenaturally in a lot of modelling and verification contexts. In particular, we first proposeabstractions of tree automata based on collapsing their states havingan equal language of trees up to some bounded height. Then, we proposean 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 giveus very encouraging verification results.

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

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

BOUAJJANI, A.; HABERMEHL, P.; ROGALEWICZ, A.; VOJNAR, T.

03.02.2006

Elsevier Science

Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY 2005)

1571-0661

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

149

1

United States of America

37

48

12

http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B75H1-4J3Y06T-4-1&_cdi=13109&_user=640830&_orig=browse&_coverDate=02%2F03%2F2006&_sk=998509998&view=c&wchp=dGLbVlz-zSkWA&md5=8e10fd6367f1b94bb331d35d09b3ae26&ie=/sdarticle.pdf