Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
History and Prospects for First-Order Automated Deduction Read chapter Read first chapter

2015 | OriginalPaper | Chapter

Deciding \(\mathsf {ATL^*}\) Satisfiability by Tableaux

Author : Amélie David

Published in: Automated Deduction - CADE-25

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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/​.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter A Decision Procedure for (Co)datatypes in SMT Solvers
next chapter A Formalisation of Finite Automata Using Hereditarily Finite Sets
Literature
1.
2.
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
3.
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)
4.
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)
5.
6.
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)MathSciNetCrossRefMATH
7.
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
8.
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) CrossRef
Metadata
Title
Deciding Satisfiability by Tableaux
Author
Amélie David
Copyright Year
2015
Book
Automated Deduction - CADE-25

Print ISBN: 978-3-319-21400-9

Electronic ISBN: 978-3-319-21401-6

Copyright Year: 2015

DOI
https://doi.org/10.1007/978-3-319-21401-6_14

Premium Partner

    Image Credits