Resource separation in dynamic logic of propositional assignments. (English) Zbl 1518.68203
Summary: We extend dynamic logic of propositional assignments by adding an operator of parallel composition that is inspired by separation logics. We provide an axiomatization via reduction axioms, thereby establishing decidability. We also prove that the complexity of both the model checking and the satisfiability problem stay in PSPACE.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B70 | Logic in computer science |
| 68Q25 | Analysis of algorithms and problem complexity |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Keywords:
dynamic logic; separation logic; propositional assignments; parallel composition; concurrencySoftware:
GraphplanReferences:
| [1] | Abrahamson, K. R., Decidability and expressivity of logics of processes (1980), Department of Computer Science, University of Washington: Department of Computer Science, University of Washington Seattle, WA, Report 80-08-01 |
| [2] | Balbiani, Philippe; Boudou, Joseph, Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization, J. Log. Comput., 28, 4, 705-731 (2018) · Zbl 1444.03109 |
| [3] | Benevides, Mario R. F.; de Freitas, Renata P.; Viana, Jorge Petrucio, Propositional dynamic logic with storing, recovering and parallel composition, Electron. Notes Theor. Comput. Sci., 269, 95-107 (2011) · Zbl 1347.03059 |
| [4] | Blum, Avrim; Furst, Merrick L., Fast planning through planning graph analysis, Artif. Intell., 90, 1-2, 281-300 (1997) · Zbl 1017.68533 |
| [5] | Balbiani, Philippe; Herzig, Andreas; Schwarzentruber, François; Troquard, Nicolas, DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE (2014), CoRR |
| [6] | Balbiani, Philippe; Herzig, Andreas; Troquard, Nicolas, Dynamic logic of propositional assignments: a well-behaved variant of PDL, (Kupferman, O., Logic in Computer Science (LICS) (2013), IEEE) · Zbl 1366.03208 |
| [7] | Boudou, Joseph; Herzig, Andreas; Troquard, Nicolas, Resource separation in dynamic logic of propositional assignments, (Barbosa, Luís Soares; Baltag, Alexandru, Dynamic Logic. New Trends and Applications - Second International Workshop, DaLí 2019, Porto, Portugal, October 7-11, 2019, Proceedings. Dynamic Logic. New Trends and Applications - Second International Workshop, DaLí 2019, Porto, Portugal, October 7-11, 2019, Proceedings, Lecture Notes in Computer Science, vol. 12005 (2019), Springer), 155-170 · Zbl 1496.03124 |
| [8] | Brookes, Stephen; O’Hearn, Peter W., Concurrent separation logic, SIGLOG News, 3, 3, 47-65 (2016) |
| [9] | Boudou, Joseph, Complexity optimal decision procedure for a propositional dynamic logic with parallel composition, (Olivetti, Nicola; Tiwari, Ashish, International Joint Conference on Automated Reasoning. International Joint Conference on Automated Reasoning, IJCAR. International Joint Conference on Automated Reasoning. International Joint Conference on Automated Reasoning, IJCAR, Lecture Notes in Computer Science, vol. 9706 (2016), Springer), 373-388 · Zbl 1475.68075 |
| [10] | Stephen D. Brookes, A semantics for concurrent separation logic, in: Gardner and Yoshida [19], pp. 16-34. · Zbl 1099.68650 |
| [11] | Balbiani, Philippe; Tinchev, Tinko, Definability and computability for PRSPDL, (Goré, Rajeev; Kooi, Barteld P.; Kurucz, Agi, Advances in Modal Logic, vol. 10 (2014), College Publications), 16-33 · Zbl 1385.03033 |
| [12] | Balbiani, Philippe; Vakarelov, Dimiter, PDL with intersection of programs: a complete axiomatization, J. Appl. Non-Class. Log., 13, 3-4, 231-276 (2003) · Zbl 1181.03030 |
| [13] | Cooper, Martin C.; Herzig, Andreas; Maffre, Faustine; Maris, Frédéric; Régnier, Pierre, A simple account of multi-agent epistemic planning, (Kaminka, G. A.; Fox, M.; Bouquet, P.; Hüllermeier, E.; Dignum, V.; Dignum, F.; van Harmelen, F., European Conference on Artificial Intelligence (ECAI). European Conference on Artificial Intelligence (ECAI), Frontiers in Artificial Intelligence and Applications, vol. 285 (2016), IOS Press), 193-201 · Zbl 1403.68259 |
| [14] | Charrier, Tristan; Schwarzentruber, François, Arbitrary public announcement logic with mental programs, (Weiss, G.; Yolum, P.; Bordini, R. H.; Elkind, E., Autonomous Agents and Multiagent Systems (AAMAS) (2015), ACM), 1471-1479 |
| [15] | Charrier, Tristan; Schwarzentruber, François, A succinct language for dynamic epistemic logic, (Larson, K.; Winikoff, M.; Das, S.; Durfee, E. H., Autonomous Agents and Multiagent Systems (AAMAS) (2017), ACM), 123-131 |
| [16] | Darvas, Ádám; Hähnle, Reiner; Sands, David, A theorem proving approach to analysis of secure information flow, (Hutter, D.; Ullmann, M., Security in Pervasive Computing (2005), Springer: Springer Berlin, Heidelberg), 193-209 |
| [17] | Feuillade, Guillaume; Herzig, Andreas; Rantsoudis, Christos, A dynamic logic account of active integrity constraints, Fundam. Inform., 169, 3, 179-210 (2019) · Zbl 1427.68064 |
| [18] | Goldblatt, Robert, Parallel action: concurrent dynamic logic with independent modalities, Stud. Log., 51, 3/4, 551-578 (1992) · Zbl 0784.03019 |
| [19] | (Gardner, Philippa; Yoshida, Nobuko, CONCUR 2004 - Concurrency Theory, 15th Int. Conf., London, UK, August 31 - September 3, 2004, Proceedings. CONCUR 2004 - Concurrency Theory, 15th Int. Conf., London, UK, August 31 - September 3, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3170 (August 2004), Springer: Springer London, UK) · Zbl 1058.68006 |
| [20] | Herzig, Andreas, A simple separation logic, (Libkin, L.; Kohlenbach, U.; de Queiroz, R. J.G. B., Workshop on Logic, Language, Information and Computation (WoLLIC). Workshop on Logic, Language, Information and Computation (WoLLIC), Lecture Notes in Computer Science, vol. 8071 (2013), Springer), 168-178 · Zbl 1395.03017 |
| [21] | Herzig, Andreas, Belief change operations: a short history of nearly everything, told in dynamic logic of propositional assignments, (Baral, Chitta; De Giacomo, Giuseppe, Principles of Knowledge Representation and Reasoning (KR) (2014), AAAI Press) |
| [22] | Herzig, Andreas; Menezes, Viviane; Nunes De Barros, Leliane; Wassermann, Renata, On the revision of planning tasks, (Schaub, T., European Conference on Artificial Intelligence. European Conference on Artificial Intelligence, ECAI (August 2014)) · Zbl 1366.68263 |
| [23] | Herzig, Andreas; Maris, Frédéric; Vianey, Julien, Dynamic logic of parallel propositional assignments and its applications to planning, (Kraus, S., International Joint Conference on Artificial Intelligence. International Joint Conference on Artificial Intelligence, IJCAI (2019)), 5576-5582, ijcai.org |
| [24] | Mayer, Alain J.; Stockmeyer, Larry J., The complexity of PDL with interleaving, Theor. Comput. Sci., 161, 1&2, 109-122 (1996) · Zbl 0872.03016 |
| [25] | Novaro, Arianna; Grandi, Umberto; Herzig, Andreas, Judgment aggregation in dynamic logic of propositional assignments, J. Log. Comput., 28, 7, 1471-1498 (2018) · Zbl 1444.03119 |
| [26] | Peter W. O’Hearn, Resources, concurrency and local reasoning, in: Gardner and Yoshida [19], pp. 49-67. |
| [27] | Peleg, David, Concurrent dynamic logic, J. ACM, 34, 2, 450-479 (1987) · Zbl 0645.03021 |
| [28] | Reynolds, John C., Separation logic: a logic for shared mutable data structures, (Logic in Computer Science (LICS) (2002), IEEE Computer Society), 55-74 |
| [29] | Scheben, Christoph; Greiner, Simon, Information flow analysis, (Ahrendt, W.; Beckert, B.; Bubel, R.; Hähnle, R.; Schmitt, P. H.; Ulbrich, M., Deductive Software Verification - the KeY Book - from Theory to Practice. Deductive Software Verification - the KeY Book - from Theory to Practice, Lecture Notes in Computer Science, vol. 10001 (2016), Springer), 453-471 |
| [30] | van Ditmarsch, Hans P.; van der Hoek, Wiebe; Kooi, Barteld, Dynamic Epistemic Logic (2007), Kluwer Academic Publishers · Zbl 1156.03015 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
