×

zbMATH — the first resource for mathematics

Bridging the gap between fair simulation and trace inclusion. (English) Zbl 1082.68055
Summary: 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 nondeterministic 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 \(\mu\)-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 an appropriate ‘non-constraining’ automaton. This establishes that fair simulation offers a complete method for checking trace inclusion for finite-state systems. 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.

MSC:
68Q45 Formal languages and automata
Software:
STeP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.; Lamport, L., The existence of refinement mappings, Theor. comput. sci., 82, 2, 253-284, (1991) · Zbl 0728.68083
[2] R. Alur, S. La Torre, P. Madhusudan, Playing games with boxes and diamonds, in: Proc. 14th International Conference on Cuncurrency Theory vol. 2761 of Lect. Notes in Comput. Sci., Springer-Verlag, Berlin, 2003, pp. 127-141 · Zbl 1274.68173
[3] Bloom, B.; Paige, R., Transformational design and implementation of a new efficient solution to the ready simulation problem, Sci. comput. programming, 24, 189-220, (1996) · Zbl 0832.68050
[4] Bryant, R., Graph-based algorithms for Boolean function manipulation, IEEE trans. comput. C, 35, 12, 1035-1044, (1986)
[5] Choueka, Y., Theories of automata on ω-tapes: a simplified approach, J. comp. syst. sci., 8, 117-141, (1974) · Zbl 0292.02033
[6] L. de Alfaro, T. Henzinger, R. Majumdar, From verification to control: dynamic programs for omega-regular objectives, in: Proc. 16th IEEE symposium logic in computer science, 2001
[7] Emerson, E., Model checking and the μ-calculus, (), 185-214 · Zbl 0877.03020
[8] Emerson, E.; Clarke, E., Characterizing correctness properties of parallel programs using fixpoints, (), 169-181 · Zbl 0456.68016
[9] E.A. Emerson, C.L. Lei, Efficient model-checking in fragments of the propositional modal μ-calculus, in: Proc. First IEEE Symp. Logic in Comput. Sci., 1986, pp. 267-278
[10] Grumberg, O.; Long, D., Model checking and modular verification, ACM trans. programming lang. syst., 16, 3, 843-871, (1994)
[11] Y. Gurevich, L. Harrington, Automata, trees and games, in: Proc. 14th ACM Symp. Theory of Comput, 1982, pp. 60-65
[12] Henzinger, M.; Henzinger, T.; Kopke, P., Computing simulations on finite and infinite graphs, (), 453-462 · Zbl 0938.68538
[13] T. Henzinger, O. Kupferman, S. Rajamani, Fair simulation, in: Proc. 8th International Conference on Concurrency Theory vol. 1243 of Lect. Notes in Comput. Sci., Springer-Verlag, Berlin, 1997, pp. 273-287 · Zbl 1009.68071
[14] T. Henzinger, S. Rajamani, Fair bisimulation, in: S. Graf, M. Schwartzbach (Eds.), Proc. 6th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems vol. 1785 of Lect. Notes in Comput. Sci. Springer-Verlag, Berlin, 2000, pp. 299-314
[15] M. Jurdzinski, Small progress measures for solving parity games, in: Proc. 17th Annual Symposium on Theoretical Aspects of Computer Science volume 1770 of Lect. Notes in Comput. Sci., Springer-Verlag, 2000, pp. 290-301 · Zbl 0962.68111
[16] Y. Kesten, N. Piterman, A. Pnueli, Bridging the gap between fair simulation and trace inclusion, in: W. Hunt Jr., F. Somenzi, (Eds.), Proc. 15th Intl. Conference on Computer Aided Verification 2003, pp. 381-392 · Zbl 1278.68178
[17] Kesten, Y.; Pnueli, A., Control and data abstractions: the cornerstones of practical formal verification, Software tools technol. transfer, 2, 1, 328-342, (2000) · Zbl 1059.68589
[18] Kesten, Y.; Pnueli, A., Verification by augmented finitary abstraction, Inform. comput., 163, 203-243, (2000) · Zbl 1003.68069
[19] Kesten, Y.; Pnueli, A.; Raviv, L., Algorithmic verification of linear temporal logic specifications, (), 1-16
[20] Y. Kesten, A. Pnueli, E. Shahar, L. Zuck, Network invariants in action, in: Proc. 13th International Conference on Concurrency Theory vol. 2421 of Lect. Notes in Comput. Sci., Springer-Verlag, Berlin, 2002, pp. 101-105 · Zbl 1012.68131
[21] Kozen, D., Results on the propositional μ-calculus, Theor. comput. sci., 27, 333-354, (1983) · Zbl 0553.03007
[22] O. Kupferman, N. Piterman, M. Vardi, Fair equivalence relations, in: S. Kapoor, S. Prasad (Eds.), in: Proc. 20th Conf. Foundations of Software Technology and Theoretical Computer Science vol. 1974 of Lect. Notes in Comput. Sci., Springer-Verlag, Berlin, 2000, pp. 151-163 · Zbl 1044.68110
[23] O. Kupferman, M. Vardi, Weak alternating automata and tree automata emptiness, in Proc. 30th ACM Symp. Theory of Comput. Dallas, 1998, pp. 224-233 · Zbl 1005.68525
[24] O. Lichtenstein, Decidability, Completeness, and Extensions of Linear Time Temporal Logic. PhD thesis, Weizmann Institute of Science, 1991
[25] K. Lodaya, P. Thiagarajan, A modal logic for a subclass of events structures, in: Proc. 14th Int. Colloq. Aut. Lang. Prog. vol. 267 of Lect. Notes in Comput. Sci., Springer-Verlag, Berlin, 1987, pp. 290-303 · Zbl 0643.68026
[26] D. Long, A. Brown, E. Clarke, S. Jha, W. Marrero, An improved algorithm for the evaluation of fixpoint expressions, in: D. Dill (Ed.), Proc. 6th Intl. Conference on Computer Aided Verification vol. 818 of Lect. Notes in Comput. Sci., Springer-Verlag, Berlin, 1994, pp. 338-350
[27] Z. Manna, A. Anuchitanukul, N. Bjørner, A. Browne, E. Chang, M. Colón, L. D. Alfaro, H. Devarajan, H. Sipma, T. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comput. Sci., Stanford University, Stanford, California, 1994
[28] Manna, Z.; Pnueli, A., Temporal verification of reactive systems: safety, (1995), Springer-Verlag New York
[29] A. Melton, D. Schmidt, D. Strecker, Galois connections and computer science applications, in: D. Pitt, S. Abramsky, A. Poigne, D. Rydeheard (Eds.), Category Theory and Computer programming vol. 240 of Lect. Notes in Comput. Sci., Springer-Verlag, Berlin, 1986, pp. 299-312 · Zbl 0622.06004
[30] Milner, R., An algebraic definition of simulation between programs, (), 481-489
[31] A. Pnueli, The temporal logic of programs, in: Proc. 18th IEEE Symp. Found. of Comput. Sci., 1977, pp. 46-57
[32] A. Pnueli, E. Shahar, A platform for combining deductive with algorithmic verification, in: R. Alur, T. Henzinger (Eds.), Proc. 8th Intl. Conference on Computer Aided Verification vol. 1102 of Lect. Notes in Comput. Sci. Springer-Verlag, 1996, pp. 184-195
[33] S. Safra, Exponential determinization for ω-automata with strong-fairness acceptance condition, in: Proc. 24th ACM Symp. on Theory of Computing, 1992 · Zbl 1120.68072
[34] Seidl, H., Fast and simple nested fixpoints, Info. proc. lett., 59, 6, 303-308, (1996) · Zbl 0900.68458
[35] Streett, R., Propositional dynamic logic of looping and converse is elementarily decidable, Inform. control, 54, 121-141, (1982) · Zbl 0515.68062
[36] M. Vardi, Personal communication, 2001
[37] Vardi, M.; Wolper, P., Reasoning about infinite computations, Inform. control, 115, 1, 1-37, (1994) · Zbl 0827.03009
[38] Vardi, M.Y., Verification of concurrent programs—the automata-theoretic framework, Ann. pure appl. logic, 51, 79-98, (1991) · Zbl 0725.03013
[39] Wolper, P., Temporal logic can be more expressive, Inform. control, 56, 72-99, (1983) · Zbl 0534.03009
[40] P. Wolper, V. Lovinfosse, Verifying properties of large sets of processes with network invariants, in: J. Sifakis (Ed.), Automatic Verification Methods for Finite State Systems vol. 407 of Lect. Notes in Comput. Sci., Springer-Verlag, Berlin, 1989, pp. 68-80
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.