Skip to main content
SpringerLink
Log in

Reasoning About Reversal-Bounded Counter Machines

  • Chapter
  • First Online:
Ewa Orłowska on Relational Methods in Logic and Computer Science

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 17))

  • 226 Accesses

Abstract

In this paper, we present a short survey on reversal-bounded counter machines. It focuses on the main techniques for model-checking such counter machines with specifications expressed with formulae from some linear-time temporal logic. All the decision procedures are designed by translation into Presburger arithmetic. We provide a proof that is alternative to Ibarra’s original one for showing that reachability sets are effectively definable in Presburger arithmetic. Extensions to repeated control state reachability and to additional temporal properties are discussed in the paper. The article is written to the honor of Professor Ewa Orłowska and focuses on several topics that are developed in her works.

To the honor of Professor Ewa Orłowska

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 119.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 159.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  • Atig, M. F. (2010). Global model checking of ordered multi-pushdown systems. In K. Lodaya & M. Mahajan (Eds.), IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010 (Vol. 8, pp. 216–227). LIPIcs. Chennai: Schloss Dagstuhl - Leibniz- Zentrum für Informatik.

    Google Scholar 

  • Baker, B. S. & Book, R. V. (1974). Reversal-bounded multipushdown machines. Journal of Computer and System Sciences, 8(3), 315–332.

    Article  Google Scholar 

  • Balbiani, P. & Orłowska, E. (1999). A hierarchy of modal logics with relative accessibility relations. Journal of Applied Non-Classical Logics: Special Issue in the Memory of George Gargov, 9(2–3), 303–328.

    Article  Google Scholar 

  • Berman, L. (1980). The complexity of logical theories. Theoretical Computer Science, 11, 71–77.

    Article  Google Scholar 

  • Bersani, M. M. & Demri, S. (2011). The complexity of reversal-bounded model-checking. In C. Tinelli & V. Sofronie-Stokkermans (Eds.), Proceedings of Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011 (Vol. 6989, pp. 71–86). Lecture Notes in Computer Science. Saarbrücken, Germany.

    Google Scholar 

  • Biere, A., Cimatti, A., Clarke, E. M., Strichman, O., & Zhu, Y. (2003). Bounded model checking. Advances in Computers, 58, 117–148.

    Article  Google Scholar 

  • Blattner, M. & Latteux, M. (1981). Parikh-bounded languages. In S. Even & O. Kariv (Eds.), Proceedings of Automata, Languages and Programming, 8th Colloquium (Vol. 115, pp. 316–323). Lecture Notes in Computer Science. Acre: Springer.

    Chapter  Google Scholar 

  • Borosh, I. & Treybig, L. B. (1976). Bounds on positive integral solutions of linear Diophantine equations. Proceedings of the American Mathematical Society, 55(2), 299–304.

    Article  Google Scholar 

  • Boigelot, B. (1999). Symbolic Methods for Exploring Infinite State Spaces, Doctoral dissertation, Université de Liège.

    Google Scholar 

  • Bojańczyk, M. & Lasota, S. (2010). An extension of data automata that captures XPath. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010 (pp. 243–252). Edinburgh: IEEE Computer Society.

    Google Scholar 

  • Bouajjani, A., Echahed, R., & Habermehl, P. (1995). On the verification problem of nonregular properties for nonregular processes. Proceedings, 10th annual IEEE symposium on logic in computer science (pp. 123–133). San Diego: IEEE Computer Society.

    Google Scholar 

  • Bozga, M., Iosif, R., & Konecný, F. (2010). Fast acceleration of ultimately periodic relations. In T. Touili, B. Cook, & P. B. Jackson (Eds.), 22nd International Conference, CAV 2010 Proceedings of Computer Aided Verification, (Vol. 6174, pp. 227–242). Lecture Notes in Computer Science. Edinburgh: Springer.

    Google Scholar 

  • Bresolin, D., Golińska-Pilarek, J., & Orłowska, E. (2006). A relational dual tableaux for interval temporal logics. Journal of Applied Non-classical Logics, 16(3–4), 251–277.

    Article  Google Scholar 

  • Bruyère, V., Dall’Olio, E., & Raskin, J.-F. (2003). Durations, parametric modelchecking in timed automata with presburger arithmetic. In H. Alt & M. Habib (Eds.), Proceedings of STACS 2003, 20th Annual Symposium on Theoretical Aspects of Computer Science (Vol. 2607, pp. 687–698). Lecture Notes in Computer Science. Berlin: Springer.

    Google Scholar 

  • Cadilhac, M., Finkel, A., & McKenzie, P. (2011). On the expressiveness of Parikh automata and related models. In R. Freund, M. Holzer, C. Mereghetti, F. Otto, & B. Palano (Eds.), Proceedings of the 3rd Workshop on Non-classical Models of Automata and Applications (NCMA’11) (Vol. 282, pp. 103–119). Austrian Computer Society.

    Google Scholar 

  • Čerāns, K. (1994). Deciding properties of integral relational automata. In S. Abiteboul & E. Shamir (Eds.), Proceedings of Automata, Languages and Programming, 21st International Colloquium, ICALP’94 (Vol. 820, pp. 35–46). Lecture Notes in Computer Science. Jerusalem: Springer.

    Chapter  Google Scholar 

  • Chan, T.-h. (1981). Reversal complexity of counter machines. In Proceedings of the 13th Annual ACM Symposium on Theory of Computing (pp. 146–157). Milwaukee: ACM.

    Google Scholar 

  • Comon, H. & Cortier, V. (2000). Flatness is not a weakness. In P. Clote & H. Schwichtenberg (Eds.), Proceedings of 14th Annual Conference of the Computer Science Logic, EACSL (Vol. 1862, pp. 262–276). Lecture Notes in Computer Science. Fischbachau: Springer.

    Google Scholar 

  • Comon, H. & Jurski, Y. (1998). Multiple counter automata, safety analysis and Presburger arithmetic. In A. J. Hu & M. Y. Vardi (Eds.), Proceedings of the 10th International Conference Computer Aided Verification, CAV’98 (Vol. 1427, pp. 268–279). Lecture Notes in Computer Science. Vancouver: Springer.

    Google Scholar 

  • Czerwiński, W., Hofman, P., & Lasota, S. (2013). Reachability problem for weak multi-pushdown automata. Logical Methods in Computer Science, 9(3).

    Google Scholar 

  • Dang, Z., Ibarra, O. H., Bultan, T., Kemmerer, R. A., & Su, J. (2000). Binary reachability analysis of discrete pushdown timed automata. In E. A. Emerson & A. P. Sistla (Eds.), Proceedings of the 12th International Conference of the Computer Aided Verification, CAV 2000 (Vol. 1855, pp. 69–84). Lecture Notes in Computer Science. Chicago: Springer.

    Chapter  Google Scholar 

  • Dang, Z., Ibarra, O. H., & Pietro, P. S. (2001). Liveness verification of reversal-bounded multicounter machines with a free counter. In R. Hariharan, M. Mukund, & V. Vinay (Eds.), Proceedings of FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 21st Conference (Vol. 2245, pp. 132–143). Lecture Notes in Computer Science. Bangalore: Springer.

    Chapter  Google Scholar 

  • Dang, Z., Pietro, P. S., & Kemmerer, R. A. (2003). Presburger liveness verification of discrete timed automata. Theoretical Computer Science, 299(1–3), 413–438.

    Article  Google Scholar 

  • Demri, S. (2006). Linear-time temporal logics with Presburger constraints: An overview. Journal of Applied Non-Classical Logics, 16(3–4), 311–348.

    Article  Google Scholar 

  • Demri, S., Dhar, A. K., & Sangnier, A. (2013). On the complexity of verifying regular properties on flat counter systems, In F. V. Fomin, R. Freivalds, M. Z. Kwiatkowska, & D. Peleg (Eds.), Proceedings of Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, part II (Vol. 7966, pp. 162–173). Lecture Notes in Computer Science. Riga: Springer.

    Chapter  Google Scholar 

  • Demri, S., Dhar, A. K., & Sangnier, A. (2015). Taming past LTL and flat counter systems. Information and Computation, 242, 306–339.

    Article  Google Scholar 

  • Demri, S., Figueira, D., & Praveen, M. (2016). Reasoning about data repetitions with counter systems. Logical Methods in Computer Science, 12(3).

    Google Scholar 

  • Demri, S., Goranko, V., & Lange, M. (2016). Temporal Logics in Computer Science: Finite-state Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge: Cambridge University Press.

    Google Scholar 

  • Demri, S. & Sangnier, A. (2010). When model-checking freeze LTL over counter machines becomes decidable. In C.-H. L. Ong (Ed.), Proceedings of Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010 (Vol. 6014, pp. 176–190). Lecture Notes in Computer Science. Paphos: Springer.

    Chapter  Google Scholar 

  • Esparza, J. (1994). On the decidability of model checking for several \(\mu \)-calculi and Petri nets. In S. Tison (Ed.), Proceedings of Trees in Algebra and Programming –CAAP’94, 19th International Colloquium (Vol. 787, pp. 115–129). Lecture Notes in Computer Science. Edinburgh: Springer.

    Google Scholar 

  • Esparza, J. (1996). Decidability and complexity of Petri net problems – an introduction. In W. Reisig & G. Rozenberg (Eds.), Lectures on Petri nets I: Basic models, advances in Petri nets (Vol. 1491, pp. 374–428). Lecture Notes in Computer Science. The volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996. Berlin: Springer.

    Chapter  Google Scholar 

  • Esparza, J. & Ganty, P. (2011). Complexity of pattern-based verification for multithreaded programs. In T. Ball & M. Sagiv (Eds.), Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011 (pp. 499–510). Austin: ACM.

    Google Scholar 

  • Fariñas del Cerro, L. & Orłowska, E. (1985). DAL – a logic for data analysis. Theoretical Computer Science, 36, 251–264. Corrigendum: ibid. Fariñas del Cerro and Orłowska (1986).

    Article  Google Scholar 

  • Fariñas del Cerro, L. & Orłowska, E. (1986). DAL – a logic for data analysis: Corrigendum. Theoretical Computer Science, 47, 345.

    Google Scholar 

  • Finkel, A., Iyer, S. P., & Sutre, G. (2003). Well-abstracted transition systems: Application to FIFO automata. Information and Computation, 181(1), 1–31.

    Article  Google Scholar 

  • Finkel, A. & Leroux, J. (2002). How to compose Presburger-accelerations: Applications to broadcast protocols. In M. Agrawal & A. Seth (Eds.), Proceedings of FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 22nd conference (Vol. 2556, pp. 145–156). Lecture Notes in Computer Science. Kanpur: Springer.

    Chapter  Google Scholar 

  • Finkel, A. & Sangnier, A. (2008). Reversal-bounded counter machines revisited. In E. Ochmański & J. Tyszkiewicz (Eds.), Proceedings of the 33rd International Symposium of the Mathematical Foundations of Computer Science 2008, MFCS 2008 (Vol. 5162, pp. 323–334). Lecture Notes in Computer Science. Toruń: Springer.

    Google Scholar 

  • Fribourg, L. (2000). Petri nets, flat languages and linear arithmetic. In M. Alpuente (Ed.), 9th International Workshop on Functional and Logic Programming, WFLP’00 (pp. 344–365). Spain: Benicassim.

    Google Scholar 

  • Fribourg, L. & Olsén, H. (1997). Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In A. W. Mazurkiewicz & J. Winkowski (Eds.), Proceedings of the 8th International Conference the CONCUR ’97: Concurrency Theory, (Vol. 1243, pp. 213–227). Lecture Notes in Computer Science. Warsaw: Springer.

    Chapter  Google Scholar 

  • Ginsburg, S. & Spanier, E. (1966). Semigroups, Presburger formulas and languages. Pacific Journal of Mathematics, 16(2), 285–296.

    Article  Google Scholar 

  • Gurari, E. M. & Ibarra, O. H. (1981). The complexity of decision problems for finite-turn multicounter machines. In S. Even & O. Kariv (Eds.), Proceedings of Automata, Languages and Programming, 8th Colloquium (Vol. 115, pp. 495–505). Lecture Notes in Computer Science. Acre (Akko): Springer.

    Chapter  Google Scholar 

  • Haase, C. (2014). Subclasses of Presburger arithmetic and the weak EXP hierarchy. In T. A. Henzinger & D. Miller (Eds.), Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (lics), CSL-LICS ’14 (pp. 47:1–47:10). Vienna: ACM.

    Google Scholar 

  • Haase, C. & Halfon, S. (2014). Integer vector addition systems with states. In J. Ouaknine, I. Potapov, & J. Worrell (Eds.), Proceedings of Reachability Problems – 8th International Workshop, RP 2014 (Vol. 8762, pp. 112–124). Lecture Notes in Computer Science. Oxford: Springer.

    Google Scholar 

  • Habermehl, P. (1997). On the complexity of the linear-time \(\mu \) -calculus for Petri nets. In P. Azéma & G. Balbo (Eds.), Proceedings of Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN ’97 (Vol. 1248, pp. 102–116). Lecture Notes in Computer Science. Toulouse: Springer.

    Google Scholar 

  • Hague, M. & Lin, A. W. (2011). Model checking recursive programs with numeric data types. In G. Gopalakrishnan & S. Qadeer (Eds.), Proceedings of Computer Aided Verification –23rd International Conference, CAV 2011 (Vol. 6806, pp. 743–759). Lecture Notes in Computer Science. Snowbird: Springer.

    Google Scholar 

  • Howell, R. R. & Rosier, L. E. (1987). An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines. Journal of Computer and System Sciences, 34(1), 55–74.

    Article  Google Scholar 

  • Howell, R. R. & Rosier, L. E. (1989). Problems concerning fairness and temporal logic for conflict-free Petri nets. Theoretical Computer Science, 64(3), 305–329.

    Article  Google Scholar 

  • Ibarra, O. H. (1974). A note on semilinear sets and bounded-reversal multihead pushdown automata. Information Processing Letters, 3(1), 25–28.

    Article  Google Scholar 

  • Ibarra, O. H. (1978). Reversal-bounded multicounter machines and their decision problems. Journal of the ACM, 25(1), 116–133.

    Article  Google Scholar 

  • Ibarra, O. H., Su, J., Dang, Z., Bultan, T., & Kemmerer, R. A. (2002). Counter machines and verification problems. Theoretical Computer Science, 289(1), 165–189.

    Article  Google Scholar 

  • Jančar, P. (1990). Decidability of a temporal logic problem for Petri nets. Theoretical Computer Science, 74(1), 71–93.

    Article  Google Scholar 

  • Karp, R. M. & Miller, R. E. (1969). Parallel program schemata. Journal of Computer and System Sciences, 3(2), 147–195.

    Article  Google Scholar 

  • Klaedtke, F. & Rueß, H. (2002). Parikh automata and monadic second-order logics with linear cardinality constraints. Technical report No. 177, Institute of Computer Science at Freiburg University.

    Google Scholar 

  • Kopczyński, E. & Widjaja To, A. (2010). Parikh images of grammars: Complexity and applications. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010 (pp. 80–89). Edinburgh: IEEE Computer Society.

    Google Scholar 

  • Kosaraju, S. R. (1982). Decidability of reachability in vector addition systems (preliminary version). In H. R. Lewis, B. B. Simons, W. A. Burkhard, & L. H. Landweber (Eds.), Proceedings of the 14th Annual ACM Symposium on Theory of Computing (pp. 267–281). San Francisco: ACM.

    Google Scholar 

  • La Torre, S., Madhusudan, P., & Parlato, G. (2007). A robust class of context-sensitive languages. In Proceedings of the 22nd IEEE Symposium on Logic in Computer Science, LICS 2007 (pp. 161–170). Wrocław: IEEE Computer Society.

    Google Scholar 

  • Laroussinie, F., Meyer, A., & Petonnet, E. (2010). Counting LTL. In N. Markey & J. Wijsen (Eds.), TIME 2010–17th International Symposium on Temporal Representation and Reasoning (pp. 51–58). Paris France: IEEE Computer Society.

    Google Scholar 

  • Leroux, J. (2009). The general vector addition system reachability problem by Presburger inductive invariants. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009 (pp. 4–13). Los Angeles: IEEE Computer Society.

    Google Scholar 

  • Leroux, J. & Schmitz, S. (2015). Demystifying reachability in vector addition systems. 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015 (pp. 56–67). Kyoto: IEEE Computer Society.

    Google Scholar 

  • Lipton, R. J. (1976). The reachability problem requires exponential space. Technical report No. 62, Department of Computer Science, Yale University.

    Google Scholar 

  • Manna, Z. & Pnueli, A. (1995). Temporal Verification of Reactive Systems – Safety. Berlin: Springer.

    Chapter  Google Scholar 

  • Mayr, E. W. (1984). An algorithm for the general Petri net reachability problem. SIAM Journal on Computing, 13(3), 441–460.

    Article  Google Scholar 

  • Minsky, M. (1961). Recursive unsolvability of Post’s problems of ’tag’ and other topics in theory of Turing machines. Annals of Mathematics, 74(3), 437–455.

    Article  Google Scholar 

  • Minsky, M. (1967). Computation, Finite and Infinite Machines. Prentice: Prentice Hall.

    Google Scholar 

  • Orłowska, E. (1973). Theorem Proving Systems., Dissertationes Mathematicae CIII Warsaw: Polish Scientific Publishers.

    Google Scholar 

  • Orłowska, E. (1985). Logic of nondeterministic information. Studia Logica, 44(1), 91–100.

    Article  Google Scholar 

  • Orłowska, E. (1988). Relational interpretation of modal logics. In H. Andreka, D. Monk, & I. Németi (Eds.), Algebraic Logic. Colloquia Mathematica Societatis Janos Bolyai (Vol. 54, pp. 443–471). Amsterdam: North Holland.

    Google Scholar 

  • Orłowska, E. (1989). Logic for reasoning about knowledge. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 35, 559–572.

    Article  Google Scholar 

  • Orłowska, E. (1993). Dynamic logic with program specifications and its relational proof system. Journal of Applied Non-Classical Logics, 3, 147–171.

    Article  Google Scholar 

  • Orłowska, E. (1995). Temporal logics in a relational framework. In L. Bolc & A. Szałas (Eds.), Time and Logic: a Computational Approach (pp. 249–277). University College London Press.

    Google Scholar 

  • Papadimitriou, C. H. (1981). On the complexity of integer programming. Journal of the ACM, 28(4), 765–768.

    Article  Google Scholar 

  • Parikh, R. (1966). On context-free languages. Journal of the ACM, 13(4), 570–581.

    Article  Google Scholar 

  • Pnueli, A. (1977). The temporal logic of programs. 18th Annual Symposium on Foundations of Computer Science (pp. 46–57). Providence: IEEE Computer Society.

    Google Scholar 

  • Presburger, M. (1929). Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes rendus du premier congrès de mathématiciens des pays slaves (pp. 92–101). Warsaw, Poland.

    Google Scholar 

  • Qadeer, S. & Rehof, J. (2005). Context-bounded model checking of concurrent software. In N. Halbwachs & L. D. Zuck (Eds.), Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 (Vol. 3440, pp. 93–107). Lecture Notes in Computer Science. Edinburgh: Springer.

    Chapter  Google Scholar 

  • Rackoff, C. (1978). The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6, 223–231.

    Article  Google Scholar 

  • Reutenauer, C. (1990). The Mathematics of Petri Nets. Masson and Prentice.

    Google Scholar 

  • Sangnier, A. (2008). Vérification de systèmes avec compteurs et pointeurs, Doctoral dissertation, LSV, ENS Cachan, France.

    Google Scholar 

  • Savitch, W. J. (1970). Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4(2), 177–192.

    Article  Google Scholar 

  • Schrijver, A. (1986). Theory of Linear and Integer Programming. New York: Wiley

    Google Scholar 

  • Suzuki, N. & Jefferson, D. (1980). Verification decidability of Presburger array programs. Journal of the ACM, 27(1), 191–205.

    Article  Google Scholar 

  • Widjaja To, A. (2010). Model Checking Infinite-state Systems: Generic and Specific Approaches, Doctoral dissertation. School of Informatics, University of Edinburgh.

    Google Scholar 

Download references

Acknowledgements

I would like to thank the anonymous reviewers for their suggestions and remarks that help me improve the quality of the document.

Author information

Authors and Affiliations

  1. LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay, 61, avenue du Président Wilson, 94235, Cachan Cedex, France

    Stéphane Demri

Authors
  1. Stéphane Demri
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stéphane Demri .

Editor information

Editors and Affiliations

  1. Institute of Philosophy, University of Warsaw, Warsaw, Poland

    Joanna Golińska-Pilarek

  2. Department of Logic and Methodology of Science, University of Lodz, Łódź, Poland

    Michał Zawidzki

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Demri, S. (2018). Reasoning About Reversal-Bounded Counter Machines. In: Golińska-Pilarek, J., Zawidzki, M. (eds) Ewa Orłowska on Relational Methods in Logic and Computer Science. Outstanding Contributions to Logic, vol 17. Springer, Cham. https://doi.org/10.1007/978-3-319-97879-6_17

Download citation

Publish with us

Policies and ethics

Search

Navigation