Abstract
In previous work, we proposed a “saturation” algorithm for symbolic state-space generation characterized by the use of multi-valued decision diagrams, boolean Kronecker operators, event locality, and a special iteration strategy. This approach outperforms traditional BDD-based techniques by several orders of magnitude in both space and time but, like them, assumes a priori knowledge of each submodel’s state space. We introduce a new algorithm that merges explicit local statespace discovery with symbolic global state-space generation. This relieves the modeler from worrying about the behavior of submodels in isolation.
Work supported in part by the National Aeronautics and Space Administration under grants NAG-1-2168 and NAG-1-02095 and by the National Science Foundation under grants CCR-0219745 and ACI-0203971.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons, New York, 1995.
V. Amoia, G. De Micheli, and M. Santomauro. Computer-oriented formulation of transition-rate matrices via Kronecker algebra. IEEE Trans. Rel., 30:123–132, June 1981.
R. Bloem, K. Ravi, and F. Somenzi. Symbolic guided search for CTL model checking. In Proc. 37th Conf. on Design Automation, p. 29–34. ACM Press, 2000.
A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In Computer Aided Verification, pages 403–418, 2000.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp., 35(8):677–691, Aug. 1986.
R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comp. Surv., 24(3):393–318, 1992.
P. Buchholz, G. Ciardo, S. Donatelli, and P. Kemper. Complexity of memorye ficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comp., 12(3):203–222, 2000.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th Annual IEEE Symp. on Logic in Computer Science, pages 428–439, Philadelphia, PA, 4–7 June 1990. IEEE Comp. Soc. Press.
G. Ciardo. Petri nets with marking-dependent arc multiplicity: properties and analysis. In R. Valette, editor, Proc. 15th Int. Conf. on Applications and Theory of Petri Nets, LNCS 815, pages 179–198, Zaragoza, Spain, June 1994. Springer-Verlag.
G. Ciardo, R. L. Jones, A. S. Miner, and R. Siminiceanu. SMART: Stochastic Model Analyzer for Reliability and Timing. In P. Kemper, editor, Tools of Int. Multiconference on Measurement, Modelling and Evaluation of Computer-Communication Systems, pages 29–34, Aachen, Germany, Sept. 2001.
G. Ciardo, G. Luettgen, and R. Siminiceanu. Efficient symbolic state-space construction for asynchronous systems. In M. Nielsen and D. Simpson, editors, Proc. 21th Int. Conf. on Applications and Theory of Petri Nets, LNCS 1825, pages 103–122, Aarhus, Denmark, June 2000. Springer-Verlag.
G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state space generation. In T. Margaria and W. Yi, editors, Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2031, pages 328–342, Genova, Italy, Apr. 2001. Springer-Verlag.
G. Ciardo and R. Siminiceanu. Using edge-valued decision diagrams for symbolic generation of shortest paths. In M. D. Aagaard and J. W. O’Leary, editors, Proc. Fourth International Conference on Formal Methods in Computer-Aided Design (FMCAD), LNCS 2517, pages 256–273, Portland, OR, USA, Nov. 2002. Springer-Verlag.
A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new symbolic model verifier. In CAV’ 99, LNCS 1633, pages 495–499. Springer-Verlag, 1999.
O. Coudert and J. C. Madre. Symbolic computation of the valid states of a sequential machine: algorithms and discussion. In 1991 Int. Workshop on Formal Methods in VLSI Design, pages 1–19, Miami, FL, USA, 1991.
M. Fujita, H. Fujisawa, and Y. Matsunaga. Variable ordering algorithms for ordered binary decision diagrams and their evaluation. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 12(1):6–12, 1993.
A. Geser, J. Knoop, G. Lüttgen, B. Steffen, and O. Rüthing. Chaotic fixed point iterations. Technical Report MIP-9403, Univ. of Passau, 1994.
P. Godefroid and D. E. Long. Symbolic protocol verification with queue BDDs. Formal Methods in System Design, 14(3):257–271, May 1999.
J. G. Henriksen, J. L. Jensen, M. E. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In E. Brinksma, R. Cleaveland, K. G. Larsen, T. Margaria, and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 1019, pages 89–110. Springer, 1995.
J.R. Burch, E.M. Clarke, and D.E. Long. Symbolic model checking with partitioned transition relations. In A. Halaas and P.B. Denyer, editors, Int. Conference on Very Large Scale Integration, pages 49–58, Edinburgh, Scotland, Aug. 1991. IFIP Transactions, North-Holland.
T. Kam, T. Villa, R. Brayton, and A. Sangiovanni-Vincentelli. Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic, 4(1–2):9–62, 1998.
J. Martinez and M. Silva. A simple and fast algorithm to obtain all invariants of a generalised Petri net. In Proc. 2nd European Workshop on Application and Theory of Petri Nets, pages 411–422, Bad Honnef, Germany, 1981.
A. S. Miner and G. Ciardo. Effcient reachability set generation and storage using decision diagrams. In H. Kleijn and S. Donatelli, editors, Proc. 20th Int. Conf. on Applications and Theory of Petri Nets, LNCS 1639, pages 6–25, Williamsburg, VA, USA, June 1999. Springer-Verlag.
T. Murata and R. Church. Analysis of marked graphs and Petri nets by matrix equations. Research report MDC 1.1.8, Department of information engineering, Univeristy of Illinois, Chicago, IL, Nov. 1975.
B. Plateau. On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In Proc. ACM SIGMETRICS, pages 147–153, Austin, TX, USA, May 1985.
K. Ravi and F. Somenzi. Efficient fixpoint computation for invariant checking. In Proc. Int. Conference on Computer Design (ICCD), pages 467–474, Austin, TX, Oct. 1999. IEEE Comp. Soc. Press.
F. Somenzi. CUDD: CU Decision Diagram Package, Release 2.3.1.http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciardo, G., Marmorstein, R., Siminiceanu, R. (2003). Saturation Unbound. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_27
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive