Abstract
We propose a compositional approach to handle complex and large systems described as a network of synchronized components. The approach combines and extends known techniques including Kronecker representations, bisimulation equivalences and decision diagrams in order to explore and represent extremely large state spaces.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
P. Buchholz. Hierarchical structuring of superposed GSPNs. IEEE Trans. on Software Engineering. 25(2):166–181, 1999.
P. Buchholz and P. Kemper. Modular state level analysis of distributed systems — techniques and tool support. In W.R. Cleaveland, editor, Tools and Algorithms for the Construction and Analysis of Systems, pages 420–434. Springer LNCS 1579, 1999.
G. Ciardo and A. Miner. A data structure for the efficient Kronecker solution of GSPNs. In Proc. 8th int. Work. Petri Nets and Performance Models, IEEE CS Press, 1999.
E. M. Clarke, E. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. Programming Lang. and Sys., 8(2):244–263, 1986.
E. M. Clarke and J. M. Wing et al. Formal methods: State of the art and future directions. ACM Comp. Surveys, 28(4):626–643, 1996.
R. Cleaveland, J. Parrow. and B. Steffen. The concurrency workbench: a semantics based tool for the verification of concurrent systems. ACM Trans. Programming Lang. and Sys., 15(1):36–72, 1993.
M. Heiner. Verification and optimization of control programs by Petri nets without state explosion. In Proc. 2nd Workshop on Manufacturing and Petri Nets. pages 69–84, 1997. available via http://www-dssz.Informatik.TU-Cottbus.DE/wwwdssz/.
G. J. Holzmann. An analysis of bitstate hashing. Formal Methods in System Design. 13(3):301–314, 1998.
T. Kam. State minimization of finite state machines using implicit techniques. Phd thesis, University of California at Berkeley, 1995.
P. Kemper. Reachability analysis based on structured representations. In J. Billington and W. Reisig, editors, Application and Theory of Petri Nets 1996, pages 269–288. Springer LNCS 1091, 1996.
B. Plateau. On the stochastic structure of parallelism and synchro nisation models for distributed algorithms. Performance Evaluation Review, 13:142–154, 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media New York
About this chapter
Cite this chapter
Buchholz, P., Kemper, P. (2000). Efficient Computation and Representation of Large Reachability Sets for Composed Automata. In: Boel, R., Stremersch, G. (eds) Discrete Event Systems. The Springer International Series in Engineering and Computer Science, vol 569. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-4493-7_4
Download citation
DOI: https://doi.org/10.1007/978-1-4615-4493-7_4
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-7025-3
Online ISBN: 978-1-4615-4493-7
eBook Packages: Springer Book Archive