Document Open Access Logo

Results on Alternating-Time Temporal Logics with Linear Past

Authors Laura Bozzelli, Aniello Murano, Loredana Sorrentino

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2018.6.pdf
  • Filesize: 0.59 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • Alternating-time temporal logics
  • Linear Past
  • Model Checking

Metrics

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

Abstract

We investigate the succinctness gap between two known equally-expressive and different linear-past extensions of standard CTL^* (resp., ATL^*). We establish by formal non-trivial arguments that the "memoryful" linear-past extension (the history leading to the current state is taken into account) can be exponentially more succinct than the standard "local" linear-past extension (the history leading to the current state is forgotten). As a second contribution, we consider the ATL-like fragment, denoted ATL_{lp}, of the known "memoryful" linear-past extension of ATL^{*}. We show that ATL_{lp} is strictly more expressive than ATL, and interestingly, it can be exponentially more succinct than the more expressive logic ATL^{*}. Moreover, we prove that both satisfiability and model-checking for the logic ATL_{lp} are Exptime-complete.

Cite As Get BibTex

Laura Bozzelli, Aniello Murano, and Loredana Sorrentino. Results on Alternating-Time Temporal Logics with Linear Past. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TIME.2018.6

Author Details

Laura Bozzelli
  • University of Napoli "Federico II", Italy
Aniello Murano
  • University of Napoli "Federico II", Italy
Loredana Sorrentino
  • University of Napoli "Federico II", Italy

References

  1. T. Ågotnes, V. Goranko, and W. Jamroga. Alternating-time temporal logics with irrevocable strategies. In TARK'07, pages 15-24, 2007. Google Scholar
  2. R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002. Google Scholar
  3. C. Baier and J.P. Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  4. L. Bozzelli. The complexity of CTL* + linear past. In FOSSACS'08, LNCS 4962, pages 186-200. Springer, 2008. Google Scholar
  5. L. Bozzelli and A. Murano. On the complexity of ATL and ATL* module checking. In GandALF'17, EPTCS 256, pages 268-282, 2017. Google Scholar
  6. T. Brihaye, A. Da Costa Lopes, F. Laroussinie, and N. Markey. ATL with strategy contexts and bounded memory. In LFCS'09, LNCS 5407, pages 92-106. Springer, 2009. Google Scholar
  7. N. Bulling, W. Jamroga, and M. Popovici. Agents with truly perfect recall in alternating-time temporal logic. In AAMAS'14, pages 1561-1562. IFAAMAS/ACM, 2014. Google Scholar
  8. A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114-133, 1981. Google Scholar
  9. K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic. Inf. Comput., 208(6):677-693, 2010. Google Scholar
  10. E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of Workshop on Logic of Programs, LNCS 131, pages 52-71. Springer-Verlag, 1981. Google Scholar
  11. E.A. Emerson and J.Y. Halpern. "Sometimes" and "Not Never" revisited: on branching versus linear time temporal logic. Journal of the ACM, 33(1):151-178, 1986. Google Scholar
  12. D. M. Gabbay. The declarative past and imperative future: Executable temporal logic for interactive systems. In Temporal Logic in Specification, LNCS 398, pages 409-448. Springer, 1987. Google Scholar
  13. D.P. Guelev, C. Dima, and C. Enea. An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking. Journal of Applied Non-Classical Logics, 21(1):93-131, 2011. Google Scholar
  14. Th. Hafer and W. Thomas. Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In Proc. 14th ICALP, LNCS 267, pages 269-279. Springer, 1987. Google Scholar
  15. W. Jamroga and A. Murano. Module checking of strategic ability. In AAMAS'15, pages 227-235. ACM, 2015. Google Scholar
  16. D. Janin and I. Walukiewicz. Automata for the modal mu-calculus and related results. In MFCS'95, LNCS 969, pages 552-562. Springer, 1995. Google Scholar
  17. O. Kupferman and A. Pnueli. Once and For All. In LICS'95, pages 25-35. IEEE Comp. Soc. Press, 1995. Google Scholar
  18. O. Kupferman, A. Pnueli, and M. Y. Vardi. Once and for all. J. Comput. Syst. Sci., 78(3):981-996, 2012. Google Scholar
  19. O. Kupferman and M. Y. Vardi. Weak alternating automata and tree automata emptiness. In STOC'98, pages 224-233. ACM, 1998. Google Scholar
  20. O. Kupferman and M.Y. Vardi. Module checking. In CAV'96, LNCS 1102, pages 75-86. Springer, 1996. Google Scholar
  21. O. Kupferman, M.Y. Vardi, and P. Wolper. An Automata-Theoretic Approach to Branching-Time Model Checking. Journal of the ACM, 47(2):312-360, 2000. Google Scholar
  22. F. Laroussinie, N. Markey, and P. Schnoebelen. Temporal logic with forgettable past. In LICS'02, pages 383-392. IEEE Computer Society, 2002. Google Scholar
  23. F. Laroussinie and P. Schnoebelen. A hierarchy of temporal logics with past. Theor. Comput. Sci., 148(2):303-324, 1995. Google Scholar
  24. F. Laroussinie and P. Schnoebelen. Specification in CTL+past for verification in CTL. Inf. Comput., 156(1-2):236-263, 2000. Google Scholar
  25. F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log., 15(4):34:1-34:47, 2014. Google Scholar
  26. F. Mogavero, A. Murano, and M.Y. Vardi. Relentful strategic reasoning in alternating-time temporal logic. J. Log. Comput., 26(5):1663-1695, 2016. Google Scholar
  27. A. Pnueli. The temporal logic of programs. In FOCS'77, pages 46-57. IEEE, 1977. Google Scholar
  28. S. Schewe. ATL* Satisfiability is 2EXPTIME-complete. In ICALP'08, LNCS 5126, pages 373-385. Springer, 2008. Google Scholar
  29. S. Schewe and B. Finkbeiner. Satisfiability and finite model property for the alternating-time mu-calculus. In CSL'06, LNCS 4207, pages 591-605. Springer, 2006. Google Scholar
  30. R. S. Streett. Propositional dynamic logic of looping and converse. In STOC'81, pages 375-383. ACM, 1981. Google Scholar
  31. M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Inf. Comput., 115(1):1-37, 1994. Google Scholar
  32. M.Y. Vardi. A temporal fixpoint calculus. In POPL'88, pages 250-259. ACM, 1988. Google Scholar
  33. M.Y. Vardi. Reasoning about the past with two-way automata. In ICALP'98, LNCS 1443, pages 628-641. Springer, 1998. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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