Skip to main content

2015 | OriginalPaper | Buchkapitel

Exponential-Size Model Property for PDL with Separating Parallel Composition

verfasst von : Joseph Boudou

Erschienen in: Mathematical Foundations of Computer Science 2015

Verlag: Springer Berlin Heidelberg

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

search-config
loading …

Abstract

Propositional dynamic logic is extended with a parallel program having a separating semantic: the program \((\alpha \parallel \beta )\) executes \(\alpha \) and \(\beta \) on two substates of the current state. We prove that when the composition of two substates is deterministic, the logic has the exponential-size model property. The proof is by a piecewise filtration using an adaptation of the Fischer-Ladner closure. We conclude that the satisfiability of the logic is decidable in NEXPTIME.

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!

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!

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!

Literatur
1.
Zurück zum Zitat 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 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.
Zurück zum Zitat Balbiani, P., Boudou, J.: Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization. J. Logic Comput. (2015, to appear) Balbiani, P., Boudou, J.: Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization. J. Logic Comput. (2015, to appear)
3.
Zurück zum Zitat Balbiani, P., Tinchev, T.: Definability and computability for PRSPDL. In: Advances in Modal Logic, pp. 16–33. College Publications (2014) Balbiani, P., Tinchev, T.: Definability and computability for PRSPDL. In: Advances in Modal Logic, pp. 16–33. College Publications (2014)
4.
Zurück zum Zitat Benevides, M.R.F., de Freitas, R.P., Viana, J.P.: Propositional dynamic logic with storing, recovering and parallel composition. ENTCS 269, 95–107 (2011) Benevides, M.R.F., de Freitas, R.P., Viana, J.P.: Propositional dynamic logic with storing, recovering and parallel composition. ENTCS 269, 95–107 (2011)
5.
Zurück zum Zitat Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge (2001) MATH Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge (2001) MATH
6.
Zurück zum Zitat Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: POPL, pp. 365–377. ACM (2000) Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: POPL, pp. 365–377. ACM (2000)
7.
Zurück zum Zitat Collinson, M., Pym, D.J.: Algebra and logic for resource-based systems modelling. Math. Struct. Comput. Sci. 19(5), 959–1027 (2009)MathSciNetCrossRefMATH Collinson, M., Pym, D.J.: Algebra and logic for resource-based systems modelling. Math. Struct. Comput. Sci. 19(5), 959–1027 (2009)MathSciNetCrossRefMATH
8.
Zurück zum Zitat Demri, S., Deters, M.: Separation logics and modalities: a survey. J. Appl. Non Class. Logics 25(1), 50–99 (2015)MathSciNetCrossRef Demri, S., Deters, M.: Separation logics and modalities: a survey. J. Appl. Non Class. Logics 25(1), 50–99 (2015)MathSciNetCrossRef
9.
Zurück zum Zitat van Ditmarsch, H., van der Hoek, W., Kooi, B.P.: Dynamic Epistemic Logic, vol. 337. Springer Science and Business Media, Heidelberg (2007) CrossRef van Ditmarsch, H., van der Hoek, W., Kooi, B.P.: Dynamic Epistemic Logic, vol. 337. Springer Science and Business Media, Heidelberg (2007) CrossRef
10.
11.
Zurück zum Zitat Harel, D.: Recurring dominoes: making the highly undecidable highly understandable (preliminary report). In: Budach, L. (ed.) Fundamentals of Computation Theory. LNCS, vol. 158, pp. 177–194. Springer, Heidelberg (1983) Harel, D.: Recurring dominoes: making the highly undecidable highly understandable (preliminary report). In: Budach, L. (ed.) Fundamentals of Computation Theory. LNCS, vol. 158, pp. 177–194. Springer, Heidelberg (1983)
12.
Zurück zum Zitat Lange, M., Lutz, C.: 2-exptime lower bounds for propositional dynamic logics with intersection. J. Symb. Log. 70(4), 1072–1086 (2005)MathSciNetCrossRefMATH Lange, M., Lutz, C.: 2-exptime lower bounds for propositional dynamic logics with intersection. J. Symb. Log. 70(4), 1072–1086 (2005)MathSciNetCrossRefMATH
13.
Zurück zum Zitat Larchey-Wendling, D., Galmiche, D.: The undecidability of boolean BI through phase semantics. In: LICS, pp. 140–149. IEEE Computer Society (2010) Larchey-Wendling, D., Galmiche, D.: The undecidability of boolean BI through phase semantics. In: LICS, pp. 140–149. IEEE Computer Society (2010)
14.
Zurück zum Zitat Marx, M., Pólos, L., Masuch, M.: Arrow Logic and Multi-modal Logic. CSLI Publications, Stanford (1996) MATH Marx, M., Pólos, L., Masuch, M.: Arrow Logic and Multi-modal Logic. CSLI Publications, Stanford (1996) MATH
15.
17.
Zurück zum Zitat Pym, D.J.: The semantics and proof theory of the logic of bunched implications, Applied Logic Series, vol. 26. Kluwer Academic Publishers (2002) Pym, D.J.: The semantics and proof theory of the logic of bunched implications, Applied Logic Series, vol. 26. Kluwer Academic Publishers (2002)
18.
Zurück zum Zitat Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS. pp. 55–74. IEEE Computer Society (2002) Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS. pp. 55–74. IEEE Computer Society (2002)
Metadaten
Titel
Exponential-Size Model Property for PDL with Separating Parallel Composition
verfasst von
Joseph Boudou
Copyright-Jahr
2015
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-48057-1_10

Premium Partner