Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Verification of Qualitative ℤ Constraints

  • Conference paper
CONCUR 2005 – Concurrency Theory (CONCUR 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3653))

Included in the following conference series:

Abstract

We introduce an LTL-like logic with atomic formulae built over a constraint language interpreting variables in ℤ. The constraint language includes periodicity constraints, comparison constraints of the form x = y and x < y, it is closed under Boolean operations and it admits a restricted form of existential quantification. This is the largest set of qualitative constraints over ℤ known so far, shown to admit a decidable LTL extension. Such constraints are those used for instance in calendar formalisms or in abstractions of counter automata by using congruences modulo some power of two. Indeed, various programming languages perform arithmetic operators modulo some integer. We show that the satisfiability and model-checking problems (with respect to an appropriate class of constraint automata) for this logic are decidable in polynomial space improving significantly known results about its strict fragments. As a by-product, LTL model-checking over integral relational automata is proved complete for polynomial space which contrasts with the known undecidability of its CTL counterpart.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Dill, D.: A theory of timed automata. TCS 126, 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  2. Alur, R., Henzinger, T.: A really temporal logic. JACM 41(1), 181–204 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  3. Balbiani, P., Condotta, J.F.: Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 162–173. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: LICS 1995, pp. 123–133 (1995)

    Google Scholar 

  5. Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)

    Google Scholar 

  6. Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast Acceleration of Symbolic Transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  7. Boigelot, B.: Symbolic methods for exploring infinite state spaces. PhD thesis, Université de Liège (1998)

    Google Scholar 

  8. Caucal, D.: On infinite transition graphs having a decidable monadic theory. TCS 290, 79–115 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  9. Comon, H., Cortier, V.: Flatness is not a weakness. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 262–276. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Čerāns, K.: Deciding properties of integral relational automata. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol. 820, pp. 35–46. Springer, Heidelberg (1994)

    Google Scholar 

  11. Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  12. Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 268–279. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  13. Demri, S., D’Souza, D.: An automata-theoretic approach to constraint LTL. Technical Report LSV-03-11, 40 pages, LSV (August 2003); An extended abstract appeared in Agrawal, M., Seth, A.K. (eds.): FSTTCS 2002. LNCS, vol. 2556. Springer, Heidelberg (2002)

    Google Scholar 

  14. Demri, S.: LTL over integer periodicity constraints. Technical Report LSV-04-6, LSV, 35 pages (February 2004); An extended abstract appeared in Walukiewicz, I. (ed.): FOSSACS 2004. LNCS, vol. 2987. Springer, Heidelberg (2004)

    Google Scholar 

  15. Demri, S., Gascon, R.: Verification of qualitative Z-constraints. Technical Report LSV-05-07, LSV (June 2005)

    Google Scholar 

  16. Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352–359 (1999)

    Google Scholar 

  17. Finkel, A., Leroux, J.: How to compose Presburger accelerations: Applications to broadcast protocols. In: FST&TCS 2002. LNCS, vol. 2256, pp. 145–156. Springer, Heidelberg (2002)

    Google Scholar 

  18. Gastin, P., Kuske, D.: Satisfiability and model checking for MSOdefinable temporal logics are in PSPACE. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 222–236. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  19. Gabelaia, D., Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: On the computational complexity of spatio-temporal logics. In: FLAIRS 2003, pp. 460–464 (2003)

    Google Scholar 

  20. Ibarra, O.: Reversal-bounded multicounter machines and their decision problems. JACM 25(1), 116–133 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  21. Jančar, P., Kučera, A., Moller, F., Sawa, Z.: DP lower bounds for equivalence-checking and model-checking of one-counter automata. I & C 188, 1–19 (2004)

    MATH  Google Scholar 

  22. Dal Lago, U., Montanari, A.: Calendars, time granularities, and automata. In: Jensen, C.S., Schneider, M., Seeger, B., Tsotras, V.J. (eds.) SSTD 2001. LNCS, vol. 2121, pp. 279–298. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  23. Logothetis, G., Schneider, K.: Abstraction from counters: an application on real-time systems. In: TIME 2001, pp. 214–223. IEEE, Los Alamitos (2001)

    Google Scholar 

  24. Lutz, C.: NEXPTIME-complete description logics with concrete domains. ACM Transactions on Computational Logic 5(4), 669–705 (2004)

    Article  MathSciNet  Google Scholar 

  25. Müller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: ESOP 2005, LNCS, Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  26. Safra, S.: Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science (1989)

    Google Scholar 

  27. Sistla, A., Clarke, E.: The complexity of propositional linear temporal logic. JACM 32(3), 733–749 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  28. Toman, D., Chomicki, J.: Datalog with integer periodicity constraints. Journal of Logic Programming 35(3), 263–290 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  29. Vardi, M., Wolper, P.: Reasoning about infinite computations. I & C 115, 1–37 (1994)

    MATH  MathSciNet  Google Scholar 

  30. Wolper, P.: Temporal logic can be more expressive. I & C 56, 72–99 (1983)

    MATH  MathSciNet  Google Scholar 

  31. Wolter, F., Zakharyaschev, M.: Spatio-temporal representation and reasoning based on RCC-8. In: KR 2000, pp. 3–14 (2000)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV/CNRS UMR 8643 & INRIA Futurs projet SECSI & ENS Cachan, 61, av. Pdt. Wilson, 94235, Cachan Cedex, France

    Stéphane Demri & Régis Gascon

Authors
  1. Stéphane Demri
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Régis Gascon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of California, Santa Cruz

    Martín Abadi

  2. University of California, Santa Cruz, USA

    Luca de Alfaro

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Demri, S., Gascon, R. (2005). Verification of Qualitative ℤ Constraints. In: Abadi, M., de Alfaro, L. (eds) CONCUR 2005 – Concurrency Theory. CONCUR 2005. Lecture Notes in Computer Science, vol 3653. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11539452_39

Download citation

  • DOI: https://doi.org/10.1007/11539452_39

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28309-6

  • Online ISBN: 978-3-540-31934-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation