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 approach.
Chapter PDF
Similar content being viewed by others
Keywords
References
B. Bonet and H. Geffner. Planning with Incomplete Information as Heuristic Search in Belief Space. In S. Chien, S. Kambhampati, and C.A. Knoblock, editors, 5th International Conference on Artificial Intelligence Planning and Scheduling, pages 52–61. AAAI-Press, April 2000.
T. L. Booth. Sequential Machines and Automata Theory. J. Wiley, 1967.
R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
G. Cabodi, P. Camurati, and S. Quer. Improving symbolic traversals by means of activity profiles. In Proceedings of the 31st Conference on Design Automation, pages 306–311, New York, NY, USA, June 21–25 1999. ACM Pres.
A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer (STTT), 2(4), March 2000.
A. Cimatti and M. Roveri. Conformant Planning via Symbolic Model Checking. Journal of Artificial Intelligence Research (JAIR), 13:305–338, 2000.
F. Brglez, D. Bryan, and K. Kozminski. Combinational profiles of sequential benchmark circuits. In International Symposium on Circuits and Systems, May 1989.
G.J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
Zvi Kohavi. Switching and Finite Automata Theory. McGraw-Hill Book Company, New York, 1978. ISBN 0-07-035310-7.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publ., 1993.
D. Michie. Machine Intelligence at Edinburgh. In On Machine Intelligence, pages 143–155. Edinburgh University Press, 1974.
C. Pixley, S.-W. Jeong, and G. D. Hachtel. Exact calculation of synchronization sequences based on binary decision diagrams. In Proceedings of the 29th Conference on Design Automation, pages 620–623, Los Alamitos, CA, USA, June 1992. IEEE Computer Society Press.
J.-K. Rho, F. Somenzi, and C. Pixley. Minimum length synchronizing sequences of finite state machine. In ACM-SIGDA; IEEE, editor, Proceedings of the 30th ACM/IEEE Design Automation Conference, pages 463–468, Dallas, TX, June 1993. ACM Press.
J. Rintanen. Constructing conditional plans by a theorem-prover. Journal of Artificial Intellegence Research, 10:323–352, 1999.
David E. Smith and Daniel S. Weld. Conformant graphplan. In Proceedings of the 15th National Conference on Artificial Intelligence (AAAI-98) and of the 10th Conference on Innovative Applications of Artificial Intelligence (IAAI-98), pages 889–896, Menlo Park, July 26–30 1998. AAAI Press.
S. Yang. Logic synthesis and optimization benchmarks user guide version 3.0. Technical report, Microelectronics Center of North Carolina, Research Triangle Park, January 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cimatti, A., Roveri, M., Bertoli, P. (2001). Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_22
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive