Abstract
In the automata-theoretic approach to model checking we check the emptiness of the product of a system S with an automaton \(\mathcal {A}\neg\psi\) for the complemented specification. This gives rise to two automata-theoretic problems: complementation of word automata, which is used in order to generate \(\mathcal {A}\neg\psi\), and the emptiness problem, to which model checking is reduced. Both problems have numerous other applications, and have been extensively studied for nondeterministic Büchi word automata (NBW). Nondeterministic generalized Büchi word automata (NGBW) have become popular in specification and verification and are now used in applications traditionally assigned to NBW. This is due to their richer acceptance condition, which leads to automata with fewer states and a simpler underlying structure.
In this paper we analyze runs of NGBW and use the analysis in order to describe a new complementation construction and a symbolic emptiness algorithm for NGBW. The complementation construction exponentially improves the best known construction for NGBW and is easy to implement. The emptiness algorithm is almost identical to a known variant of the Emerson-Lei algorithm, and our contribution is the strong relation we draw between the complementation construction and the emptiness algorithm – both naturally follow from the analysis of the runs, which easily implies their correctness. This relation leads to a new certified model-checking procedure, where a positive answer to the model-checking query is accompanied by a certificate whose correctness can be checked by methods independent of the model checker. Unlike certificates generated in previous works on certified model checking, our analysis enables us to generate a certificate that can be checked automatically and symbolically.
Chapter PDF
Similar content being viewed by others
References
Bahar, R., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi", F.: Algebraic decision diagrams and their applications. FMSD 10(2/3), 171–206 (1997)
Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n log n symbolic steps. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 37–54. Springer, Heidelberg (2000)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, pp. 1–12. Stanford University Press, Stanford (1962)
Choueka, Y.: Theories of automata on ω-tapes: A simplified approach. Journal of Computer and System Sciences 8, 117–141 (1974)
Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional μ-calculus. In: Proc. 1st LICS, pp. 267–278 (1986)
Fisler, K., Fraer, R., Kamhi, G., Vardi, M.Y., Yang, Z.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 420–434. Springer, Heidelberg (2001)
Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic Büchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 96–110. Springer, Heidelberg (2003)
Gentilini, R., Piazza, C., Policriti, A.: Computing strongly connected components in a linear number of symbolic steps. In: Proc. 14th SODA, pp. 573–582 (2003)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing, and Verification, August 1995, pp. 3–18. Chapman & Hall, Boca Raton (1995)
De Giacomo, G., Vardi, M.Y.: Automata-theoretic approach to planning for temporally extended goals. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS (LNAI), vol. 1809, pp. 226–238. Springer, Heidelberg (2000)
Hardin, R.H., Kurshan, R.P., Shukla, S.K., Vardi, M.Y.: A new heuristic for bad cycle detection using BDDs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 268–278. Springer, Heidelberg (1997)
Hojati, R., Touati, H., Kurshan, R., Brayton, R.: Efficient ω-regula language containment. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, Springer, Heidelberg (1993)
Klarlund, N.: Progress measures for complementation of ω-automata with applications to temporal logic. In: Proc. 32nd FOCS, pp. 358–367 (1991)
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)
Kurshan, R.P.: The complexity of verification. In: 26th STOC, pp. 365–371 (1994)
Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal methods in System Design 19(3), 291–314 (2001)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. on Computational Logic 2001(2), 408–429 (2001)
Merz, S.: Weak alternating automata in Isabelle/HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 423–440. Springer, Heidelberg (2000)
Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)
Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)
Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by ∀-automata. In: Proc. Proc. 14th POPL, pp. 1–12 (1987)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification, Berlin (January 1992)
Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM TOPLAS 6(1), 68–93 (1984)
Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–13. Springer, Heidelberg (2001)
Necula, G.C.: Proof-carrying code. In: Proc. 24th POPL, pp. 106–119 (1997)
Peled, D., Pnueli, A., Zuck, L.D.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 292–304. Springer, Heidelberg (2001)
Peled, D., Zuck, L.D.: From model checking to a temporal proof. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 1–14. Springer, Heidelberg (2001)
Ravi, K., Bloem, R., Somenzi, F.: A comparative study of symbolic algorithms for the computation of fair cycles. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 143–160. Springer, Heidelberg (2000)
Safra, S.: On the complexity of ω-automata. In: 29th FOCS, pp. 319–327 (1988)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
Sistla, A.P.: Satefy, liveness and fairness in temporal logic. Formal Aspects of Computing 6, 495–511 (1994)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. TCS 49, 217–237 (1987)
Tasiran, S., Hojati, R., Brayton, R.K.: Language containment using nondeterministic ω-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 261–277. Springer, Heidelberg (1995)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1-2), 72–99 (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kupferman, O., Vardi, M.Y. (2004). From Complementation to Certification. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_43
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive