Abstract
We here discuss an approach which uses the optimal simulation — a kind of reachability relation — to enable reasoning about important dynamic properties of a concurrent system. The optimal simulation usually involves only a very small subset of the possible behaviours generated by the system, yet provides a sufficient information to reason about a number of interesting system's properties (such as deadlock-freeness and liveness). In this paper we show how the optimal simulation might be used to generate a reachability graph which is usually much smaller than the standard reachability graph of the system; however, both graphs essentially convey the same information about its dynamic behaviour.
Chapter PDF
References
Cartier P., Foata D., Problemes combinatoires de communication et rearrangements, Lecture Notes in Mathematics 85, Springer 1969.
Clarke E.M., Grümberg O., Research on Automatic Verification of Finite-State Concurrent Systems, Ann. Rev. Comp. Sci. 2(1987), 269–290.
Clarke E.M., Emerson E.A., Sistla A.P., Automatic Verification of Finite-State Systems using Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems 8(1986), 244–263.
Godefroid P., Using Partial Orders to Improve Automatic Verification Methods, Proc. of CAV'90, this volume.
Hennessy M. and Milner R., Algebraic Laws for Nondeterminism and Concurrency, JACM 32(1985), 136–161.
Hoare C.A.R., Communicating Sequential Processes, Prentice-Hall, 1985.
Janicki R., Lauer P.E., Koutny M., Devillers R., Concurrent and Maximally Concurrent Evolution of Non-Sequential Systems, Theoretical Computer Science 43(1986), 213–238.
Janicki R., Koutny M., Towards a Theory of Simulation for Verification of Concurrent Systems, Lecture Notes in Computer Science 366, Springer 1989, 73–88.
Janicki R., Koutny M., Optimal Simulation for Verification of Concurrent Systems, Technical Report No. 89-05, McMaster University, Hamilton, Ontario, 1989.
Janicki R., Koutny M., On Some Implementation of Optimal Simulations, Technical Report No. 90-07, McMaster University, Hamilton, Ontario, 1990 (also to appear in the ACM/AMS DIMACS series).
Jensen K., Coloured Petri Nets, LNCS 254, Springer 1987, pp. 248–299.
Keller R.M., Formal Verification of Concurrent Programs, CACM 19(7), 1976, 371–384.
Lauer P.E., Shields M.W., Cotronis J.Y., Formal Behavioural Specification of Concurrent Systems without Globality Assumptions, Lecture Notes in Computer Science 107, Springer 1981, 115–151.
Martinez J., Silva M., A Simple and Fast Algorithm to Obtain All Invariants of a Generalized Petri Net, Informatik-Fachberichte 52, Springer 1982, 301–310.
Mazurkiewicz A., Trace Theory, Lecture Notes in Computer Science 255, Springer 1986, 297–324.
Morgan E.T, Razouk R.R., Interactive State-Space Analysis of Concurrent Systems, IEEE Transactions on Software Engineering 13(10), 1987.
Reisig W., Petri Nets, Springer 1985.
Szpilrajn-Marczewski E., Sur l'extension de l'ordre partial, Fundamenta Mathematicae 16 (1930), pp. 386–389.
Tauber D., Finite Representations of CCS and TCSP Programs by Automata and Petri Nets, Lecture Notes in Computer Science 369, Springer 1989.
Valmari A., Stubborn Sets for Reduced State Space Generation, Proc. of the 10th International Conference on Application and Theory of Petri Nets, Bonn, June, 1989.
Zielonka W., Safe Executions of Recognizable Trace Languages by Asynchronous Automata, Lecture Notes in Computer Science 363, Springer 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Janicki, R., Koutny, M. (1991). Using optimal simulations to reduce reachability graphs. In: Clarke, E.M., Kurshan, R.P. (eds) Computer-Aided Verification. CAV 1990. Lecture Notes in Computer Science, vol 531. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023730
Download citation
DOI: https://doi.org/10.1007/BFb0023730
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54477-7
Online ISBN: 978-3-540-38394-9
eBook Packages: Springer Book Archive