Sciweavers

Share
CAV
2005
Springer

Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking

9 years 6 months ago
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking
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...
Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vard
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CAV
Authors Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
Comments (0)
books