The ability to analyze a digital system under conditions of uncertainty is important in several application domains. The problem is naturally described in terms of search in the powerset of the automaton representing the system. However, the associated exponential blow-up prevents the application of traditional model checking techniques. This work describes a new approach to searching powerset automata, which does not require the explicit powerset construction. We present an efficient representation of the search space based on the combination of symbolic and explicit-state model checking techniques. We describe several search algorithms, based on two different, complementary search paradigms, and we experimentally evaluate the approach
Searching Porwerset Automata by Combining Explicit-State and Symbolic Model Checking / Cimatti, Alessandro; Roveri, Marco; Bertoli, Piergiorgio. - 2031:(2001), pp. 313-327. (Intervento presentato al convegno Tools and Algorithms for the Construction and Analysis of Systems [TACAS 2001], Conference Proceedings tenutosi a Genova nel 2-6 Aprile 2001).
Searching Porwerset Automata by Combining Explicit-State and Symbolic Model Checking
Alessandro Cimatti;Marco Roveri;
2001-01-01
Abstract
The ability to analyze a digital system under conditions of uncertainty is important in several application domains. The problem is naturally described in terms of search in the powerset of the automaton representing the system. However, the associated exponential blow-up prevents the application of traditional model checking techniques. This work describes a new approach to searching powerset automata, which does not require the explicit powerset construction. We present an efficient representation of the search space based on the combination of symbolic and explicit-state model checking techniques. We describe several search algorithms, based on two different, complementary search paradigms, and we experimentally evaluate the approachI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione