Reasoning about Reachability and Concurrency in DEL Games Silvia Stranieri1 1 University of Naples Federico II, Italy Abstract Dynamic Epistemic Logic allows modelling high order knowledge and the evolution of what an agent knows over time. This work shows decidability results about reachability goals and concurrent execution of Dynamic Epistemic Logic games. Keywords Dynamic Epistemic Logic, Multi-agent systems, DEL games 1. Introduction Dynamic Epistemic Logic (DEL) [1] is used to describe how actions affect the world, how agents perceive them, and how their knowledge changes during the execution of the game. In this work, DEL is investigated on reachability and concurrency aspects. We do this in two different directions. First, a setting in which agents are not active, but they simply observe a controller and an environment playing in turn and modifying their knowledge. In this case the controller synthesis problem is addressed. In the second setting, agents become players of an imperfect information game playing in coalitions against each other, addressing the distributed synthesis problem. Precisely, reachability goals are expressed through LTLK formulas, involving both temporal and knowledge operators, and decidability results over public actions and public announcements are provided [2]. We recall that an action is public when it is visible to all agents [3, 4, 5, 6], while a public announcement is a special case of public action with no effect besides epistemic ones. DEL game concurrent executions are also considered in this work, by providing an opportune concurrent update product to define how actions played concurrently affect the epistemic model, relying on a scheduler to solve possible conflicts. The distributed synthesis is proved to be decidable when actions are public. This is obtained by reducing the problem to the model checking of ATL*K [7]. 2. DEL Models In this section, the key aspects of epistemic logic are provided [8]. OVERLAY 2022: 4th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, November 28, 2022, Udine, Italy $ silvia.stranieri@unina.it (S. Stranieri) Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) Epistemic Model Definition 2.1. Let AP and Agt be the set of atomic propositions and the set of agents respectively, an epistemic model β„³ = (W , (β‰Όπ‘Ž )π‘ŽβˆˆAgt , πœ†) is a tuple where β€’ W is a set of worlds (or situations), β€’ β‰Όπ‘Ž βŠ† W Γ— W is an accessibility relation for agent π‘Ž, and β€’ πœ† : W β†’ 2AP is a valuation function. One can write w β‰Όπ‘Ž u instead of (w , u) βˆˆβ‰Όπ‘Ž ; the intended meaning of w β‰Όπ‘Ž u is that when the actual world is w , agent π‘Ž considers that u may be the actual world. The valuation function πœ† provides the subset of atomic propositions that hold in a world. A pair (β„³, w ) where w is a world in β„³ is called a pointed epistemic model, or epistemic state, while a pair (β„³, W β€² ), where W β€² βŠ† W is a subset of worlds, is called a multipointed epistemic model. An epistemic model is finite if its set of worlds W is finite and βˆ‘οΈ€ ∈ W , πœ†(w ) is for each world wβˆ‘οΈ€ finite. In that case, we let |β„³| be the size of β„³, defined as |W |+ π‘ŽβˆˆAgt | β‰Όπ‘Ž |+ w ∈W |πœ†(w )|. From now on, all epistemic models are assumed to be finite. Event models Dynamic Epistemic Logic also relies on event models. These models specify actions, the preconditions for their execution, their effects on the world, and how agents perceive their occurrence. Definition 2.2. An event model π’œ = (A, (β‰Όπ’œ π‘Ž )π‘ŽβˆˆAgt , pre, post) is a tuple where: β€’ A is a set of possible actions, β€’ β‰Όπ’œπ‘Ž βŠ† A Γ— A is the accessibility relation for agent π‘Ž, β€’ pre : A β†’ EL is a precondition function (where EL stands for epistemic logic), and β€’ post : AΓ—AP β†’ Prop is a postcondition function (where Prop stands for set of propositions). An action 𝛼 is executable in a world w of an epistemic model β„³ if its precondition pre(𝛼) β€² ⋁︀ holds in w , i.e., β„³, w |= pre(𝛼). A set of actions A βŠ† A is non-blocking if π›ΌβˆˆAβ€² pre(𝛼) ≑ ⊀, i.e., there is always at least one action in Aβ€² that is executable. After executing an executable action 𝛼 in a world w , proposition 𝑝 holds if its postcondition was satisfied before executing the action; thus, let us define πœ†(w , 𝛼) := {𝑝 ∈ AP | β„³, w |= post(𝛼, 𝑝)} as the set of propositions holding after executing 𝛼 in w . Since postconditions are propositional, one can define similarly πœ†(𝜈, 𝛼) where 𝜈 βŠ† 2AP is a valuation. A pointed action model is a pair (π’œ, 𝛼) where 𝛼 represents the actual action. Only finite action models will be considered, i.e., such that the set of actions A is finite, and for every action 𝛼 ∈ A there are only finitely many atomic propositions 𝑝 ∈ AP whose postcondition is not trivially false, i.e., such that post(𝛼, 𝑝) ΜΈ=βŠ₯. We let |π’œ| be the size of π’œ, defined as follows: βˆ‘οΈ βˆ‘οΈ βˆ‘οΈ |π’œ| := |A| + | β‰Όπ’œ π‘Ž | + |pre(𝛼)| + |post(𝛼, 𝑝)| π‘ŽβˆˆAgt π›ΌβˆˆA π›ΌβˆˆA,π‘βˆˆAP When working with variables π‘₯ over finite domains, one may write π‘₯ := 𝑑 for the effect of setting π‘₯ to value 𝑑. This can again be encoded with atomic propositions π‘₯𝑑 and postconditions as defined above. Update product After occurrence of an action 𝛼 in a world w , agent π‘Ž considers it possible that action 𝛼′ occurred in world w β€² , if in w he considers w β€² possible and 𝛼′ is executable in w β€² . Hence, he considers action 𝛼′ possible when action 𝛼 is executed. This leads to the following definition of the product that models how to update an epistemic model when an action is executed [9]. Definition 2.3 (Product [9]). Let β„³ = (W , (β‰Ό)π‘ŽβˆˆAgt , πœ†) be an epistemic model, and π’œ = (A, (β‰Όπ’œ π‘Ž )π‘ŽβˆˆAgt , pre, post) be an action model. The product of β„³ and π’œ is defined as β„³ βŠ— π’œ = (W β€² , (β‰Όπ’œ β€² β€² π‘Ž ) , πœ† ) where: β€’ W β€² = {(w , 𝛼) ∈ W Γ— A | β„³, w |= pre(𝛼)}, β€’ (w , 𝛼) β‰Όβ€²π‘Ž (w β€² , 𝛼′ ) if w β‰Όπ‘Ž w β€² and 𝛼 β‰Όπ’œ β€² π‘Ž 𝛼 , and β€’ πœ†β€² (w , 𝛼) = πœ†(w , 𝛼). 3. Reachability Results As previously said, reachability goals in DEL games have been considered in two different settings. In the first case, two players (the Controller and the Environment) playing in turn are taken into account, and hence the set of actions is partitioned according to them. In this case, the problem is to decide whether the Controller has a strategy to ensure that some epistemic property holds. The controller synthesis problem is undecidable, in general. There are some special cases in which it becomes decidable. Precisely, when actions are: β€’ Public announcements, the problem is Pspace-complete; β€’ Public actions, the problem is Exptime-complete. The problem can be further investigated by letting the agents be active entities and chose their own actions. Then, one can consider the distributed strategy synthesis as the problem of deciding whether a coalition of agents has a common strategy to let some property hold. This problem is undecidable in general [10], but, as for the controller synthesis problem, there are cases in which some decidability results can be obtained, in particular when actions are: β€’ Public announcements, the problem is Pspace-complete; β€’ Public actions, the problem is Exptime-complete. Further details on the algorithms to prove the results above can be found in [2]. 4. Concurrency results In this section, concurrent executions of DEL games are considered and some decidability results are shown. Concurrent Actions To define concurrent actions, atomic propositions are partitioned into shared propositions (AP 𝑠 ) that all agents can modify, and private ones (AP π‘π‘Ž , for the specific agent π‘Ž). The set Aπ‘Ž denotes the actions that an agent can play without βˆοΈ€ modifying private propositions of others. A joint action is a tuple ⃗𝛼 = βŸ¨π›Ό1 , . . . , 𝛼𝑁 ⟩ ∈ π‘ŽβˆˆAgt Aπ‘Ž , and we let ⃗𝛼𝑏 denote action 𝛼𝑏 , and it is available in w when every individual action ⃗𝛼𝑏 can be executed in w . The formula noconflict(𝛼 βƒ— )(𝑝) expresses that all individual actions of a joint action ⃗𝛼 agree on their effect (if any) on proposition 𝑝, and in general: ⋀︁ noconflict(𝛼⃗ ) := noconflict(𝛼 βƒ— )(𝑝). (1) π‘βˆˆAP Hence, one can say that a joint action ⃗𝛼 is non-conflicting in w if β„³, w |= noconflict(𝛼 βƒ— ). Otherwise ⃗𝛼 is conflicting in w . In case of conflicting available joint action, a scheduler is supposed to select a maximal subset of consistent individual actions, by inhibiting the remaining ones, through a ghost mapping. Concurrent Update Product Definition 4.1 (Concurrent update product). The concurrent update product of an epistemic model β„³ and an action model π’œ is the Kripke model β„³ ⊞ π’œ = (W ⊞ , (β‰ˆβŠž ⊞ π‘Ž )π‘ŽβˆˆAgt , πœ† ), where: β€’ W ⊞ = {(w , ⃗𝛽 ) ∈ W Γ— A𝑁 | ⃗𝛽 ∈ Max(𝛼 βƒ— , u), ⃗𝛼 available in w }; βƒ— ⊞ βƒ— π’œ β€’ (w , 𝛽 ) β‰ˆπ‘Ž (u, ⃗𝛾 ) if w β‰ˆπ‘Ž u and 𝛽 𝑏 β‰ˆπ‘Ž ⃗𝛾 𝑏 for all 𝑏; β€’ 𝑝 ∈ πœ†βŠž (u, ⃗𝛽 ) if (β„³, u) |= π‘ŽβˆˆAgt(𝛽⃗ ,𝑝) post(π›½π‘Ž , 𝑝). β‹€οΈ€ where: Max(𝛼⃗ , w ) := βƒ— | ⃗𝛽 βͺ― ⃗𝛼 and ⃗𝛽 is non-conflicting in w and ⃗𝛽 is βͺ― -maximal} {𝛽 The set of epistemic states that may result when a joint action ⃗𝛼 is executed in (β„³, w ) are: (β„³, w ) ⊞ ⃗𝛼 := {(β„³ ⊞ π’œ, (w , ⃗𝛽 )) | ⃗𝛽 ∈ Max(𝛼 βƒ— , w )}. This set is a singleton when ⃗𝛼 is non-conflicting in w . Decidability Results By exploiting the result of [6] saying that the model checking of ATL*K on finite deterministic concurrent game structures is 2-Exptime-complete when actions are public, one can conclude that the same decidability results holds for model checking on concurrent DEL games, when actions are public, the ghost mapping is injective, and the scheduler is public. 5. Conclusions This work shows Pspace-completeness both for the controller synthesis and the distributed synthesis problem when actions are public announcements, and Exptime-completeness when actions are public. This last decidability result also holds for model checking on concurrent DEL games. We plan to further investigate the connection of DEL with more powerful logics for strategic reasoning, such as Strategy Logic [11] under imperfect information [12, 13]. Acknowledgments This papers is based on my Phd Thesis [14] and the works [2, 7]. I would like to thank Aniello Murano, Bastien Maubert, Sophie Pinchinat, and Francois Schwarzentruber for their mentoring and support. This work is partially supported by the PRIN project RIPER (No. 20203FFYLK). References [1] H. Van Ditmarsch, W. van Der Hoek, B. Kooi, Dynamic epistemic logic, volume 337, Springer Science & Business Media, 2007. [2] B. Maubert, A. Murano, S. Pinchinat, F. Schwarzentruber, S. Stranieri, Dynamic epistemic logic games with epistemic temporal goals, in: Proceedings of 24th European Conference on Artificial Intelligence ECAI 2020, IOS Press, 2020, pp. 155–162. [3] F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin, Verification of broadcasting multi-agent systems against an epistemic strategy logic, in: C. Sierra (Ed.), Proc. of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, 2017, pp. 91–97. [4] F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin, Verification of multi-agent systems with imperfect information and public actions, in: Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, ACM, 2017, pp. 1268–1276. [5] F. Belardinelli, S. Knight, A. Lomuscio, B. Maubert, A. Murano, S. Rubin, Reasoning about agents that may know other agents’ strategies, in: Proc. of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, ijcai.org, 2021, pp. 1787–1793. [6] F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin, Verification of multi-agent systems with public actions against strategy logic, Artif. Intell. 285 (2020) 103302. [7] B. Maubert, S. Pinchinat, F. Schwarzentruber, S. Stranieri, Concurrent games in dynamic epistemic logic, in: Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, 2020, pp. 1877–1883. [8] R. Fagin, J. Halpern, Y. Moses, M. Vardi, Reasoning about Knowledge, MIT Press, 1995. [9] A. Baltag, L. S. Moss, S. Solecki, The logic of public announcements, common knowledge, and private suspicions, in: TARK’98, 1998, pp. 43–56. [10] M. J. Coulombe, J. Lynch, Cooperating in video games? impossible! undecidability of team multiplayer games, in: FUN’18, 2018, pp. 14:1–14:16. [11] F. Mogavero, A. Murano, G. Perelli, M. Y. Vardi, Reasoning about strategies: On the model-checking problem, ACM Trans. Comput. Log. 15 (2014) 34:1–34:47. [12] W. Jamroga, V. Malvone, A. Murano, Natural strategic ability, Artif. Intell. 277 (2019). [13] R. Berthon, B. Maubert, A. Murano, S. Rubin, M. Y. Vardi, Strategy logic with imperfect information, ACM Trans. Comput. Log. 22 (2021) 5:1–5:51. [14] S. Stranieri, Vehicular ad Hoc Networks: an algorithmic and a game-theoretic approach, Ph.D. thesis, UniversitΓ‘ di Napoli, Federico II, 2022.