Abstract
We propose a tableau-based decision procedure for the full Alternating-time Temporal Logic \(\mathsf {ATL^*}\). We extend our procedure for \(\mathsf {ATL^{+}}\) in order to deal with nesting of temporal operators. As a side effect, we obtain a new and conceptually simple tableau method for \(\mathsf {CTL^*}\). The worst case complexity of our procedure is \(\mathrm {3EXPTIME} \), which is suboptimal compared to the \(\mathrm {2EXPTIME} \) complexity of the problem. However our method is human-readable and easily implementable. A web application and binaries for our procedure are available at http://atila.ibisc.univ-evry.fr/tableau_ATL_star/.
All proofs of lemmas, propositions and theorems, as well as complete examples can be found in the version with appendices at https://www.ibisc.univ-evry.fr/~adavid/fichiers/cade15_tableaux_atl_star_long.pdf.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)
Cerrito, S., David, A., Goranko, V.: Optimal tableaux-based decision procedure for testing satisfiability in the alternating-time temporal logic ATL+. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 277–291. Springer, Heidelberg (2014). http://arxiv.org/abs/1407.4645
Carral, D., Feier, C., Cuenca Grau, B., Hitzler, P., Horrocks, I.: \(\cal EL\)-ifying ontologies. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 464–479. Springer, Heidelberg (2014)
Emerson, E.A.: Temporal and modal logics. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. MIT Press (1990)
Emerson, E.A., Sistla, A.P.: Deciding full branching time logic. Inf. Control 61(3), 175–201 (1984)
Goranko, V., Shkatov, D.: Tableau-based decision procedures for logics of strategic ability in multiagent systems. ACM Trans. Comput. Log. 11(1), 1–48 (2009)
Reynolds, M.: A faster tableau for CTL. In: Puppis, G., Villa, T. (eds.) Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2013, Borca di Cadore, Dolomites, Italy, 29–31th August 2013. EPTCS, vol. 119, pp. 50–63 (2013). http://dx.doi.org/10.4204/EPTCS.119.7
Schewe, S.: ATL* satisfiability Is 2EXPTIME-complete. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 373–385. Springer, Heidelberg (2008)
Acknowledgement
I would like to thank Serenella Cerrito and Valentin Goranko for their advices and proofreading. I also thank the anonymous referees for their helpful criticisms.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
David, A. (2015). Deciding \(\mathsf {ATL^*}\) Satisfiability by Tableaux . In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-21401-6_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-21400-9
Online ISBN: 978-3-319-21401-6
eBook Packages: Computer ScienceComputer Science (R0)