=Paper=
{{Paper
|id=Vol-3311/paper7
|storemode=property
|title=Reasoning about Reachability and Concurrency in DEL Games
|pdfUrl=https://ceur-ws.org/Vol-3311/paper7.pdf
|volume=Vol-3311
|authors=Silvia Stranieri
|dblpUrl=https://dblp.org/rec/conf/aiia/Stranieri22
}}
==Reasoning about Reachability and Concurrency in DEL Games==
<pdf width="1500px">https://ceur-ws.org/Vol-3311/paper7.pdf</pdf>
<pre>
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.

</pre>