Abstract
In the automata-theoretic approach to formal verification, the satisfiability and the model-checking problems for linear temporal logics are reduced to the nonemptiness problem of automata on infinite words. Modifying the nonemptiness algorithm to return a shortest witness to the nonemptiness (that is, a word of the form uv ω that is accepted by the automaton and for which |uv| is minimal) has applications in synthesis and counterexample analysis. Unlike shortest accepting runs, which have been studied in the literature, the definition of shortest witnesses is semantic and is independent on the specification formalism of the property or the system. In particular, its robustness makes it appropriate for analyzing counterexamples of concurrent systems.
We study the problem of finding shortest witnesses in automata with various types of concurrency. We show that while finding shortest witnesses is more complex than just checking nonemptiness in the nondeterministic and in the concurrent models of computation, it is not more complex in the alternating model. It follows that when the system is the composition of concurrent components, finding a shortest counterexample to its correctness is not harder than finding some counterexample. Our results give a computational motivation to translating temporal logic formulas to alternating automata, rather than going all the way to nondeterministic automata.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)
Bouajjani, A., Fernandez, J.-C., Halbwachs, N.: Minimal model genration. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 197–203. Springer, Heidelberg (1991)
Birget, J.C.: State-complexity of finite-state devices, state compressibility and incompressibility. Mathematical Systems Theory 26(3), 237–269 (1993)
Brzozowski, J.A., Leiss, E.: Finite automata and sequential networks. TCS 10, 19–35 (1980)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. International Congress on Logic, Method, and Philosophy of Science, 1960, pp. 1–12. Stanford University Press, Stanford (1962)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)
Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. 32nd DAC, pp. 427–432. IEEE Computer Society, Los Alamitos (1995)
Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)
Drusinsky, D., Harel, D.: On the power of bounded concurrency I: Finite automata. J. ACM 41(3), 517–539 (1994)
Emerson, E.A., Jutla, C.: Tree automata, μ-calculus and determinacy. In: Proc. 32nd FOCS, pp. 368–377 (1991)
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)
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM TOPLAS 16(3), 843–871 (1994)
Gastin, P., Moro, P., Zeitoun, M.: Minimization of counterexamples in spin. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 92–108. Springer, Heidelberg (2004)
Gastin, P., Oddoux, D.: Fast LTL to Büchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Galperin, H., Wigderson, A.: Succinct representations of graphs. I& C 56(3), 183–198 (1983)
Harel, D.: Statecharts: A visual formalism for complex systems. Sci. Computer Prog. 8, 231–274 (1987)
Harel, D., Kupferman, O., Vardi, M.Y.: On the complexity of verifying concurrent transition systems. I & C 173, 1–19 (2002)
Harel, D., Rosner, R., Vardi, M.Y.: On the power of bounded concurrency iii: Reasoning about programs. In: Proc. 5th LICS, pp. 478–488 (1990)
Jones, G.A., Jones, J.M., Tyrer-Jones, J.M.: Elementary Number Theory. Undergraduate Mathematics Series. Springer, Berlin (1998)
Kozen, D.: Lower bounds for natural proof systems. In: Proc. 18th FOCS, pp. 254–266 (1977)
Kupferman, O., Vardi, M.Y.: Verification of fair transition systems. CJTCS 1998(2) (1998)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM TOCL 2(2), 408–429 (2001)
Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. J. STTT 4(2), 224–233 (2003)
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th FOCS, pp. 531–540 (2005)
Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)
Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. TCS 32, 321–330 (1984)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of the tree and its complexity. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 275–283. Springer, Heidelberg (1986)
Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)
Savitch, W.J.: Relationship between nondeterministic and deterministic tape complexities. Journal on Computer and System Sciences 4, 177–192 (1970)
Schuppan, V., Biere, A.: Shortest counterexamples for symbolic model checking of LTL with past. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 493–509. Springer, Heidelberg (2005)
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)
Vardi, M.Y.: Alternating automata and program verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 471–485. Springer, Heidelberg (1995)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I& C 115(1), 1–37 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kupferman, O., Sheinvald-Faragy, S. (2006). Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words. In: Baier, C., Hermanns, H. (eds) CONCUR 2006 – Concurrency Theory. CONCUR 2006. Lecture Notes in Computer Science, vol 4137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817949_33
Download citation
DOI: https://doi.org/10.1007/11817949_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37376-6
Online ISBN: 978-3-540-37377-3
eBook Packages: Computer ScienceComputer Science (R0)