Abstract
We study the computational complexity of model checking EF logic and modal logic on parametric one-counter automata (POCA). A POCA is a one-counter automaton whose counter updates are either integer values encoded in binary or integer-valued parameters. Given a formula and a configuration of a POCA, the model-checking problem asks whether the formula is true in this configuration for all possible valuations of the parameters. We show that this problem is undecidable for EF logic via reduction from Hilbert’s tenth problem, however for modal logic we prove PSPACE-completeness. Obtaining the PSPACE upper bound involves analysing systems of linear Diophantine inequalities of exponential size that admit solutions of polynomial size. Finally, we show that model checking EF logic on POCA without parameters is PSPACE-complete.
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
Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with Lists are Counter Automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 517–531. Springer, Heidelberg (2006)
Bozga, M., Iosif, R.: On Decidability within the Arithmetic of Addition and Divisibility. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 425–439. Springer, Heidelberg (2005)
Bozga, M., Iosif, R., Lakhnech, Y.: Flat Parametric Counter Automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 577–588. Springer, Heidelberg (2006)
Chitic, C., Rosu, D.: On validation of xml streams using finite state machines. In: Proc. of WebDB, pp. 85–90. ACM, New York (2004)
Comon, H., Jurski, Y.: Multiple Counters Automata, Safety Analysis and Presburger Arithmetic. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)
Göller, S., Haase, C., Ouaknine, J., Worrell, J.: Model Checking Succinct and Parametric One-Counter Automata. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 575–586. Springer, Heidelberg (2010)
Göller, S., Lohrey, M.: Branching-time Model Checking of One-counter Processes. In: Proc. of STACS. LIPIcs, vol. 5, pp. 405–416. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)
Göller, S., Mayr, R., To, A.W.: On the Computational Complexity of Verifying One-Counter Processes. In: Proc. of LICS, pp. 235–244. IEEE Computer Society (2009)
Haase, C., Kreutzer, S., Ouaknine, J., Worrell, J.: Reachability in Succinct and Parametric One-Counter Automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 369–383. Springer, Heidelberg (2009)
Hague, M., Lin, A.W.: Model Checking Recursive Programs with Numeric Data Types. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 743–759. Springer, Heidelberg (2011)
Ibarra, O.H., Dang, Z.: On the solvability of a class of diophantine equations and applications. Theor. Comput. Sci. 352(1), 342–346 (2006)
Ibarra, O.H., Jiang, T., Trân, N., Wang, H.: New decidability results concerning two-way counter machines and applications. In: Lingas, A., Carlsson, S., Karlsson, R. (eds.) ICALP 1993. LNCS, vol. 700, Springer, Heidelberg (1993)
Jančar, P., Kučera, A., Mayr, R.: Deciding bisimulation-like equivalences with finite-state processes. Theor. Comput. Sci. 258(1-2), 409–433 (2001)
Lange, M.: Model checking propositional dynamic logic with all extras. J. Applied Logic 4(1), 39–49 (2006)
Leroux, J., Sutre, G.: Flat Counter Automata Almost Everywhere! In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 489–503. Springer, Heidelberg (2005)
Matiyasevich, Y.: Enumerable sets are Diophantine. Soviet Math. Dokl. 11, 354–357 (1970)
Minsky, M.L.: Recursive unsolvability of Post’s problem of “tag” and other topics in theory of Turing machines. Annals of Mathematics. Second Series 74, 437–455 (1961)
Robinson, J.: Definability and Decision Problems in Arithmetic. J. Symbolic Logic 14(2), 98–114 (1949)
Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Inc., New York (1986)
Serre, O.: Parity Games Played on Transition Graphs of One-Counter Processes. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 337–351. Springer, Heidelberg (2006)
Shallit, J.: The Frobenius Problem and its Generalizations. In: Ito, M., Toyama, M. (eds.) DLT 2008. LNCS, vol. 5257, pp. 72–83. Springer, Heidelberg (2008)
To, A.W.: Model Checking FO(R) over One-Counter Processes and beyond. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 485–499. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Göller, S., Haase, C., Ouaknine, J., Worrell, J. (2012). Branching-Time Model Checking of Parametric One-Counter Automata. In: Birkedal, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2012. Lecture Notes in Computer Science, vol 7213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28729-9_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-28729-9_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28728-2
Online ISBN: 978-3-642-28729-9
eBook Packages: Computer ScienceComputer Science (R0)