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. 2. DEL Models
Dynamic Epistemic Logic (DEL) [
DEL game concurrent executions are also considered in this work, by providing an opportune
concurrent update product to define how actions played concurrently afect 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 [
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 for each world w ∈ W , (w ) is ifnite. 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 efects 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| + ∈Agt ∑︁ | ≼ | + ∑︁ |pre( )| + ∈A
∑︁ ∈A,∈AP |post (, )|
When working with variables over finite domains, one may write := for the efect 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 [
Definition 2.3 (Product [
As previously said, reachability goals in DEL games have been considered in two diferent 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 [
Further details on the algorithms to prove the results above can be found in [
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 le⃗t denote action , and it is available in w when every individual action⃗ can be executed in w .
The formula noconflic⃗t( )() expresses that all individual actions of a joint action⃗ agree on their efect (if any) on proposition , and in general: noconflic⃗t( ) := ⋀︁ noconflic⃗t( )().
(1) ∈AP
Hence, one can say that a joint action⃗ is non-conflicting in w if ℳ, w |= noconflic⃗t( ). 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.
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 [
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 [
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).