This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Saturation for a General Class of Models
August 2006 (vol. 32 no. 8)
pp. 559-570
Andrew S. Miner, IEEE Computer Society
Implicit techniques for construction and representation of the reachability set of a high-level model have become quite efficient for certain types of models. In particular, previous work developed a "saturation” algorithm that exploits asynchronous behavior to efficiently construct the reachability set using multiway decision diagrams, but using a Kronecker product expression to represent each model event. For models whose events do not naturally fall into this category, use of the saturation algorithm requires adjusting the model by combining components or splitting events into subevents until a Kronecker product expression is possible. In practice, this can lead to additional overheads during reachability set construction. This paper presents a new version of the saturation algorithm that works for a general class of models: models whose events are not necessarily expressible as Kronecker products, models containing events with complex priority structures, and models whose state variables have unknown bounds. Experimental results are given for several examples.

[1] R.E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. 35, no. 8, pp. 677-691, Aug. 1986.
[2] R.E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,” ACM Computing Surveys, vol. 24, no. 3, pp. 293-318, Sept. 1992.
[3] P. Buchholz, “Hierarchical Structuring of Superposed GSPNs,” Proc. Int'l Workshop Petri Nets and Performance Models (PNPM '97), pp. 81-90, June 1997.
[4] P. Buchholz and P. Kemper, “Efficient Computation and Representation of Large Reachability Sets for Composed Automata,” Discrete Event Dynamic Systems: Theory and Applications, vol. 12, pp. 265-286, 2002.
[5] P. Buchholz and P. Kemper, “Kronecker Based Matrix Representations for Large Markov Models,” Validation of Stochastic Systems, 2004.
[6] J. Burch, E. Clarke, and D. Long, “Symbolic Model Checking with Partitioned Transition Relations,” Proc. Int'l Conf. VLSI, Aug. 1991.
[7] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, “Symbolic Model Checking: $10^{20}$ States and Beyond,” Information and Computation, vol. 98, no. 2, pp. 142-170, June 1992.
[8] G. Ciardo, R. Jones, A. Miner, and R. Siminiceanu, “Logical and Stochastic Modeling with SMART,” Proc. Int'l Conf. Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS 2003), pp. 78-97, Sept. 2003.
[9] G. Ciardo, G. Luettgen, and R. Siminiceanu, “Efficient Symbolic State-Space Construction for Asynchronous Systems,” Proc. Int'l Conf. Application and Theory of Petri Nets (ICATPN 2000), pp. 103-122, June 2000.
[10] G. Ciardo, G. Luettgen, and R. Siminiceanu, “Saturation: An Efficient Iteration Strategy for Symbolic State Space Generation,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), pp. 328-342, Apr. 2001.
[11] G. Ciardo, R. Marmorstein, and R. Siminiceanu, “Saturation Unbound,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), pp. 379-393, Apr. 2003.
[12] G. Ciardo and A.S. Miner, “A Data Structure for the Efficient Kronecker Solution of GSPNs,” Proc. Int'l Workshop Petri Nets and Performance Models (PNPM '99), pp. 22-31, Sept. 1999.
[13] G. Ciardo and R. Siminiceanu, “Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths,” Proc. Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD 2002), pp.256-273, Nov. 2002.
[14] G. Ciardo and K.S. Trivedi, “A Decomposition Approach for Stochastic Reward Net Models,” Performance Evaluation, vol. 18, no. 1, pp. 37-59, 1993.
[15] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 1999.
[16] I. Davies, W.J. Knottenbelt, and P.S. Kritzinger, “Symbolic Methods for the State Space Exploration of GSPN Models,” Proc. Int'l Conf. Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS 2002), pp. 188-199, Apr. 2002.
[17] M. Davio, “Kronecker Products and Shuffle Algebra,” IEEE Trans. Computers, vol. 30, no. 2, pp. 116-125, Feb. 1981.
[18] S. Derisavi, P. Kemper, and W.H. Sanders, “Symbolic State-Space Exploration and Numerical Analysis of State-Sharing Composed Models,” Linear Algebra and Its Applications, vol. 386, pp. 137-166, July 2004.
[19] P. Fernandes, B. Plateau, and W.J. Stewart, “Efficient Descriptor-Vector Multiplication in Stochastic Automata Networks,” J. ACM, vol. 45, no. 3, pp. 381-414, 1998.
[20] C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall Int'l, 1985.
[21] T. Kam, T. Villa, R. Brayton, and A. Sangiovanni-Vincentelli, “Multi-Valued Decision Diagrams: Theory and Applications,” Multiple-Valued Logic, vol. 4, nos. 1-2, pp. 9-62, 1998.
[22] S. Katz and D. Peled, “An Efficient Verification Method for Parallel and Distributed Programs,” Proc. Workshop Linear Time, Branching Time and Partial Order Logics and Models for Concurrency, pp. 489-507, 1988.
[23] P. Kemper, “Numerical Analysis of Superposed GSPNs,” IEEE Trans. Software Eng., vol. 22, no. 9, pp. 615-628, Sept. 1996.
[24] P. Kemper, “Reachability Analysis Based on Structured Representations,” Proc. Int'l Conf. Application and Theory of Petri Nets (ICATPN 1996), pp. 269-288, June 1996.
[25] K. Lampka and M. Siegle, “MTBDD-Based Activity-Local State Graph Generation,” Proc. Int'l Workshop Performability Modelling of Computer and Comm. Systems (PMCCS-6), pp. 15-18, Sept. 2003.
[26] A. Miner and D. Parker, “Symbolic Representations and Analysis of Large State Spaces,” Validation of Stochastic Systems, pp. 296-338, 2004.
[27] A.S. Miner, “Efficient Solution of GSPNs Using Canonical Matrix Diagrams,” Proc. Int'l Workshop Petri Nets and Performance Models (PNPM '01), pp. 101-110, Sept. 2001.
[28] A.S. Miner, “Implicit GSPN Reachability Set Generation Using Decision Diagrams,” Performance Evaluation, vol. 56, nos. 1-4, pp.145-165, Mar. 2004.
[29] A.S. Miner, “Saturation for a General Class of Models,” Proc. Int'l Conf. Quantitative Evaluation of Systems (QEST '04), pp. 282-291, Sept. 2004.
[30] A.S. Miner and G. Ciardo, “Efficient Reachability Set Generation and Storage Using Decision Diagrams,” Proc. Int'l Conf. Application and Theory of Petri Nets (ICATPN 1999), pp. 6-25, June 1999.
[31] T. Murata, “Petri Nets: Properties, Analysis and Applications,” Proc. IEEE, vol. 77, no. 4, pp. 541-580, Apr. 1989.
[32] E. Pastor, O. Roig, J. Cortadella, and R. Badia, “Petri Net Analysis Using Boolean Manipulation,” Proc. Proc. Int'l Conf. Application and Theory of Petri Nets (ICATPN 1994), pp. 416-435, June 1994.
[33] B. Plateau, “On the Stochastic Structure of Parallelism and Synchronisation Models for Distributed Algorithms,” Proc. SIGMETRICS Conf., pp. 147-153, May 1985.
[34] O. Roig, J. Cortadella, and E. Pastor, “Verification of Asynchronous Circuits by BDD-Based Model Checking of Petri Nets,” Proc. Int'l Conf. Application and Theory of Petri Nets (ICATPN 1995), pp.374-391, June 1995.
[35] W.H. Sanders and L.M. Malhis, “Dependability Evaluation Using Composed SAN-Based Reward Models,” J. Parallel and Distributed Computing, vol. 15, no. 3, pp. 238-254, July 1992.
[36] A. Valmari, “A Stubborn Attack on State Explosion,” Proc. Workshop Computer Aided Verification (CAV 1990), pp. 156-165, 1990.
[37] C.M. Woodside and Y. Li, “Performance Petri Net Analysis of Commmunications Protocol Software by Delay-Equivalent Aggregation,” Proc. Int'l Workshop Petri Nets and Performance Models (PNPM '91), pp. 64-73, Dec. 1991.

Index Terms:
Model checking, stochastic analysis.
Citation:
Andrew S. Miner, "Saturation for a General Class of Models," IEEE Transactions on Software Engineering, vol. 32, no. 8, pp. 559-570, Aug. 2006, doi:10.1109/TSE.2006.81
Usage of this product signifies your acceptance of the Terms of Use.