Abstract
One-counter processes are pushdown processes over a singleton stack alphabet (plus a stack-bottom symbol). We study the problems of model checking asynchronous products of one-counter processes against 1) first-order logic FO(R) with reachability predicate, 2) the finite variable fragments FO k(R) (k ≥ 2) of FO(R), 3) EF-logic which is a fragment of FO 2(R), and 4) all these logics extended with simple component-wise synchronizing predicates. We give a rather complete picture of their combined, expression, and data complexity. To this end, we show that these problems are poly-time reducible to two syntactic restrictions of Presburger Arithmetic, which are equi-expressive with first-order modulo counting theory of (ℕ, <), for which we give optimal quantifier elimination procedures. In particular, these problems are all shown to be in PSPACE, which is in sharp contrast to the closely related problem of model checking FO(R) over pushdown processes (with one stack) which has nonelementary complexity. Finally, we apply our proof method to give a fixed automatic (and so rational) graph whose modal logic theory has nonelementary complexity, solving a recently posed open question.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bekker, W., Goranko, V.: Symbolic model checking of tense logics on rational Kripke models. To appear in proceedings of ILC 2007 (2007)
Blumensath, A., Grädel, E.: Automatic structures. In: LICS 2000, pp. 51–62 (2000)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Compton, K.J., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. Ann. Pure Appl. Logic 48(1), 1–79 (1990)
Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2), 355–376 (2003)
Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput. 179(2), 279–295 (2002)
Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories, vol. 718. Springer, Heidelberg (1979)
Göller, S., Mayr, R., To, A.W.: On the computational complexity of verifying one-counter processes. To appear in LICS 2009 (2009)
Grohe, M., Schweikardt, N.: The succinctness of first-order logic on linear orders. Logical Methods in Computer Science 1(1) (2005)
Jancar, P., Sawa, Z.: A note on emptiness for alternating finite automata with a one-letter alphabet. Inf. Process. Lett. 104(5), 164–167 (2007)
Jančar, P., Kučera, A., Moller, F., Sawa, Z.: DP lower bounds for equivalence-checking and model-checking of one-counter automata. Inf. Comput. 188(1), 1–19 (2004)
Kozen, D.C.: Theory of Computation. Springer, Heidelberg (2006)
Krentel, M.W.: The complexity of optimization problems. J. Comput. Syst. Sci. 36(3), 490–509 (1988)
Kučera, A.: Efficient verification algorithms for one-counter processes. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 317–328. Springer, Heidelberg (2000)
Libkin, L.: Elements Of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)
Löding, C.: Reachability problems on regular ground tree rewriting graphs. Theory Comput. Syst. 39(2), 347–383 (2006)
Makowsky, J.A.: Algorithmic uses of the Feferman-Vaught Theorem. Ann. Pure Appl. Logic 126(1-3), 159–213 (2004)
Mayr, R.: Decidability of model checking with the temporal logic EF. Theor. Comput. Sci. 256(1-2), 31–62 (2001)
Morvan, C.: On rational graphs. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 252–266. Springer, Heidelberg (2000)
Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci. 37, 51–75 (1985)
Péladeau, P.: Logically defined subsets of N k. Theor. Comput. Sci. 93(2), 169–183 (1992)
Rabinovich, A.: On compositionality and its limitations. ACM Trans. Comput. Logic 8(1), 4 (2007)
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)
Stockmeyer, L.J.: The complexity of decision problems in automata theory and logic. PhD thesis, Department of Electrical Engineering, MIT (1974)
Thomas, W.: Constructing infinite graphs with a decidable MSO-theory. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 113–124. Springer, Heidelberg (2003)
To, A.W., Libkin, L.: Recurrent reachability analysis in regular model checking. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 198–213. Springer, Heidelberg (2008)
Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 127–138. Springer, Heidelberg (2000)
Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234–263 (2001)
Wöhrle, S., Thomas, W.: Model checking synchronized products of infinite transition systems. Logical Methods in Computer Science 3(4) (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
To, A.W. (2009). Model Checking FO(R) over One-Counter Processes and beyond. In: Grädel, E., Kahle, R. (eds) Computer Science Logic. CSL 2009. Lecture Notes in Computer Science, vol 5771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04027-6_35
Download citation
DOI: https://doi.org/10.1007/978-3-642-04027-6_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04026-9
Online ISBN: 978-3-642-04027-6
eBook Packages: Computer ScienceComputer Science (R0)