Abstract
The paper considers the problem of checking abstraction between two finite-state fair discrete systems. In automata-theoretic terms this is trace inclusion between two Streett automata. We propose to reduce this problem to an algorithm for checking fair simulation between two generalized Büchi automata. For solving this question we present a new triply nested μ-calculus formula which can be implemented by symbolic methods.
We then show that every trace inclusion of this type can be solved by fair simulation, provided we augment the concrete system (the contained automaton) by appropriate auxiliary variables. This establishes that fair simulation offers a complete method for checking trace inclusion. We illustrate the feasibility of the approach by algorithmically checking abstraction between finite state systems whose abstraction could only be verified by deductive methods up to now.
This research was supported in part by THE ISRAEL SCIENCE FOUNDATION (grant no.106/02-1) and the John von-Neumann Minerva center for Verification of Reactive Systems.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Lamport, L.: The existence of refinement mappings. TCS 82 (1991)
Bloom, B., Paige, R.: Transformational design and implementation of a new efficient solution to the ready simulation problem. SCP 24, 189–220 (1996)
Choueka, Y.: Theories of automata on ω-tapes: A simplified approach. In: JCSS (1974)
de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: dynamic programs for omega-regular objectives. In: 16th LICS (2001)
Emerson, E.A., Lei, C.L.: Efficient model-checking in fragments of the propositional modal μ-calculus. In: 1st LICS, pp. 267–278 (1986)
Emerson, E.A.: Model checking and the μ-calculus. In: Descriptive Complexity and Finite Models, pp. 185–214. AMS (1997)
Gurevich, Y., Harrington, L.A.: Automata, trees and games. In: 14th STOC (1982)
Grumberg, O., Long, D.E.: Model checking and modular verification. TOPLAS 16(3), 843–871 (1994)
Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: 36th FOCS, pp. 453–462 (1995)
Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 273–287. Springer, Heidelberg (1997)
Henzinger, T., Rajamani, S.: Fair bisimulation. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, p. 299. Springer, Heidelberg (2000)
Jurdzinski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Kozen, D.: Results on the propositional μ-calculus. TCS 27, 333–354 (1983)
Kesten, Y., Pnueli, A.: Control and data abstractions: The cornerstones of practical formal verification. STTT 2(1), 328–342 (2000)
Kesten, Y., Pnueli, A.: Verification by finitary abstraction. IC 163, 203–243 (2000)
Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 1–16. Springer, Heidelberg (1998)
Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.: Network invariants in action. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–105. Springer, Heidelberg (2002)
Kupferman, O., Piterman, N., Vardi, M.Y.: Fair equivalence relations. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 151–163. Springer, Heidelberg (2000)
Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: 30th STOC, pp. 224–233 (1998)
Lodaya, K., Thiagarajan, P.S.: A modal logic for a subclass of events structures. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 290–303. Springer, Heidelberg (1987)
Manna, Z., Anuchitanukul, A., Bjørner, N., Browne, A., Chang, E., Colón, M., De Alfaro, L., Devarajan, H., Sipma, H., Uribe, T.E.: STeP. Tech. Report, Stanford (1994)
Milner, R.: An algebraic definition of simulation between programs. In: IJCAI (1971)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)
Safra, S.: Exponential determinization for ω-automata with strong-fairness acceptance condition. In: 24th STOC (1992)
Vardi, M.Y.: Verification of concurrent programs – the automata-theoretic framework. APAL 51, 79–98 (1991)
Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 68–80. Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kesten, Y., Piterman, N., Pnueli, A. (2003). Bridging the Gap between Fair Simulation and Trace Inclusion. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_36
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive