Abstract
This paper describes a technique for generating a logical formula that differentiates between two bisimulation-inequivalent finite-state systems. The method works in conjunction with a partition-refinement algorithm for computing bisimulation equivalence and yields formulas that are often minimal in a precisely defined sense.
Research supported by NSF/DARPA research grant CCR-9014775.
Chapter PDF
References
Bloom, B., S. Istrail and A. Meyer. “Bisimulation Can't Be Traced.” In Proceedings of the ACM Symposium on Principles of Programming Languages, 1988.
Boudol, G., V. Roy, R. de Simone and D. Vergamini, “Process Algebras and Systems of Communicating Processes.” In Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science 407, 1–10. Springer-Verlag, Berlin, 1990.
Brookes, S.D., C.A.R. Hoare and A.W. Roscoe. “A Theory of Communicating Sequential Processes.” Journal of the ACM, v. 31, n. 3, July 1984, pp. 560–599.
Cleaveland, R. and M. Hennessy. “Testing Equivalence as a Bisimulation Equivalence.” In Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science 407, 11–23. Springer-Verlag, Berlin, 1990.
Cleaveland, R., J. Parrow and B. Steffen. “A Semantics-Based Tool for the Verification of Finite-State Systems.” In Proceedings of the Ninth IFIP Symposium on Protocol Specification, Testing and Verification, 287–302. North-Holland, Amsterdam, 1990.
Cleaveland, R., J. Parrow and B. Steffen. “The Concurrency Workbench.” In Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science 407, 24–37. Springer-Verlag, Berlin, 1989.
DeNicola, R., and Hennessy, M. “Testing Equivalences for Processes.” Theoretical Computer Science, v. 34, 1983, 83–133.
Hennessy, M. Algebraic Theory of Processes. MIT Press, Boston, 1988.
Hennessy, M. and R. Milner. “Algebraic Laws for Nondeterminism and Concurrency”. Journal of the Association for Computing Machinery, v. 32, n. 1, January 1985, 137–161.
Hillerström, M. Verification of CCS-processes. M.Sc. Thesis, Computer Science Department, Aalborg University, 1987.
Kanellakis, P. and Smolka, S.A. “CCS Expressions, Finite State Processes, and Three Problems of Equivalence.” In Proceedings of the Second ACM Symposium on the Principles of Distributed Computing, 1983.
Larsen, K. and A. Skou. “Bisimulation through Probabilistic Testing.” Proceedings of the ACM Symposium on Principles of Programming Languages, 1989.
Malhotra, J., Smolka, S.A., Giacalone, A. and Shapiro, R. “Winston: A Tool for Hierarchical Design and Simulation of Concurrent Systems.” In Proceedings of the Workshop on Specification and Verification of Concurrent Systems, University of Stirling, Scotland, 1988.
Milner, R. Communication and Concurrency. Prentice Hall, 1989.
Paige, R. and Tarjan, R.E. “Three Partition Refinement Algorithms.” SIAM Journal of Computing, v. 16, n. 6, December 1987, 973–989.
Pnueli, A. “Linear and Branching Structures in the Semantics and Logics of Reactive Systems.” Lecture Notes in Computer Science 194, 14–32. Springer-Verlag, Berlin, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cleveland, R. (1991). On automatically explaining bisimulation inequivalence. 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/BFb0023750
Download citation
DOI: https://doi.org/10.1007/BFb0023750
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