nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Resource Separation in Dynamic Logic of Propositional Assignments

verfasst von : Joseph Boudou, Andreas Herzig, Nicolas Troquard

Erschienen in: Dynamic Logic. New Trends and Applications

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We extend dynamic logic of propositional assignments by adding an operator of parallel composition that is inspired by separation logics. We provide an axiomatisation via reduction axioms, thereby establishing decidability. We also prove that the complexity of both the model checking and the satisfiability problem stay in PSPACE.

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 Iterative Division in the Distributive Full Non-associative Lambek Calculus

Nächstes Kapitel Stit Semantics for Epistemic Notions Based on Information Disclosure in Interactive Settings

As suggested by one of the reviewers, it may be relaxed and one may suppose that a program can only modify a variable without being able to read its value. This would simplify the presentation of the logic; however, we believe that our inclusion constraint is natural in most applications.

We are grateful to Rainer Hähnle for pointing this out to us.

[BB18]

Balbiani, P., Boudou, J.: Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization. J. Log. Comput. 28(4), 705–731 (2018)MathSciNetCrossRef

[BdFV11]

Benevides, M.R.F., de Freitas, R.P., Viana, J.P.: Propositional dynamic logic with storing, recovering and parallel composition. Electr. Notes Theor. Comput. Sci. 269, 95–107 (2011)MathSciNetCrossRef

[BHST14]

Balbiani, P., Herzig, A., Schwarzentruber, F., Troquard, N.: DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE. CoRR, abs/1411.7825 (2014)

[BHT13]

Balbiani, P., Herzig, A., Troquard, N.: Dynamic logic of propositional assignments: a well-behaved variant of PDL. In: Kupferman, O. (ed.) Logic in Computer Science (LICS). IEEE (2013)

[BO16]

Brookes, S., O’Hearn, P.W.: SIGLOG News. Concurrent separation logic 3(3), 47–65 (2016)

[Bro04]

Brookes, S.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 16–34. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_2. [GY04]CrossRef

[Bro07]

Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1–3), 227–270 (2007)MathSciNetCrossRef

[BV03]

Balbiani, P., Vakarelov, D.: PDL with intersection of programs: a complete axiomatization. J. Appl. Non-Class. Log. 13(3–4), 231–276 (2003)CrossRef

[CHM+16]

Cooper, M.C., Herzig, A., Maffre, F., Maris, F., Régnier, P.: A simple account of multi-agent epistemic planning. In: Kaminka, G.A., et al. (eds.) ECAI 2016–22nd European Conference on Artificial Intelligence, The Hague, The Netherlands, 29 August–2 September 2016, Volume 285 of Frontiers in Artificial Intelligence and Applications, pp. 193–201. IOS Press (2016)

[CS15]

Charrier, T., Schwarzentruber, F.: Arbitrary public announcement logic with mental programs. In: Weiss, G., Yolum, P., Bordini, R.H., Elkind, E. (eds.) Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, 4–8 May 2015, pp. 1471–1479. ACM (2015)

[CS17]

Charrier, T., Schwarzentruber, F.: A succinct language for dynamic epistemic logic. In: Larson, K., Winikoff, M., Das, S., Durfee, E.H. (eds.) Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, São Paulo, Brazil, 8–12 May 2017, pp. 123–131. ACM (2017)

[DHS05]

Darvas, Á., Hähnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193–209. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32004-3_20CrossRef

[FHR19]

Feuillade, G., Herzig, A., Rantsoudis, C.: A dynamic logic account of active integrity constraints. Fundamenta Informaticae 169(3), 179–210 (2019)MathSciNetCrossRef

[Gol92]

Goldblatt, R.: Parallel action: concurrent dynamic logic with independent modalities. Studia Logica 51(3/4), 551–578 (1992)MathSciNetCrossRef

[GY04]

Gardner, P., Yoshida, N. (eds.): CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 – 3 September 2004, Proceedings, Volume 3170 of Lecture Notes in Computer Science. Springer, Heidelberg (2004)

[Her13]

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). https://doi.org/10.1007/978-3-642-39992-3_16CrossRefMATH

[Her14]

Herzig, A.: Belief change operations: a short history of nearly everything, told in dynamic logic of propositional assignments. In: Baral, C., De Giacomo, G. (eds.) Proceedings of KR 2014. AAAI Press (2014)

[HMNDBW14]

Herzig, A., Menezes, V., De Barros, L.N., Wassermann, R.: On the revision of planning tasks. In: Schaub, T. (ed.) European Conference on Artificial Intelligence (ECAI), August 2014

[HMV19]

Herzig, A., Maris, F., Vianey, J.: Dynamic logic of parallel propositional assignments and its applications to planning. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, 10–16 August 2019, pp. 5576–5582. ijcai.org (2019)

[MS96]

Mayer, A.J., Stockmeyer, L.J.: The complexity of PDL with interleaving. Theor. Comput. Sci. 161(1&2), 109–122 (1996)MathSciNetCrossRef

[NGH18]

Novaro, A., Grandi, U., Herzig, A.: Judgment aggregation in dynamic logic of propositional assignments. J. Log. Comput. 28(7), 1471–1498 (2018)MathSciNetCrossRef

[O’H04]

O’Hearn, P.W.: Resources, concurrency and local reasoning. Gardner and Yoshida, pp. 49–67

[Pel87]

Peleg, D.: Concurrent dynamic logic. J. ACM 34(2), 450–479 (1987)MathSciNetCrossRef

[SG16]

Scheben, C., Greiner, S.: Information flow analysis. Deductive Software Verification – The KeY Book. LNCS, vol. 10001, pp. 453–471. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49812-6_13CrossRef

[vDvdHK07]

van Ditmarsch, H.P., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Kluwer Academic Publishers (2007)

[VVB14]

Veloso, P.A.S., Veloso, S.R.M., Benevides, M.R.F.: PDL for structured data: a graph-calculus approach. Logic J. IGPL 22(5), 737–757 (2014)MathSciNetCrossRef

Titel: Resource Separation in Dynamic Logic of Propositional Assignments
verfasst von: Joseph Boudou
Andreas Herzig
Nicolas Troquard
Verlag: Springer International Publishing
Buch: Dynamic Logic. New Trends and Applications
Print ISBN: 978-3-030-38807-2

Electronic ISBN: 978-3-030-38808-9

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-38808-9_10

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"