Symbolic systems,explicit properties: on hybrid approaches for LTL symbolic model checking |
| |
Authors: | Roberto Sebastiani Stefano Tonetta Moshe Y Vardi |
| |
Affiliation: | 1.DISI, Università di Trento,Trento,Italy;2.Embedded Systems Unit,Fondazione Bruno Kessler - IRST,Trento,Italy;3.Dept. of Computer Science,Rice University,Houston,USA |
| |
Abstract: | In this work we study hybrid approaches to LTL symbolic model checking; that is, approaches that use explicit representations of the property automaton,
whose state space is often quite manageable, and symbolic representations of the system, whose state space is typically exceedingly
large. We compare the effects of using, respectively, (i) a purely symbolic representation of the property automaton, (ii)
a symbolic representation, using logarithmic encoding, of explicitly compiled property automaton, and (iii) a partitioning
of the symbolic state space according to an explicitly compiled property automaton. We apply this comparison to three model-checking
algorithms: the doubly-nested fixpoint algorithm of Emerson and Lei, the reduction of emptiness to reachability of Biere et al.,
and the singly-nested fixpoint algorithm of Bloem et al. for weak automata. The emerging picture from our study is quite clear,
hybrid approaches outperform pure symbolic model checking, while partitioning generally performs better than logarithmic encoding.
The conclusion is that the hybrid approaches benefit from state-of-the-art techniques in semantic compilation of LTL properties.
Partitioning gains further from the fact that the image computation is applied to smaller sets of states. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|