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

Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition

Authors : Philippe Balbiani, Joseph Boudou

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

PRSPDL is a propositional dynamic logic with an operator for parallel compositions of programs. We first give a complexity upper bound for this logic. Then we focus on the class of \(\vartriangleleft \)-deterministic frames and give tableaux methods for two fragments of PRSPDL over this class of frames.

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 KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
next chapter Regular Patterns in Second-Order Unification
Literature
1.
Abrahamson, K.: 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.: Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization, J. Logic Comput. (2015)
3.
Balbiani, P., Tinchev, T.: Definability and computability for PRSPDL. In: Advances in Modal Logic, pp. 16–33. College Publications (2014)
4.
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.
6.
Collinson, M., Pym, D.J.: Algebra and logic for resource-based systems modelling. Math. Struct. Comput. Sci. 19(5), 959–1027 (2009)MathSciNetCrossRefMATH
7.
Courtault, J.R., Galmiche, D.: A Modal BI logic for dynamic resource properties. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 134–148. Springer, Heidelberg (2013) CrossRef
8.
Danecki, R.: Nondeterministic propositional dynamic logic with intersection is decidable. In: Skowron, A. (ed.) Computation Theory. LNCS, vol. 208, pp. 34–53. Springer, Heidelberg (1984) CrossRef
9.
De Giacomo, G., Massacci, F.: Combining deduction and model checking into tableaux and algorithms for converse-PDL. Inf. Comput. 162(1–2), 117–137 (2000)CrossRefMATH
10.
Demri, S., Deters, M.: Separation logics and modalities: a survey. J. Appl. Non-Class. Logics 25(1), 50–99 (2015)MathSciNetCrossRef
11.
12.
Goré, R., Widmann, F.: An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 437–452. Springer, Heidelberg (2009) CrossRef
13.
Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput. 9(3), 385–410 (1999)MathSciNetCrossRefMATH
14.
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)CrossRefMATH
15.
Lutz, C.: PDL with intersection and converse is decidable. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 413–427. Springer, Heidelberg (2005) CrossRef
16.
Massacci, F.: Decision procedures for expressive description logics with intersection, composition, converse of roles and role identity. In: IJCAI, pp. 193–198. Morgan Kaufmann (2001)
17.
18.
19.
Pym, D.J.: The semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, vol. 26. Kluwer Academic Publishers, Dordrecht (2002) MATH
20.
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002)
Metadata
Title
Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition
Authors
Philippe Balbiani
Joseph Boudou
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_37

Premium Partner

    Image Credits