Abstract
In this paper we compare among four notions of fair simulation: direct [6], delay [7], game [10], and exists [9]. Our comparison refers to three main aspects: The time complexity of constructing the fair simulation, the ability to use it for minimization, and the relationship between the fair simulations and universal branching-time logics.
Based on our comparison we derive several practical implications: We develop an efficient approximated minimization algorithm for the direct/delay simulations. In addition, we suggest a new implementation for the assume-guarantee modular framework presented in [9]. The new implementation, significantly improves the complexity of the framework.
Chapter PDF
Similar content being viewed by others
References
A. Aziz, V. Singhal, T.R. Shiple, A.L. Sangiovanni-Vincentelli, F. Balarin, and R.K. Brayton. Equivalences for fair kripke structures. In ICALP, LNCS 840, pages 364–375, 1994.
S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property preserving simulation. In Computer-aided Verification, volume 663 LNCS, pages 260–273, 1981.
D. Bustan and O. Grumberg. Simulation based minimization. In Conference on Automated Deduction, volume 17, pages 255–270, 2000.
E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 1999.
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In Proceedings of Computer-Aided Verification, volume 531 of LNCS, pages 233–242, 1991.
D.L. Dill, A.J. Hu, and H. Wong-Toi. Checking for language inclusion using simulation relation. In Computer-Aided Verification, LNCS 575, pages 255–265, 1991.
K. Etessami, Th. Wilke, and R. Schuller. Fair simulation relations, parity games, and state space reduction for Büchi automata. In Automata,L anguages and Programming, 28th international collquium, LNCS 2076, pages 694–707, 2001.
N. Francez. The Analysis of Cyclic Programs. PhD thesis, Weizmann Institute of Science, 1976.
O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems (TOPLAS), 16(3):843–871, 1994.
T.A. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. In Proc. 8th Conference on Concurrency Theory, LNCS 1234, 1997.
C. B. Jones. Specification and design of (parallel) programs. In In International Federation for Information Processing (IFIP), pages 321–332, 1983.
O. Kupferman and M.Y. Vardi. Verification of fair transition systems. In Computer Aided Verification (CAV’96), LNCS 1102, pages 372–382, 1996.
O. Kupferman and M.Y. Vardi. Modular model checking. In Proc. Compositionality Workshop, LNCS 1536. Springer-Verlag, 1998.
R. Milner. An algebraic definition of simulation between programs. In Proc. of the 2nd International Joint Conferences on Artificial Intelligence (IJCAI), pages 481–489, London, UK, 1971.
J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, 7(7):417–426, 1981.
A. Pnueli. In transition for global to modular temporal reasoning about programs. In K. R. Apt, editor, Logics and Models of Concurrent Systems, volume 13 of NATO ASI series F. sv, 1984.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bustan, D., Grumberg, O. (2002). Applicability of Fair Simulation. In: Katoen, JP., Stevens, P. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2002. Lecture Notes in Computer Science, vol 2280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46002-0_28
Download citation
DOI: https://doi.org/10.1007/3-540-46002-0_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43419-1
Online ISBN: 978-3-540-46002-2
eBook Packages: Springer Book Archive