
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Andrew S. Miner, "Saturation for a General Class of Models," IEEE Transactions on Software Engineering, vol. 32, no. 8, pp. 559570, August, 2006.  
BibTex  x  
@article{ 10.1109/TSE.2006.81, author = {Andrew S. Miner}, title = {Saturation for a General Class of Models}, journal ={IEEE Transactions on Software Engineering}, volume = {32}, number = {8}, issn = {00985589}, year = {2006}, pages = {559570}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2006.81}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Saturation for a General Class of Models IS  8 SN  00985589 SP559 EP570 EPD  559570 A1  Andrew S. Miner, PY  2006 KW  Model checking KW  stochastic analysis. VL  32 JA  IEEE Transactions on Software Engineering ER   
[1] R.E. Bryant, “GraphBased Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. 35, no. 8, pp. 677691, Aug. 1986.
[2] R.E. Bryant, “Symbolic Boolean Manipulation with Ordered BinaryDecision Diagrams,” ACM Computing Surveys, vol. 24, no. 3, pp. 293318, Sept. 1992.
[3] P. Buchholz, “Hierarchical Structuring of Superposed GSPNs,” Proc. Int'l Workshop Petri Nets and Performance Models (PNPM '97), pp. 8190, 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. 265286, 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. 142170, 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. 7897, Sept. 2003.
[9] G. Ciardo, G. Luettgen, and R. Siminiceanu, “Efficient Symbolic StateSpace Construction for Asynchronous Systems,” Proc. Int'l Conf. Application and Theory of Petri Nets (ICATPN 2000), pp. 103122, 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. 328342, 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. 379393, 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. 2231, Sept. 1999.
[13] G. Ciardo and R. Siminiceanu, “Using EdgeValued Decision Diagrams for Symbolic Generation of Shortest Paths,” Proc. Int'l Conf. Formal Methods in ComputerAided Design (FMCAD 2002), pp.256273, Nov. 2002.
[14] G. Ciardo and K.S. Trivedi, “A Decomposition Approach for Stochastic Reward Net Models,” Performance Evaluation, vol. 18, no. 1, pp. 3759, 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. 188199, Apr. 2002.
[17] M. Davio, “Kronecker Products and Shuffle Algebra,” IEEE Trans. Computers, vol. 30, no. 2, pp. 116125, Feb. 1981.
[18] S. Derisavi, P. Kemper, and W.H. Sanders, “Symbolic StateSpace Exploration and Numerical Analysis of StateSharing Composed Models,” Linear Algebra and Its Applications, vol. 386, pp. 137166, July 2004.
[19] P. Fernandes, B. Plateau, and W.J. Stewart, “Efficient DescriptorVector Multiplication in Stochastic Automata Networks,” J. ACM, vol. 45, no. 3, pp. 381414, 1998.
[20] C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall Int'l, 1985.
[21] T. Kam, T. Villa, R. Brayton, and A. SangiovanniVincentelli, “MultiValued Decision Diagrams: Theory and Applications,” MultipleValued Logic, vol. 4, nos. 12, pp. 962, 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. 489507, 1988.
[23] P. Kemper, “Numerical Analysis of Superposed GSPNs,” IEEE Trans. Software Eng., vol. 22, no. 9, pp. 615628, Sept. 1996.
[24] P. Kemper, “Reachability Analysis Based on Structured Representations,” Proc. Int'l Conf. Application and Theory of Petri Nets (ICATPN 1996), pp. 269288, June 1996.
[25] K. Lampka and M. Siegle, “MTBDDBased ActivityLocal State Graph Generation,” Proc. Int'l Workshop Performability Modelling of Computer and Comm. Systems (PMCCS6), pp. 1518, Sept. 2003.
[26] A. Miner and D. Parker, “Symbolic Representations and Analysis of Large State Spaces,” Validation of Stochastic Systems, pp. 296338, 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. 101110, Sept. 2001.
[28] A.S. Miner, “Implicit GSPN Reachability Set Generation Using Decision Diagrams,” Performance Evaluation, vol. 56, nos. 14, pp.145165, Mar. 2004.
[29] A.S. Miner, “Saturation for a General Class of Models,” Proc. Int'l Conf. Quantitative Evaluation of Systems (QEST '04), pp. 282291, 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. 625, June 1999.
[31] T. Murata, “Petri Nets: Properties, Analysis and Applications,” Proc. IEEE, vol. 77, no. 4, pp. 541580, 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. 416435, June 1994.
[33] B. Plateau, “On the Stochastic Structure of Parallelism and Synchronisation Models for Distributed Algorithms,” Proc. SIGMETRICS Conf., pp. 147153, May 1985.
[34] O. Roig, J. Cortadella, and E. Pastor, “Verification of Asynchronous Circuits by BDDBased Model Checking of Petri Nets,” Proc. Int'l Conf. Application and Theory of Petri Nets (ICATPN 1995), pp.374391, June 1995.
[35] W.H. Sanders and L.M. Malhis, “Dependability Evaluation Using Composed SANBased Reward Models,” J. Parallel and Distributed Computing, vol. 15, no. 3, pp. 238254, July 1992.
[36] A. Valmari, “A Stubborn Attack on State Explosion,” Proc. Workshop Computer Aided Verification (CAV 1990), pp. 156165, 1990.
[37] C.M. Woodside and Y. Li, “Performance Petri Net Analysis of Commmunications Protocol Software by DelayEquivalent Aggregation,” Proc. Int'l Workshop Petri Nets and Performance Models (PNPM '91), pp. 6473, Dec. 1991.