Document Open Access Logo

Constraint Automata on Infinite Data Trees: from CTL(ℤ)/CTL^*(ℤ) to Decision Procedures

Authors Stéphane Demri, Karin Quaas

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.29.pdf
  • Filesize: 0.88 MB
  • 18 pages

Document Identifiers

Author Details

Stéphane Demri
  • Université Paris-Saclay, LMF, CNRS, ENS Paris-Saclay, France
Karin Quaas
  • Fakultät für Mathematik und Informatik, Universität Leipzig, Germany

Cite AsGet BibTex

Stéphane Demri and Karin Quaas. Constraint Automata on Infinite Data Trees: from CTL(ℤ)/CTL^*(ℤ) to Decision Procedures. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.29

Abstract

We introduce the class of tree constraint automata with data values in ℤ (equipped with the less than relation and equality predicates to constants), and we show that the nonemptiness problem is EXPTIME-complete. Using an automata-based approach, we establish that the satisfiability problem for CTL(ℤ) (CTL with constraints in ℤ) is EXPTIME-complete, and the satisfiability problem for CTL^*(ℤ) is 2ExpTime-complete (only decidability was known so far). By-product results with other concrete domains and other logics, are also briefly discussed.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Constraints
  • Constraint Automata
  • Temporal Logics
  • Infinite Data Trees

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. S. Abriola, D. Figueira, and S. Figueira. Logics of repeating values on data trees and branching counter systems. In FoSSaCS'17, volume 10203 of LNCS, pages 196-212, 2017. Google Scholar
  2. E.G. Amparore, S. Donatelli, and F. Gallà. A CTL* model checker for Petri nets. In Petri Nets'20, volume 12152 of LNCS, pages 403-413. Springer, 2020. Google Scholar
  3. F. Baader and J. Rydval. Using model theory to find decidable and tractable description logics with concrete domains. JAR, 66(3):357-407, 2022. Google Scholar
  4. Ph. Balbiani and J.F. Condotta. Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In FroCoS'02, volume 2309 of LNAI, pages 162-173. Springer, 2002. Google Scholar
  5. K. Bartek and M. Lelyk. Modal mu-calculus with atoms. In CSL'17, pages 30:1-30:21. Leibniz-Zentrum für Informatik, LIPICS, 2017. Google Scholar
  6. B. Bednarczyk and O. Fiuk. Presburger Büchi tree automata with applications to logics with expressive counting. In WoLLIC'22, volume 13468 of LNCS, pages 295-308. Springer, 2022. Google Scholar
  7. A. Bhaskar and M. Praveen. Realizability problem for constraint LTL. In TIME'22, volume 247 of LIPIcs, pages 8:1-8:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  8. M. Bojańczyk. A bounding quantifier. In CSL'04, volume 3210 of LNCS, pages 41-55. Springer, 2004. Google Scholar
  9. M. Bojańczyk and Th. Colcombet. Bounds in ω-Regularity. In LiCS'06, pages 285-296. IEEE Computer Society, 2006. Google Scholar
  10. M. Bojańczyk and S. Toruńczyk. Weak MSO+U over infinite trees. In STACS'12, LIPIcs, pages 648-660, 2012. Google Scholar
  11. L. Bozzelli and R. Gascon. Branching-time temporal logic extended with Presburger constraints. In LPAR'06, volume 4246 of LNCS, pages 197-211. Springer, 2006. Google Scholar
  12. L. Bozzelli and S. Pinchinat. Verification of gap-order constraint abstractions of counter systems. TCS, 523:1-36, 2014. Google Scholar
  13. C. Carapelle. On the satisfiability of temporal logics with concrete domains. PhD thesis, Leipzig University, 2015. Google Scholar
  14. C. Carapelle, A. Kartzow, and M. Lohrey. Satisfiability of CTL^* with constraints. In CONCUR'13, LNCS, pages 455-463. Springer, 2013. Google Scholar
  15. C. Carapelle, A. Kartzow, and M. Lohrey. Satisfiability of ECTL^* with constraints. Journal of Computer and System Sciences, 82(5):826-855, 2016. Google Scholar
  16. C. Carapelle and A.-Y. Turhan. Description Logics Reasoning w.r.t. General TBoxes is Decidable for Concrete Domains with the EHD-property. In ECAI'16, volume 285, pages 1440-1448. IOS Press, 2016. Google Scholar
  17. K. Čer̅ans. Deciding properties of integral relational automata. In ICALP'94, volume 820 of LNCS, pages 35-46. Springer, 1994. Google Scholar
  18. A. Chandra, D. Kozen, and L. Stockmeyer. Alternation. JACM, 28(1):114-133, 1981. Google Scholar
  19. R. Condurache, C. Dima, Y. Oualhdaj, and N. Troquard. Rational Synthesis in the Commons with Careless and Careful Agents. In AAMAS'21, pages 368-376, 2021. Google Scholar
  20. B. Cook, H. Khlaaf, and N. Piterman. On automation of CTL* verification for infinite-state systems. In CAV'15, volume 9206 of LNCS, pages 13-29. Springer, 2015. Google Scholar
  21. N. Decker, P. Habermehl, M. Leucker, and D. Thoma. Ordered navigation on multi-attributed data words. In CONCUR'14, volume 8704 of LNCS, pages 497-511, 2014. Google Scholar
  22. S. Demri and M. Deters. Temporal logics on strings with prefix relation. Journal of Logic and Computation, 26:989-1017, 2016. Google Scholar
  23. S. Demri and D. D'Souza. An automata-theoretic approach to constraint LTL. I & C, 205(3):380-415, 2007. Google Scholar
  24. S. Demri and R. Gascon. Verification of qualitative ℤ constraints. TCS, 409(1):24-40, 2008. Google Scholar
  25. S. Demri and R. Lazić. LTL with the freeze quantifier and register automata. ACM ToCL, 10(3), 2009. Google Scholar
  26. S. Demri and K. Quaas. Concrete domains in logics: a survey. ACM SIGLOG News, 8(3):6-29, 2021. Google Scholar
  27. S. Demri and K. Quaas. Constraint automata on infinite data trees: From CTL(Z)/CTL*(Z) to decision procedures. CoRR, abs/2302.05327, 2023. URL: https://arxiv.org/abs/2302.05327.
  28. A. Deutsch, R. Hull, and V. Vianu. Automatic verification of database-centric system. SIGMOD Record, 43(3):5-17, 2014. Google Scholar
  29. E.A. Emerson and J. Halpern. "Sometimes" and "Not Never" revisited: on branching versus linear time temporal logic. JACM, 33:151-178, 1986. Google Scholar
  30. E.A. Emerson and C.S. Jutla. The complexity of tree automata and logics of programs. SIAM Journal of Computing, 29(1):132-158, 2000. Google Scholar
  31. E.A. Emerson and P. Sistla. Deciding full branching time logic. Information and Control, 61:175-201, 1984. Google Scholar
  32. L. Exibard, E. Filiot, and A. Khalimov. Church synthesis on register automata over linearly ordered data domains. In STACS'21, volume 187 of LIPIcs, pages 28:1-28:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  33. L. Exibard, E. Filiot, and A. Khalimov. A generic solution to register-bounded synthesis with an application to discrete orders. In ICALP'22, volume 229 of LIPIcs, pages 122:1-122:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  34. P. Felli, M. Montali, and S. Winkler. CTL* model checking for data-aware dynamic systems with arithmetic. In IJCAR'22, volume 13385 of LNCS, pages 36-56. Springer, 2022. Google Scholar
  35. P. Felli, M. Montali, and S. Winkler. Linear-time verification of data-aware dynamic systems with arithmetic. In AAAI'22, pages 5642-5650. AAAI Press, 2022. Google Scholar
  36. D. Figueira. Reasoning on words and trees with data. PhD thesis, ENS Cachan, 2010. Google Scholar
  37. D. Figueira. Decidability of Downward XPath. ACM ToCL, 13(4):1-40, 2012. Google Scholar
  38. R. Gascon. An automata-based approach for CTL* with constraints. Electronic Notes in Theoretical Computer Science, 239:193-211, 2009. Google Scholar
  39. S. Göller, Ch. Haase, J. Ouaknine, and J. Worrell. Branching-time model checking of parametric one-counter automata. In FoSSaCS'12, volume 7213 of LNCS, pages 406-420. Springer, 2012. Google Scholar
  40. J.F. Groote and R. Mastescu. Verification of temporal properties of processes in a setting with data. In AMAST'98, volume 1548 of LNCS, pages 74-90, 1998. Google Scholar
  41. R. Iosif and X. Xu. Alternating automata modulo first order theories. In CAV'19, volume 11562 of LNCS, pages 46-63, 2019. Google Scholar
  42. M. Jurdziński and R. Lazić. Alternating automata on data trees and XPath satisfiability. ACM ToCL, 12(3):19:1-19:21, 2011. Google Scholar
  43. A. Kartzow and Th. Weidner. Model checking constraint LTL over trees. CoRR, abs/1504.06105, 2015. URL: https://arxiv.org/abs/1504.06105.
  44. O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. JACM, 47(2):312-360, 2000. Google Scholar
  45. N. Labai. Automata-based reasoning for decidable logics with data values. PhD thesis, TU Wien, May 2021. Google Scholar
  46. N. Labai, M. Ortiz, and M. Simkus. An Exptime Upper Bound for ALC with integers. In KR'20, pages 425-436. Morgan Kaufman, 2020. Google Scholar
  47. S. Lasota and I. Walukiewicz. Alternating timed automata. ACM ToCL, 9(2):10:1-10:27, 2008. Google Scholar
  48. A. Lechner, R. Mayr, J. Ouaknine, A. Pouly, and J. Worrell. Model checking flat freeze LTL on one-counter automata. Logical Methods in Computer Science, 14(4), 2018. Google Scholar
  49. C. Lutz. Interval-based temporal reasoning with general TBoxes. In IJCAI'01, pages 89-94. Morgan-Kaufmann, 2001. Google Scholar
  50. C. Lutz. The Complexity of Description Logics with Concrete Domains. PhD thesis, RWTH, Aachen, 2002. Google Scholar
  51. C. Lutz. Description logics with concrete domains - A survey. In Advances in Modal Logics Volume 4, pages 265-296. King’s College Publications, 2003. Google Scholar
  52. C. Lutz. NEXPTIME-complete description logics with concrete domains. ACM ToCL, 5(4):669-705, 2004. Google Scholar
  53. C. Lutz and M. Milicić. A Tableau Algorithm for Description Logics with Concrete Domains and General Tboxes. JAR, 38(1-3):227-259, 2007. Google Scholar
  54. R. Mayr and P. Totzke. Branching-time model checking gap-order constraint systems. Fundamenta Informaticae, 143(3-4):339-353, 2016. Google Scholar
  55. D. Muller and E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. TCS, 141(1-2):69-107, 1995. Google Scholar
  56. F. Neven, T. Schwentick, and V. Vianu. Finite state machines for strings over infinite alphabets. ACM ToCL, 5(3):403-435, 2004. Google Scholar
  57. D. Peteler and K. Quaas. Deciding Emptiness for Constraint Automata on Strings with the Prefix and Suffix Order. In MFCS'22, volume 241 of LIPIcs, pages 76:1-76:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  58. M.O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the AMS, 141:1-35, 1969. Google Scholar
  59. P. Revesz. Introduction to Constraint Databases. Springer, New York, 2002. Google Scholar
  60. S. Safra. Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science, Rehovot, 1989. Google Scholar
  61. L. Segoufin and S. Toruńczyk. Automata based verification over linearly ordered data domains. In STACS'11, pages 81-92, 2011. Google Scholar
  62. H. Seidl, Th. Schwentick, and A. Muscholl. Counting in trees. In Logic and Automata: History and Perspectives, volume 2 of Texts in Logic and Games, pages 575-612. Amsterdam University Press, 2008. Google Scholar
  63. F. Song and Z. Wu. On temporal logics with data variable quantifications: decidability and complexity. I & C, 251:104-139, 2016. Google Scholar
  64. W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, Volume B, Formal models and semantics, pages 133-191. Elsevier, 1990. Google Scholar
  65. Sz. Torunczyk and Th. Zeume. Register automata with extrema constraints, and an application to two-variable logic. Logical Methods in Computer Science, 18(1), 2022. Google Scholar
  66. M. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In STOC'85, pages 240-251. ACM, 1985. Google Scholar
  67. M. Vardi and Th. Wilke. Automata: from logics to algorithms. In Logic and Automata: History and Perspectives, number 2 in Texts in Logic and Games, pages 629-736. Amsterdam University Press, 2008. Google Scholar
  68. M. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Sciences, 32:183-221, 1986. Google Scholar
  69. M. Vardi and P. Wolper. Reasoning about infinite computations. I & C, 115:1-37, 1994. Google Scholar
  70. S. Vester. On the complexity of model-checking branching and alternating-time temporal logics in one-counter systems. In ATVA'15, volume 9364 of LNCS, pages 361-377. Springer, 2015. Google Scholar
  71. Th. Weidner. Probabilistic Logic, Probabilistic Regular Expressions, and Constraint Temporal Logic. PhD thesis, University of Leipzig, 2016. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact