Skip Navigation



Journal of Logic and Computation Advance Access published online on July 22, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp037
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Demri, S.
Right arrow Articles by Gascon, R.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

The Effects of Bounding Syntactic Resources on Presburger LTL

Stéphane Demri

LSV, ENS Cachan, CNRS, INRIA Saclay, Cachan, France.
E-mail: demri{at}lsv.ens-cachan.fr

Régis Gascon

INRIA, I3S, CNRS, University of Nice Sophia Antipolis, France.
E-mail: rgascon{at}sophia.inria.fr

Received 13 February 2008.

LTL over Presburger constraints is the extension of LTL where the atomic formulae are quantifier-free Presburger formulae having as free variables the counters at different states of the model. This logic is known to admit undecidable satisfiability and model-checking problems. We study decidability and complexity issues for fragments of LTL with Presburger constraints obtained by restricting the syntactic resources of the formulae (the number of variables, the maximal distance between two states for which counters can be compared and, to a smaller extent, the set of Presburger constraints), while preserving the strength of the logical operators. We provide a complete picture refining known results from the literature. We show that model-checking and satisfiability problems for the fragments of LTL with difference constraints restricted to two variables and distance one and to one variable and distance two are highly undecidable, enlarging significantly the class of known undecidable fragments. On the positive side, we prove that the fragment restricted to one variable and to distance one augmented with propositional variables is PSPACE-complete. Since the atomic formulae can state quantitative properties on the counters, this extends some results about model-checking pushdown systems and one-counter automata. In order to establish the PSPACE upper bound, we show that the non-emptiness problem for Büchi one-counter automata taking values in Z and allowing zero tests and sign tests, is only NLOGSPACE-complete. Finally, we establish that model-checking one-counter automata with complete quantifier-free Presburger LTL restricted to one variable is also PSPACE-complete, whereas the satisfiability problem is undecidable.

Keywords: Linear-time temporal logic; Presburger arithmetic; Büchi automaton; one-counter automaton



References

  1. Alur R, Dill D. A theory of timed automata. Theoretical Computer Science (1994) 126:183–235.[CrossRef][Web of Science]
  2. Alur R, Henzinger T. A really temporal logic. Journal of the Association for Computing Machinery (1994) 41:181–204.
  3. Balbiani Ph, Condotta JF. Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In: Proceedings of the 4th International Workshop on Frontiers of Combining Systems (FroCoS’02) (2002) Springer. 162–173. Vol. 2309 of Lecture Notes in Artificial Intelligence.
  4. Balcázar J, Díaz J, Gabarró J. Structural Complexity I (1988) 2nd edn. Springer.
  5. Bardin S, Finkel A, Lozes E, Sangnier A. From pointer systems to counter systems using shape analysis. In: Proceedings of the 5th International Workshop on Automated Verification of Infinite-State Systems (AVIS’06) (2006).
  6. Berstel J, Boasson L. Context-free languages. In: Handbook of Theoretical Computer Science, Volume B, Formal models and semantics (1990) Elsevier. 59–102.
  7. Boigelot B. Symbolic Methods for Exploring Infinite State Spaces (1998) Belgium: Université de Liège. PhD Thesis.
  8. Bouajjani A, Habermehl P. Constrained properties, semilinear sets, and Petri nets. (1996) Springer. 481–497. In Proceedings of the 7th International Conference on Concurrency Theory (CONCUR’96), Vol. 1119 of Lecture Notes in Computer Science.
  9. Bouajjani A, Bozga M, Habermehl P, Iosif R, Moro P, Vojnar T. Programs with lists are counter automata. (2006) Springer. 517–531. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV’06), Vol. 4144 of Lecture Notes in Computer Science.
  10. Bouajjani A, Echahed R, Habermehl P. On the verification problem of nonregular properties for nonregular processes. (1995) IEEE. 123–133. In Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS’95).
  11. Bouajjani A, Esparza J, Maler O. Reachability analysis of pushdown automata: application to model checking. (1997) Springer. 135–150. In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR’97), Vol. 1243 of Lecture Notes in Computer Science.
  12. Bouajjani A, Habermehl P, Mayr R. Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science (2003) 295:85–106.[CrossRef][Web of Science]
  13. Chitic C, Rosu D. On validation of XML streams using finite state machines. In: Proceedings of the 7th International Workshop on the Web and Databases (WebDB’04 (2004) 85–90.
  14. Comon H, Cortier V. Flatness is not a weakness. (2000) Springer. 262–276. In Proceedings of the 8th Annual EACSL Conference on Computer Science Logic (CSL’00), Vol. 1862 of Lecture Notes in Computer Science.
  15. Comon H, Jurski Y. Multiple counters automata, safety analysis and Presburger arithmetic. (1998) Springer. 268–279. In Proceedings of the 10th International Conference on Computer Aided Verification (CAV’98), Vol. 1427 of Lecture Notes in Computer Science.
  16. Clarke E, Grumberg O, Peled D. Model Checking (2000) MIT Press.
  17. Dang Z, San Pietro P, Kemmerer R. Presburger liveness verification of discrete timed automata. Theoretical Computer Science (2003) 299:413–438.[CrossRef][Web of Science]
  18. Demri S, D'Souza D. An automata-theoretic approach to constraint LTL. Information and Computation (2007) 205:380–415.[CrossRef][Web of Science]
  19. Demri S, Gascon R. The effects of bounding syntactic resources on Presburger LTL (extended abstract). (2007) IEEE. 94–104. In Proceedings of the 14th International Symposium on Temporal Representation and Reasoning (TIME’07).
  20. Demri S, Gascon R. Verification of qualitativeZconstraints. Theoretical Computer Science (2008) 409:24–40.[CrossRef][Web of Science]
  21. Demri S, Schnoebelen Ph. The complexity of propositional linear temporal logics in simple cases. Information and Computation (2002) 174:84–103.[CrossRef][Web of Science]
  22. Esparza J, Kucera A, Schwoon S. Model checking LTL with regular valuations for pushdown systems. Information and Computation (2003) 186:355–376.[CrossRef][Web of Science]
  23. Finkel A, Leroux J. How to compose Presburger accelerations: Applications to broadcast protocols. (2002) Springer. 145–156. In Proceedings of the 22nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’02), Vol. 2256 of Lecture Notes in Computer Science.
  24. Finkel A, Willems B, Wolper P. Adirect symbolic approach to model checking pushdown systems (extended abstract). (1997) Elsevier. In Proceedings of the 2nd International Workshop on Verification of Infinite State Systems (INFINITY’97), Vol. 9 of Electronic Notes in Theoretical Computer Science.
  25. Gabbay D, Pnueli A, Shelah S, Stavi J. On the temporal analysis of fairness. (1980) ACM Press. 163–173. In 7th Annual ACM Symposium on Principles of Programming Languages.
  26. Gastin P, Kuske D. Satisfiability and model checking for MSO-definable temporal logics are in PSPACE. (2003) Springer. 222–236. In Proceedings of the 14th International Conference on Concurrency Theory (CONCUR’03), Vol. 2761 of Lecture Notes in Computer Science.
  27. Haase C, Kreutzer S, Ouaknine J, Worrell J. Reachability in succinct and parametric one-counter automata. (2009) Springer. In Proceedings of the 20th International Conference on Concurrency Theory (CONCUR’09), Lecture Notes in Computer Science. To appear.
  28. Halpern J. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. Artificial Intelligence (1995) 75:361–372.[CrossRef][Web of Science]
  29. Ibarra O. Reversal-bounded multicounter machines and their decision problems. Journal of the Association for Computing Machinery (1978) 25:116–133.
  30. Ibarra O, Su J, Dang Z, Bultan T, Kemmerer A. Counter machines: decidable properties and applications to verification problems. (2000) Springer. 426–435. In Proceedings of the 25st International Symposium on Mathematical Foundations of Computer Science (MFCS’00), Vol. 1893 of Lecture Notes in Computer Science.
  31. Jancar P, Kucera A, Moller F, Sawa Z. DP lower bounds for equivalence-checking and model-checking of one-counter automata. Information and Computation (2004) 188:1–19.[CrossRef][Web of Science]
  32. Kucera A. Efficient verification algorithms for one-counter processes. (2000) Springer. 317–328. In Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP’00), Vol. 1853 of Lecture Notes in Computer Science.
  33. Kupferman O, Vardi MY, Wolper P. An automata-theoretic approach to branching-time model checking. Journal of the Association for Computing Machinery (2000) 47:312–360.
  34. Lafourcade P, Lugiez D, Treinen R. Intruder deduction for AC-like equational theories with homomorphisms. In: Research Report LSV-04-16 (2004) France: Laboratoire Spécification et Vérification, ENS Cachan. 69.
  35. Lafourcade P, Lugiez D, Treinen R. Intruder deduction for AC-like equational theories with homomorphisms. (2005) Springer. 308–322. In Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA’05), Vol. 3467 of Lecture Notes in Computer Science.
  36. Laroussinie F, Markey N, Schnoebelen P. Model checking timed automata with one or two clocks. (2004) Springer. 387–401. In Proceedings of the 15th International Conference on Concurrency Theory (CONCUR’04), Vol. 3170 of Lecture Notes in Computer Science.
  37. Lasota S, Walukiewicz I. Alternating timed automata. (2005) Springer. In Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’05), Vol. 3441 of Lecture Notes in Computer Science.
  38. Lutz C. NEXPTIME-complete description logics with concrete domains. ACM Transactions on Computational Logic (2004) 5:669–705.[CrossRef]
  39. Minsky M. Computation, Finite and Infinite Machines (1967) Prentice Hall.
  40. Ouaknine J, Worrell J. On the decidability of metric temporal logic. (2005) IEEE. 188–197. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05).
  41. Rogers H Jr. Theory of Recursive Functions and Effective Computability (1967) McGraw-Hill Book Company.
  42. Rosier L, Yen H-C. A multiparameter analysis of the boundedness problem for vector addition systems. Journal of Computer and System Sciences (1986) 32:105–135.[CrossRef][Web of Science]
  43. Serre O. Parity games played on transition graphs of one-counter processes. (2006) Springer. 337–351. In Proceedings of the 9th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’06), Vol. 3921 of Lecture Notes in Computer Science.
  44. Sistla A, Clarke E. The complexity of propositional linear temporal logic. Journal of the Association for Computing Machinery (1985) 32:733–749.
  45. Vardi M. A temporal fixpoint calculus. (1988) ACM. 250–259. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages (POPL’88).
  46. Vardi M, Wolper P. Reasoning about infinite computations. Information and Computation (1994) 115:1–37.[CrossRef][Web of Science]
  47. Wakatsuki M, Teraguchi K, Tomita E. Polynomial time identification of strict deterministic restricted one-counter automata in some class from positive data. (2004) Springer. 260–272. In Proceedings of the 7th International Colloquium on Grammatical Inference (ICGI’04), Vol. 3264 of Lecture Notes in Artificial Intelligence.
  48. Walukiewicz I. Pushdown processes: games and model-checking. Information and Computation (2001) 164:234–263.[CrossRef][Web of Science]
  49. Wolper P. Temporal logic can be more expressive. Information and Computation (1983) 56:72–99.

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Demri, S.
Right arrow Articles by Gascon, R.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?