Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
A Logical Framework for Developing and Mechanizing Set Theories Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition

verfasst von : Joseph Boudou

Erschienen in: Automated Reasoning

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

PPDL det extends propositional dynamic logic (PDL) with parallel composition of programs. This new construct has separation semantics: to execute the parallel program \((\alpha \,||\,\beta )\) the initial state is separated into two substates and the programs \(\alpha \) and \(\beta \) are executed on these substates. By adapting the elimination of Hintikka sets procedure, we provide a decision procedure for the satisfiability problem of PPDL det. We prove that this decision procedure can be executed in deterministic exponential time, hence that the satisfiability problem of PPDL det is EXPTIME-complete.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Effective Normalization Techniques for HOL
Nächstes Kapitel Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments
Literatur
1.
Abrahamson, K.R.: Modal logic of concurrent nondeterministic programs. In: Kahn, G. (ed.) Semantics of Concurrent Computation. LNCS, vol. 70, pp. 21–33. Springer, Heidelberg (1979)CrossRef
2.
Balbiani, P., Boudou, J.: Tableaux methods for propositional dynamic logics with separating parallel composition. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 539–554. Springer, Switzerland (2015)CrossRef
3.
Balbiani, P., Tinchev, T.: Definability and computability for PRSPDL. In: Goré, R., Kooi, B.P., Kurucz, A. (eds.) Advances in Modal Logic - AiML, pp. 16–33. College Publications, San Diego (2014)
4.
Benevides, M.R.F., de Freitas, R.P., Viana, J.P.: Propositional dynamic logic with storing, recovering and parallel composition. In: Hermann Haeusler, E., Farinas del Cerro, L. (eds.) Logical and Semantic Frameworks, with Applications - LSFA. ENTCS, vol. 269, pp. 95–107 (2011)
5.
Boudou, J.: Exponential-size model property for PDL with separating parallel composition. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 129–140. Springer, Heidelberg (2015)CrossRef
6.
7.
Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108–119. Springer, Heidelberg (2001)CrossRef
8.
Demri, S., Deters, M.: Separation logics and modalities: a survey. J. Appl. Non-Class. Logics 25(1), 50–99 (2015)MathSciNetCrossRef
9.
van Ditmarsch, H., van der Hoek, W., Kooi, B.P.: Dynamic Epistemic Logic, vol. 337. Springer Science & Business Media, Netherlands (2007)CrossRefMATH
10.
van Eijck, J., Stokhof, M.: The gamut of dynamic logics. In: Gabbay, D.M., Woods, J. (eds.) Logic and the Modalities in the Twentieth Century. Handbook of the History of Logic, vol. 7, pp. 499–600. Elsevier, Amsterdam (2006)CrossRef
11.
12.
Frias, M.F.: Fork Algebras in Algebra, Logic and Computer Science. Advances in Logic, vol. 2. World Scientific, Singapore (2002)MATH
13.
Harel, D.: Recurring dominoes: making the highly undecidable highly understandable (preliminary report). In: Karpinski, M. (ed.) FCT. LNCS, vol. 158, pp. 177–194. Springer, Heidelberg (1983)
14.
Herzig, A.: A simple separation logic. In: Libkin, L., Kohlenbach, U., de Queiroz, R. (eds.) WoLLIC 2013. LNCS, vol. 8071, pp. 168–178. Springer, Heidelberg (2013)
15.
Kurucz, Á., Németi, I., Sain, I., Simon, A.: Decidable and undecidable logics with a binary modality. J. Logic, Lang. Inf. 4(3), 191–206 (1995)MathSciNetCrossRefMATH
16.
17.
Lange, M., Lutz, C.: 2-ExpTime lower bounds for propositional dynamic logics with intersection. J. Symbolic Logic 70(4), 1072–1086 (2005)MathSciNetCrossRefMATH
18.
Larchey-Wendling, D., Galmiche, D.: The undecidability of boolean BI through phase semantics. In: Logic in Computer Science - LICS, pp. 140–149. IEEE Computer Society (2010)
19.
Marx, M., Pólos, L., Masuch, M.: Arrow Logic and Multi-modal Logic. CSLI Publications, Stanford (1996)MATH
20.
21.
22.
23.
Pratt, V.R.: Models of program logics. In: Foundations of Computer Science - FOCS, pp. 115–122. IEEE Computer Society (1979)
24.
Pym, D.J.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, vol. 26. Springer, Netherlands (2002). Kluwer Academic PublishersMATH
25.
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science - LICS, pp. 55–74. IEEE Computer Society (2002)
26.
Schild, K.: A correspondence theory for terminological logics: preliminary report. In: Mylopoulos, J., Reiter, R. (eds.) International Joint Conference on Artificial Intelligence - IJCAI, pp. 466–471. Morgan Kaufmann (1991)
27.
Metadaten
Titel
Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition
verfasst von
Joseph Boudou
Copyright-Jahr
2016
Buch
Automated Reasoning

Print ISBN: 978-3-319-40228-4

Electronic ISBN: 978-3-319-40229-1

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-40229-1_26

Premium Partner

    Bildnachweise