## Epistemic Ensembles in Semantic and Symbolic Environments (Extended Version with Proofs)

Rolf Hennicker 1 , Alexander Knapp , and Martin Wirsing 2 1

1 Ludwig-Maximilians-Universit¨ at M¨ unchen, M¨ unchen, Germany

{ hennicker , wirsing @ifi.lmu.de } 2 Universit¨ at Augsburg, Augsburg, Germany knapp@informatik.uni-augsburg.de

Dedicated to Rocco De Nicola

Abstract. An epistemic ensemble is composed of knowledge-based agents capable of retrieving and sharing knowledge and beliefs about themselves and their peers. These agents access a global knowledge state and use actions to communicate and cooperate, altering the collective knowledge state. We study two types of mathematical semantics for epistemic ensembles based on a common syntactic operational ensemble semantics: a semantic environment defined by a class of global epistemic states, and a symbolic environment consisting of a set of epistemic formulæ. For relating these environments, we use the concept of Φ -equivalence, where a class of epistemic states and a knowledge base are Φ -equivalent, if any formula of Φ holds in the class of epistemic states if, and only if, it is an element of the knowledge base. Our main theorem shows that Φ -equivalent configurations simulate each other and satisfy the same dynamic epistemic ensemble formulae.

## 1 Introduction

Ensembles [15,20] are collective systems consisting of dynamically interacting autonomic entities. In an epistemic ensemble [13] these entities are epistemic agents that possess knowledge and beliefs about themselves and other agents. The agents have access to a global knowledge state and utilise epistemic actions to cooperate and communicate. An epistemic action involves announcing an agent's knowledge or belief to others, thereby altering the collective knowledge state.

This paper builds upon our previous work [13,14]. In [13], we introduced epistemic ensembles in a semantic environment consisting of a single epistemic state; in

[14], we considered epistemic processes and related them in semantic environments of a single epistemic state with symbolic environments. Here, we focus on ensembles and model them as families of concurrently running epistemic processes. We introduce a syntactic operational semantics for these epistemic ensembles. Building on the operational semantics we consider an extended notion of semantic environment consisting not only of a single epistemic state but of a class of epistemic states. Following ideas from [14], we also apply the symbolic approach to epistemic ensembles and relate symbolic environments with the new, more general semantic approach.

The dynamic behaviour of each agent process in an ensemble is specified using a simple process algebra with guards and recursion. The syntactic operational semantics of the entire ensemble is defined generically by conditional transitions over uninterpreted agent actions. To specify global properties of epistemic ensembles, we use propositional dynamic logic over compound ensemble actions. Our main result is the study of two complementary kinds of mathematical semantics for epistemic ensembles building on the common syntactic operational semantics: one in a semantic environment defined by a class of global epistemic states, represented by pointed Kripke structures, and the other in a symbolic environment defined by a global epistemic knowledge base, represented by a finite set of epistemic formulæ. The agent actions are first interpreted by pointed action models [1,2]; in the semantic environment their effect is given by product updates on Kripke structures [1,2], while in the symbolic environment we use weakest liberal preconditions [10]. Building on [14], we relate the semantic and symbolic environments by fixing a finite set Φ of focus formulæ: A class K of epistemic states is Φ -equivalent to a symbolic state Γ ⊆ Φ if all K ∈ K satisfy exactly those ϕ ∈ Φ that are in Γ . Reusing the notion of Φ -representability we ensure that semantic and symbolic updates preserve Φ -equivalence. As our main results we show that Φ -equivalent ensemble configurations simulate each other and that they satisfy the same dynamic ensemble formulæ.

Related work. Research on using epistemic logic in system modelling and programming began with the seminal works on Dynamic Epistemic Logic (DEL [1,11]) and knowledgebased programs [12]. DEL focuses on modelling and verifying knowledge changes induced by action execution. We use DEL's reduction rules to define the weakest liberal precondition, which also underpin many foundational results of DEL, such as soundness and completeness [1,2], as well as the definition of a sequent calculus [21]. Knowledgebased programsconsider systems of concurrentlyrunningagents. [4] examines protocols based on DEL and, as [18], system properties in epistemic temporal logic.

Ourworkisbasedonaprocess-orienteddescription of dynamic system behaviour [9], in alignment with modern languages for ensembles such as SCEL [17], CARMA [7], and DEECo [8]. However, these languages rely on communication mechanisms like message passing and predicate-based communication,rather than epistemic actions. Our symbolic semantics for epistemic representation is related to the syntactic structures in [13] and belief bases in [16]. While Lorini's work is also based on DEL, it lacks a process-algebraic setting and uses specialised forms of knowledge update operations. In contrast, we consider general action models and apply an abstraction technique from epistemic Kripke semantics to a symbolic approach, preserving and reflecting dynamic ensemble properties.

Structure of the paper. We first introduce epistemic ensembles and their syntactic operational semantics in Sect. 2 and dynamic ensemble formulæ in Sect. 3. The agent actions of epistemic ensembles are interpreted by action models in Sect. 4. Section 5 and Sect. 6 present the semantic and the symbolic environment of epistemic ensembles. The equivalence of both semantics is shown in Sect. 7. We conclude in Sect. 8.

## 2 Epistemic Ensembles

An epistemic ensemble is formed by a collection of agents which run concurrently to accomplish a certain task. In the epistemic context collaboration of agents is achieved

by the execution of agent actions where agents inform other agents about (parts of) their knowledge, which may concern themselves, other agents or the environment. Each agent follows a certain protocol which is given by an epistemic process description. In this section we introduce the syntactic notions for building epistemic ensembles and we provide a generic operational semantics for epistemic ensembles which will be instantiated later on for executing ensembles in semantic and symbolic environments.

Epistemic formulæ. Epistemic formulæ provide the means to describe knowledge; see, e.g., [2,11,12]. An epistemic signature Σ = ( Π,A ) consists of a set Π of (atomic) propositions and a set A of agents . The set F Σ of epistemic formulæ ϕ over Σ = ( Π,A ) is defined by the following grammar:

$$\varphi \, \left \| \colon = \, p \, \right | \, \text{ true } \, \left | \, \neg \varphi \, \left | \, \varphi _ { 1 } \wedge \varphi _ { 2 } \, \right | \, K _ { a } \, \varphi \, \text{ where } p \in \Pi \text{ and } a \in A.$$

Theepistemic formula K a ϕ is to be read as 'agent a knows ϕ '. We use the usual Boolean shorthand notations like false for ¬ true , ϕ 1 ∨ ϕ 2 for ¬ ¬ ( ϕ 1 ∧¬ ϕ 2 ) , etc. Moreover, we write M a ϕ for ¬ K a ¬ ϕ ; this latter epistemic modality is dual to K a and to be read as 'agent a deems ϕ possible '. For each a ∈ A , the set F Σ /harpoonupright a of a -epistemic formulæ ϕ a having an a -modality as their top operator, is given by the following grammar:

$$\varphi _ { a } \, \vdots = \, \text{true} \ | \ \supset \varphi _ { a } \ | \ \varphi _ { a, 1 } \wedge \varphi _ { a, 2 } \ | \ K _ { a } \, \varphi \ \text{ where } \varphi \in \mathcal { F } _ { \Sigma }.$$

For any ϕ ∈ F Σ the set of possible agents of ϕ is given by ags Σ ( ϕ ) = { a ∈ A | ϕ ∈ F Σ /harpoonupright a } . In our setting, ags Σ ( ϕ ) is either a singleton or A (if no K a occurs in ϕ ).

Example 1. Our running example is inspired by [22]. We consider a set of two agents A 2 = { 1 2 , } each one holding a bit x i ∈ Π 2 = { x 1 , x 2 } . The epistemic signature is Σ 2 = ( Π ,A 2 2 ) . In a situation where x 1 is true, the 1 -formula K 1 x 1 expresses that agent 1 knows this. The 2 -formula K 2 x 1 ∨ K 2 ¬ x 1 says that agent 2 knows the value of x 1 but we cannot infer its concrete value. The 1 -formula ¬ K 1 ( K 2 x 1 ∨ K 2 ¬ x ) 1 expresses that agent 1 does not know whether agent 2 knows the value of x 1 .

Epistemic ensemble signatures. Our formalisation of epistemic ensembles is based on the notion of an epistemic ensemble signature ˇ Σ = ( Σ, (N ) a a ∈ A ) consisting of an epistemic signature Σ = ( Π,A ) and an A -family (N ) a a ∈ A of pairwise disjoint sets N a of agent action symbols , briefly called agent actions . Each set N a determines which actions are possible for agent a . We write ⋃ N for ⋃ a ∈ A N a and for each η ∈ ⋃ N we set ags ˇ Σ ( η ) = { a } if η ∈ N a .

Example 2. Continuing Ex. 1 we introduce an action stop and two actions tell 12(x ) 1 and tell 12( ¬ x ) 1 for agent 1 , i. e., N 2 , 1 = { stop , tell 12(x ) 1 , tell 12( ¬ x ) 1 } , the latter two to express that agent 1 tells the value of x 1 to agent 2 but, in each case, the information transfer is unreliable since agent 2 maybe too far away. On the other hand, agent 2 (when it got the value of x 1 ) may acknowledge in a reliable way the reception with the action ack 21( x 1 ) , i. e., N 2 , 2 = { ack 21( x 1 ) } .

General assumption. In the sequel, we always assume given an epistemic ensemble signature ˇ = ( Σ Σ, (N ) a a ∈ A ) with underlying epistemic signature Σ = ( Π,A ) .

↦

$$\eta. P \xrightarrow { \text{true:\eta} } _ { \tilde { \Sigma } } P & & \frac { P \xrightarrow { \hat { \varphi } \cdot \eta } _ { \tilde { \Sigma } } P ^ { \prime } } { \varphi \supset P \xrightarrow { \hat { \varphi } \cdot \eta } _ { \tilde { \Sigma } } P ^ { \prime } } \\ \frac { P _ { \ell } \xrightarrow { \hat { \varphi } \cdot \eta } _ { \tilde { \Sigma } } P ^ { \prime } _ { \ell } } { P _ { 1 } + P _ { 2 } \xrightarrow { \hat { \varphi } \cdot \eta } _ { \tilde { \Sigma } } P ^ { \prime } _ { \ell } } & & \text{ for } \ell \in \{ 1, 2 \} & & \frac { P \{ X \mapsto \mu X \,. \, P \} \xrightarrow { \hat { \varphi } \cdot \eta } _ { \tilde { \Sigma } } P ^ { \prime } } { \mu X \,. \, P \xrightarrow { \hat { \varphi } \cdot \eta } _ { \tilde { \Sigma } } P ^ { \prime } } \\ & & \text{Table 1. Rules for enlistemic nprocesses}$$

Table 1. Rules for epistemic processes

Epistemic processes. We consider an epistemic process language for describing the behaviour of agents which participate in an epistemic ensemble. The set P ˇ Σ of epistemic processes P over ˇ Σ is defined by the grammar

$$P \, \colon = \, 0 \, \left | \, \eta. P \, \right | \, \varphi \supset P \, \right | \, P _ { 1 } + P _ { 2 } \, \left | \, \mu X \,. \, P \, \right | \, X$$

where 0 represents the inactive process, η.P prefixes P with an agent action η ∈ ⋃ N , ϕ ⊃ P is a guarded process with condition ϕ ∈ F Σ , P 1 + P 2 denotes the nondeterministic choice between processes P 1 and P 2 , µX . P is a recursive process, and X is a process variable typically used in recursive process definitions.

The operational semantics of epistemic processes is given by conditional transitions P ↪ ̂ ϕ η : - -→ ˇ Σ P ′ relating a process P via a guard ̂ ϕ ∈ F Σ and an agent action η ∈ ⋃ N with another process P ′ . The transitions are defined inductively by the rules in Tab. 1, where successive guards are conjoined and true represents the empty guard.

Epistemic processes are used to describe the behaviour of single agents. But not any process expression in P ˇ Σ is meaningful for any agent. For instance, a process η. 0 can be carried out by an agent a only if the action symbol η represents an action of a , i. e., η ∈ N a . For any process P ∈ P ˇ Σ the set ags ˇ Σ ( P ) of agents that are allowed to execute P is inductively defined by

$$& \ a g s _ { \hat { \Sigma } } ( 0 ) = A & \ a g s _ { \hat { \Sigma } } ( \eta. P ) = \ a g s _ { \hat { \Sigma } } ( \eta ) \cap \ a g s _ { \hat { \Sigma } } ( P ) \\ & \ a g s _ { \hat { \Sigma } } ( \varphi \supset P ) = \ a g s _ { \hat { \Sigma } } ( \varphi ) \cap \ a g s _ { \hat { \Sigma } } ( P ) & \ a g s _ { \hat { \Sigma } } ( P _ { 1 } + P _ { 2 } ) = \ a g s _ { \hat { \Sigma } } ( P _ { 1 } ) \cap \ a g s _ { \hat { \Sigma } } ( P _ { 2 } ) \\ & \ a g s _ { \hat { \Sigma } } ( \mu X \,. \, P ) = \ a g s _ { \hat { \Sigma } } ( P ) & \ a g s _ { \hat { \Sigma } } ( X ) = A$$

For executing a process P ∈ P ˇ Σ the following kind of subject reduction holds:

$$\text{Lemma} \, 1. \, \text{If} \, P \stackrel { \widehat { \varphi } \colon \eta } { \longrightarrow } _ { \Sigma } P ^ { \prime }, \, \text{then} \, \text{ags} _ { \Sigma } ( P ) \subseteq \text{ags} _ { \Sigma } ( \widehat { \varphi } ) \cap \text{ags} _ { \Sigma } ( \eta ) \cap \text{ags} _ { \Sigma } ( P ^ { \prime } ).$$

Epistemic ensembles. Now we have all ingredients to define epistemic ensembles as families of epistemic agent processes. Formally, an epistemic ensemble over ˇ Σ is given by a family /vector E = ( a : P a ) a ∈ A such that, for each a ∈ A P , a is an epistemic process in P ˇ Σ with a ∈ ags ˇ Σ ( P a ) , i. e., a is allowed to perform P a .

For notational reasons and for defining the operational semantics of ensembles, we also consider (sub-)families ( a : P a ) a ∈ G of agent processes with G ⊆ A ; their composition ( a 1 : P a 1 ) a 1 ∈ G 1 ‖ ( a 2 : P a 2 ) a 2 ∈ G 2 for disjoint G , G 1 2 ⊆ A as the family ( a : P a ) a ∈ G 1 ∪ G 2 ; and, for i ∈ A , the singleton i : P i which stands for ( a : P a ) a ∈{ } i .

$$\neg K _ { 1 } K _ { 2 } x _ { 1 } \wedge K _ { 1 } \neg x _ { 1 } \colon t e l l 1 2 ( \neg x _ { 1 } ) \\ \neg K _ { 1 } K _ { 2 } x _ { 1 } \wedge K _ { 1 } x _ { 1 } \subset \underbrace { \underbrace { \underbrace { \underbrace { \underbrace { 1 \colon A g 1 } } } } { 1 \colon A g 1 } \| 2 \colon A g 2 } \underbrace { K _ { 1 } K _ { 2 } x _ { 1 } \colon s t o p } { 1 \colon 0 \| 2 \colon A g 2 } \\ K _ { 2 } x _ { 1 } \colon a c k 2 1 ( x _ { 1 } ) \left \| \underbrace { K _ { 2 } x _ { 1 } \colon a c k 2 1 ( x _ { 1 } ) } { 1 \colon A g 1 } \| 2 \colon 0 \right \| \underbrace { K _ { 1 } K _ { 2 } x _ { 1 } \colon s t o p } { 1 \colon 0 \| 2 \colon 0 } \right \| \\ \neg K _ { 1 } K _ { 2 } x _ { 1 } \wedge K _ { 1 } \neg x _ { 1 } \colon t e l l 1 2 ( \neg x _ { 1 } ) \\ \text{Fig. 1. Transition system for the syntactic bit transmission ensemble.}$$

Fig. 1. Transition system for the syntactic bit transmission ensemble.

Example 3. Relying on the epistemic ensemble signature developed in Ex. 1 and Ex. 2, we consider the following simple epistemic ensemble Sys with two processes Ag1 for agent 1 and Ag2 for agent 2 . In the process descriptions we abbreviate, for each a ∈ { 1 2 , } , the formula K a x 1 ∨ K a ¬ x 1 by K a x 1 ( x 1 written in italics).

$$a \subset \{ 1, 2 \}, \, \text{$one$ formula $\tilde{ }omega_{a}x_{1} \vee \tilde{ }omega_{a} \neg x_{1}$} \, \text{$oy $\tilde{ }omega_{a}x_{1} (x_{1}$ written in names)}. \\ A g 1 & = \mu X \,. \, ( \neg K _ { 1 } K _ { 2 } x _ { 1 } \supset ( K _ { 1 } x _ { 1 } \supset t e l l 1 2 ( x _ { 1 } ). X + \\ K _ { 1 } \neg x _ { 1 } \supset t e l l 1 2 ( \neg x _ { 1 } ). X ) + \\ K _ { 1 } K _ { 2 } x _ { 1 } \supset s t o p. 0 ) \\ A g 2 & = K _ { 2 } x _ { 1 } \supset a c k 2 1 ( x _ { 1 } ). 0 \\ S y s & = 1 \, \colon A g 1 \, \| \, 2 \, \colon A g 2$$

By tell 12(x ) 1 and tell 12( ¬ x ) 1 agent 1 repeatedly 'tells' agent 2 the value of x 1 (in an unreliable way) until it is sure that agent 2 knowsthevalue; whenhavingindeedlearntthe value of x 1 , agent 2 acknowledges this fact (in a reliable way) to agent 1 with ack 21( x 1 ) .

The syntactic operational semantics of epistemic ensembles is given by conditional transitions ↪ -→ ˇ Σ relating an ensemble /vector E via a guard ̂ ϕ ∈ F Σ and an agent action η with another ensemble /vector E ′ according to the following rule which is based on the rules for processes:

$$( * ) \ i \colon P _ { i } \, \| \, \vec { E } \overset { \widehat { \varphi } \colon \eta } { \longleftrightarrow } _ { \hat { \Sigma } } i \colon P _ { i } ^ { \prime } \, \| \, \vec { E } \ \text{ if } P _ { i } \overset { \widehat { \varphi } \colon \eta } { \longleftrightarrow } _ { \hat { \Sigma } } P _ { i } ^ { \prime }$$

Note that each ensemble step is well-defined, since i ∈ ags ˇ Σ ( P i ) implies i ∈ ags ˇ Σ ( P ′ i ) by Lem. 1, and thus i : P ′ i ‖ /vector E is again an ensemble. Moreover, the ordering of processes in an ensemble is irrelevant since they are families, i.e., functions mapping agents to processes.

Therule ( ∗ ) is formulated in a generic way without considering evaluations of guards and effects of actions. It provides, however, a convenient basis for concrete instantiations.

Example 4. Figure 1 depicts the conditional transitions of the bit transmission protocol in Ex. 3.

## 3 Dynamic Epistemic Ensemble Logic

So far we have considered a constructive approach for representing epistemic ensembles with local processes for each agent. We are now interested in a declarative language for expressing and specifying behavioural properties of epistemic ensembles from a global perspective. For this purpose we use formulæ in the style of propositional dynamic logic where regular expressions of agent actions, called compound ensemble actions, are used as modalities. In contrast to local agent processes, we have now a global view where actions of different agents can be combined.

The set C ˇ Σ of compound ensemble actions over ˇ Σ is defined by the following grammar:

$$\lambda \, \colon = \, \eta \ | \ \varphi? \ | \ \lambda _ { 1 } + \lambda _ { 2 } \ | \ \lambda _ { 1 } ; \lambda _ { 2 } \ | \ \lambda ^ { * } \ \text{ where } \eta \in \bigcup N \text{ and } \varphi \in \mathcal { F } _ { \Sigma }.$$

Besides agent actions the compound ensemble actions include a test ϕ ? on an epistemic formula ϕ ∈ F Σ , non-deterministic choices λ 1 + λ 2 of compound ensemble actions λ 1 and λ 2 , sequential compositions λ 1 ; λ 2 , and sequential loops λ ∗ .

Following the style of propositional dynamic logic the set D ˇ Σ of epistemic ensemble formulæ over ˇ Σ is defined by the following grammar where compound ensemble actions are used as modalities:

$$\psi \, \left \| \colon = \, \text{true} \ | \ \varphi \ | \ \neg \psi \ | \ \psi _ { 1 } \wedge \psi _ { 2 } \ | \ [ \lambda ] \psi \ \text{ where } \varphi \in \mathcal { F } _ { \Sigma } \ \text{and} \, \lambda \in \mathcal { C } _ { \Sigma }.$$

The formula [ λ ψ ] is to be read as 'after all possible executions of the compound action λ formula ψ holds'. We use the usual abbreviations like false or ∨ as before, and we write 〈 λ ψ 〉 for ¬ [ λ ] ¬ ψ ; this latter dynamic modality is dual to [ λ ] and to be read as 'there is some execution of λ such that ψ holds afterwards'.

Example 5. For our two agent system we are interested in the following properties, in which we abbreviate the compound action stop + tell 12(x )+ 1 tell 12( ¬ x )+ 1 ack 21( x 1 ) by ' some ':

- 1. 'As long as agent 1 does not know that agent 2 knows the value of x 1 the ensemble will not stop': [ some ∗ ] ¬ K K 1 2 x 1 →〈 some 〉 true
- 2. 'Whenever agent 1 tells the value of x 1 to agent 2 , it is possible that agent 2 will eventually know the value': [ some ∗ ; ( tell 12(x ) + 1 tell 12( ¬ x ))] 1 〈 some ∗ 〉 K 2 x 1

We cannot provide a formal satisfaction relation here saying when an epistemic ensemble satisfies an epistemic ensemble formula, since we cannot talk yet about satisfaction of ensemble formulæ as long as we do not have a concrete formalisation of epistemic states and of the effect of agent actions on them. But we can already now provide a definition to capture, for each compound ensemble action λ , which sequences σ = ( ̂ ϕ 1 : η /epsilon1 1 ) . . . ( ̂ ϕ k : η /epsilon1 k ) of guard and agent action pairs can be executed when moving stepwise from an ensemble /vector E to an ensemble /vector E ′ in accordance with rule ( ∗ ) from above. Thereby concatenation of such two sequences σ 1 and σ 2 is denoted by σ 1 · σ 2 and /epsilon1 denotes an artificial empty agent action. The inductive rules in Tab. 2 define when a (stepwise) move ( /vector E,σ, /vector E ′ ) is a witness for a compound ensemble action λ , written ( /vector E,σ, /vector E ′ ) :: λ .

$$( \vec { E }, \widehat { \varphi } \, \colon \, \eta, \vec { E } ^ { \prime } ) \, \left \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \ \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \    \, \\ \frac { ( \vec { E }, \sigma, \vec { E } ^ { \prime } ) \, \left \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \left \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \    \left \| \, } { ( \vec { E }, \sigma, \vec { E } ^ { \prime } ) \, \left \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \,    \left \| \, } { ( \vec { E }, \sigma, \vec { E } ^ { \prime } ) \, \left \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right\| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \|\, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \, \right \| \,    \left \| \, } { \text{Table 2. Rules for witnessing\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\} }$$

Table 2. Rules for witnessing compound ensemble actions

## 4 Action Models for Agent Actions

Going to a concrete interpretation of ensembles a crucial step is to assign meaning to the agent actions occurring in an epistemic ensemble signature. A direct way would be to fix a domain for modelling states and to associate to each agent action η a relation (or a proper function) which models the effect of η . This has been done, for instance, in [12] who associate to (joint) agent actions a so-called 'global state transformer'. In our approachwe pursue a different approach and use the notion of 'action model' introduced in [1] to provide meaning for agent actions. The advantage is that action models still have a syntactic flavour and thus are still independent of the particular denotations used for epistemic states. Most approaches use action models in the context of Kripke structures as mathematical objects for epistemic states on which updates caused by actions are defined. But, in principle, action models allow also other domains for interpretation. For instance, in [14] we have provided an interpretation using symbolic states. Therefore, our idea is here to use action models as an intermediate step to assign an 'abstract' interpretation to agent actions. Then we will consider two concrete frameworks (a Kripke style and a symbolic approach) where updates caused by action model applications are uniquely determined.

An action model U = ( Q,F, pre ) over an epistemic signature Σ = ( Π,A ) consists of a set Q of events , an A -family F = ( F a ⊆ Q × Q ) a ∈ A of action accessibility relations F a , and an action precondition function pre : Q → F Σ . We assume that the accessibility relations F a are equivalences. For any agent a ∈ A , ( q, q ′ ) ∈ F a models that a cannot distinguish between occurrences of events q and q ′ . For any event q ∈ Q , the epistemic formula pre ( q ) determines a condition under which q can happen. An epistemic action u = ( U, q ) is a pointed action model which selects an actual event q ∈ Q . We set F ( u ) a = { q ′ ∈ Q | ( q, q ′ ) ∈ F a } for a ∈ A , and write pre ( u ) for pre ( q ) and u · q ′ for ( U, q ′ ) when q ′ ∈ Q . The class of epistemic actions over Σ is denoted by U Σ . The set of possible agents for an epistemic action u ∈ U Σ is defined by ags Σ ( u ) = ags Σ ( pre ( u )) . The idea is that an action η ∈ N a of an agent a should only be interpreted by an epistemic action whose precondition is an a -formula.

Example 6. A group announcement of a formula ϕ ∈ F Σ to a group A ∗ ⊆ A of agents is modelled by the epistemic action ( U grp ( A , ϕ , ∗ ) k ) graphically represented as

![image](https://ac.marcodsn.me/arxiv-markdown-images/2408.01115v1-figure-2867980d-5b2d-4bf6-97cd-f572a6596891.jpg)

The action model U grp ( A , ϕ ∗ ) has two events k and n . Event k represents the announcement of ϕ which should only happen if ϕ holds and therefore pre grp ,ϕ ( k ) = ϕ ; only agents in the group A ∗ can recognise this event. All other agents consider it possible that nothing happened which is represented by n having no proper precondition, i.e., pre grp ,ϕ ( n ) = true . The possible agents of ( U grp ( A , ϕ , ∗ ) k ) are given by ags Σ ( ϕ ) , the possible agents of ( U grp ( A , ϕ , ∗ ) n ) are ags Σ (true) = A .

Epistemic choice actions. We also consider non-deterministic epistemic actions, similarly to [11]. They model alternatives which are not under the control of an agent but are selected by the environment. Formally, an epistemic choice action over Σ is a finite, non-empty set α ⊆ U Σ of epistemic actions. The class of epistemic choice actions over Σ is denoted by A Σ . The possible agents of an α ∈ A Σ are ags Σ ( α ) = ⋂ u ∈ α ags Σ ( u ) .

Example 7. For agents a, a ′ ∈ A , the epistemic choice action

$$\ s n d _ { \text{los} } ^ { a \rightarrow a ^ { \prime } } ( \varphi _ { a } ) = \{ ( U _ { g r p } ( \{ a ^ { \prime } \}, \varphi _ { a } ), \text{k} ), ( U _ { g r p } ( \{ a ^ { \prime } \}, \varphi _ { a } ), \text{n} ) \}$$

models a lossy sending of the information ϕ a ∈ F Σ /harpoonupright a from a to agent a ′ , in the sense that afterwards a ′ may know ϕ a if a ′ is aware of the announcement (modelled by U grp ( { a ′ } , ϕ a ) , k ) ), but need not if the announcement is lost (modelled by U grp ( { a ′ } , ϕ a ) , n ) ). In any case, a cannot recognise whether the announcement was successful. Similarly, a reliable sending is defined by the (singleton) choice action snd a → a ′ rel ( ϕ a ) = { ( U grp ( { a, a ′ } , ϕ a ) , k ) } which is modelled by a group announcement of ϕ a such that both agents recognise that the message did work. It holds that ags Σ ( snd a → a ′ los ( ϕ a )) = ags Σ ( snd a → a ′ rel ( ϕ a )) = { a . }

Let us now come back to our epistemic ensemble signature ˇ = ( Σ Σ, (N ) a a ∈ A ) with Σ = ( Π,A ) . An epistemic action interpretation for the agent actions in ⋃ N is a function act : ⋃ N →A Σ such that for all a ∈ A and η ∈ N a it holds a ∈ ags Σ ( act ( η )) .

Example 8. For the agent actions in Ex. 2 we use the epistemic action interpretation act 2 with act 2 ( tell 12(x )) 1 = snd 1 → 2 los ( K 1 x ) 1 , act 2 ( tell 12( ¬ x )) 1 = snd 1 → 2 los ( K 1 ¬ x ) 1 } and act 2 ( stop ) = ( U grp ( { 1 2 , } , true) , k ) is the group announcementof true . Moreover, act 2 ( ack 21( x 1 )) = snd 2 → 1 rel ( K 2 x 1 ) is the reliable sending from agent 2 to agent 1 that agent 2 knows the value of x 1 . (Recall that K 2 x 1 abbreviates K 2 x 1 ∨ K 2 ¬ x 1 .)

## 5 Epistemic Ensembles in a Semantic Environment

To execute an epistemic ensemble we need an environment where knowledge formulæ, in particular process guards and change of knowledge caused by agent actions, are interpreted. This section is based on the traditional possible worlds model of epistemic logic; see, e.g., [12].

Epistemic states. An epistemic structure K = ( W,E,L ) (also called Kripke model [2,11] or Kripke structure [12]) over the epistemic signature Σ = ( Π,A ) is given by a set W of worlds , an A -family E = ( E a ⊆ W × W ) a ∈ A of epistemic accessibility relations , and a labelling L : W → ℘Π which determines for each world w ∈ W the set of atomic propositions which hold in w . We assume that the accessibility relations are equivalences. For any agent a , ( w, w ′ ) ∈ E a models that agent a cannot distinguish the two worlds w and w ′ . An epistemic state K = ( K,w ) selects a world w ∈ W considered as the actual world. Thus epistemic states are pointed Kripke structures. The class of epistemic states over Σ is denoted by E Σ .

The satisfaction of an epistemic formula ϕ ∈ F Σ by an epistemic structure K = ( W,E,L ) ∈ E Σ at a world w ∈ W , written K,w | = Σ ϕ , is inductively defined by:

```
\langle \cdot \cdot, \varepsilon, \varepsilon / \varsigma \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \colon \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \, \nu, \nu \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \ \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \delta \, \nu, \nu \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot                                                                                                                                                                                                         \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \ddot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot        \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot           \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot              \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot                 \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot                    \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot                       \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot                          \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot                             \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot                                \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot                                   \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot                                      \rangle \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \
```

Hence, an agent a knows ϕ at point w if ϕ holds in all worlds w ′ which a cannot distinguish from w . For an epistemic state K = ( K,w ) ∈ E Σ and for ϕ ∈ F Σ , we define K | = ϕ by K,w | = ϕ and for Φ ⊆ F Σ we define K | = Φ by K | = Σ ϕ for all ϕ ∈ Φ . A formula ϕ ∈ F Σ is a logical consequence of Φ ⊆ F Σ , written Φ | = Σ ϕ , if K | = Σ ϕ for all K with K | = Σ Φ . We write | = Σ ϕ for ∅ | = Σ ϕ , i. e., ϕ is a tautology .

Example 9. The following diagram represents graphically an epistemic state K 0 = ( K ,w 0 0 ) in which x 1 is true and agent 1 knows this, but agent 2 does not. Indeed, agent 2 cannot distinguish between the actual world w 0 and the possible world w 1 . The self-loops represent reflexivity of the accessibility relations. Note that K 0 | = Σ 2 K 1 x 1 , K 0 | = Σ 2 ¬ K 2 x 1 , and K 0 | = Σ 2 K 1 ¬ K 2 x 1 .

![image](https://ac.marcodsn.me/arxiv-markdown-images/2408.01115v1-figure-fb5ecc19-fdd8-41a5-a745-182348204af4.jpg)

A state K ′ 0 with K ′ 0 | = Σ K 1 ¬ x 1 and K ′ 0 | = Σ K 1 ¬ K 2 ¬ x 1 is obtained by reversing the labelling of K 0 .

Epistemic updates. The product update ( W,E,L ) /triangleleft Σ ( Q,F, pre ) of an epistemic structure K = ( W,E,L ) and an action model U = ( Q,F, pre ) over Σ = ( Π,A ) yields the epistemic structure ( W ,E ,L ′ ′ ′ ) with

$$1, a n d$$

$$& W ^ { \prime } = \left \{ ( w, q ) \in W \times Q \, | \, K, w \models _ { \Sigma } p r e ( q ) \right \}, \\ & E ^ { \prime } _ { a } = \left \{ ( ( w, q ), ( w ^ { \prime }, q ^ { \prime } ) ) \, | \, ( w, w ^ { \prime } ) \in E _ { a }, \, ( q, q ^ { \prime } ) \in F _ { a } \right \} \text{for all } a \in A, \text{ and } \\ & L ^ { \prime } ( w, q ) = L ( w ) \text{ for all } ( w, q ) \in W ^ { \prime }.$$

Let K = ( K,w ) ∈ E Σ be an epistemic state and u = ( U, q ) ∈ U Σ be an epistemic action. If K | = Σ pre ( q ) then the product update K /triangleleft Σ u of K and u is defined and given by the epistemic state ( K /triangleleft Σ U, ( w, q )) ∈ E Σ .

/negationslash

Example 10. Applying ( U grp ( { 2 } , K 1 x ) 1 , k ) to the epistemic state ( K ,w 0 0 ) in Ex. 9, we obtain the epistemic state ( K , 1 ( w , 0 k )) shown, without reflexive accessibility edges, below. The world ( w , 1 k ) does not appear since ( K ,w 0 1 ) | = Σ 2 K 1 x 1 which is the precondition of k .

![image](https://ac.marcodsn.me/arxiv-markdown-images/2408.01115v1-figure-b49fd264-75b5-4bca-a2f8-2988b022fbcc.jpg)

Note that ( K , 1 ( w , 0 k )) | = Σ 2 K K 2 1 x 1 but ( K , 1 ( w , 0 k )) | = Σ 2 ¬ K K K 1 2 1 x 1 , i. e., 2 knows that 1 knows that x 1 holds, but 1 does not know that 2 knows this. If we apply the epistemic action ( U grp ( { 2 } , K 1 x ) 1 , n ) to ( K ,w 0 0 ) , we obtain the epistemic state ( K , 1 ( w , 0 n )) . Note that ( K , 1 ( w , 0 n )) = | Σ 2 ¬ K K 2 1 x 1 .

Semanticenvironments. In contrast to [13,14] we consider here not only single epistemic states K ∈ E Σ as semantic environmentsbut, more generally,non-emptyclasses K ⊆ E Σ of epistemic states; the class of all non-empty classes of epistemic states is denoted by S Σ . Such classes model abstractions where different epistemic states are considered to be possible in a current environment. For each K ⊆ E Σ and ϕ ∈ F Σ define K | = Σ ϕ as K | = Σ ϕ for all K ∈ K , and for each u ∈ U Σ define the update K /triangleleft Σ u = { K /triangleleft Σ u | K ∈ K , K | = Σ pre ( u ) } . The semantics of an epistemic choice action α ∈ A Σ is given by the relation

$$\left [ \alpha \right ] _ { \Sigma } = \left \{ \left ( \mathcal { K }, \mathcal { K } \lhd _ { \Sigma } \mathfrak { u } \right ) \in \mathcal { S } _ { \Sigma } \times \mathcal { S } _ { \Sigma } \ | \, \mathfrak { u } \in \alpha, \mathcal { K } \models _ { \Sigma } p r e ( \mathfrak { u } ) \right \}.$$

/negationslash

We require K /negationslash = ∅ because otherwise all formulæ would hold in K . Note that the semantics is well-defined, i.e., K /triangleleft Σ u = ∅ , since ∅ /negationslash = K and K | = Σ pre ( u ) hold. Let us remark that updates on a single epistemic state as considered in [13,14] and its generalisation to classes of epistemic states considered here are tightly related: For each K ∈ E Σ ,

$$\bigcup _ { u \in \alpha } \{ ( \{ \mathfrak { K } \}, \{ \mathfrak { K } \lhd _ { \Sigma } u \} ) \, | \, \mathfrak { K } \models _ { \Sigma } u \} \subseteq [ \alpha ] _ { \Sigma } \,.$$

More generally, we obtain

Lemma 2. Let K ∈ S Σ and α ∈ A Σ .

- 1. If ( { K } K , K ) ∈ /llbracket α /rrbracket Σ for some K ∈ K , then there are K ′ ∈ E Σ with K K = { K ′ } and K ∈ S ′ Σ with K ′ ∈ K ′ such that ( K K , ′ ) ∈ /llbracket α /rrbracket Σ .
- 2. If ( K K , ′ ) ∈ /llbracket α /rrbracket Σ , then for each K ′ ∈ K ′ there is some K ∈ K with ( { K } { , K ′ } ) ∈ /llbracket α /rrbracket Σ .

Ensemble configurations. We are now ready to define the execution of ensembles in semantic class environments.Given the epistemic ensemble signature ˇ = ( Σ Σ, (N ) a a ∈ A ) , an epistemic ensemble configuration over ˇ Σ is a pair ( /vector E, K ) of an ensemble over ˇ Σ and a (non-empty) class of epistemic states K ∈ S Σ . The ensemble semantics over ˇ Σ

w.r.t. an epistemic action interpretation act : ⋃ N → A Σ is the ternary relation -→ act ˇ Σ between configurations, agent actions and (successor) configurations defined by interpreting the syntactic operational ensemble semantics, given by rule ( ∗ ) in Sect. 2, in the environment of classes of epistemic states:

$$\vec { E }, \mathcal { K } \xrightarrow { \eta } _ { \vec { \Sigma } } a c t \, \vec { E } ^ { \prime }, \mathcal { K } ^ { \prime } \quad \text{if} \, \vec { E } \xrightarrow { \widehat { \varphi } \colon \eta } _ { \vec { \Sigma } } \, \vec { E } ^ { \prime }, \mathcal { K } \models _ { \Sigma } \widehat { \varphi }, \, \text{and} \, ( \mathcal { K }, \mathcal { K } ^ { \prime } ) \in [ a c t ( \eta ) ] _ { \Sigma } \\ - \quad \cdots \, \, \real - \, \dots \, \real \cdots \, \real \cdots \, \real \cdots \, \real \cdots \,.$$

Example 11. Consider the bit transmission protocol of Ex. 3 with its agent actions interpreted as in Ex. 8. As initial classes of epistemic states consider on the one hand K 0 x , 1 with all its states satisfying K 1 x 1 (as illustrated by K 0 in Ex. 9), and K 0 , ¬ x 1 with all its states satisfying K 1 ¬ x 1 (as illustrated by K ′ 0 in Ex. 9). In both cases, the value of x 2 is arbitary, as is the knowledge of the agents 1 and 2 about it. The ensemble works uniformly on K 0 x , 1 and on K 0 , ¬ x 1 . Taking an initial class of epistemic states where some states satisfy K 1 x 1 and others K 1 ¬ x 1 no transition can be taken. When starting the ensemble in a class of epistemic states all satisfying K K 1 2 x 1 , then ack 12( x 1 ) and stop can be executed.

Satisfaction of epistemic ensemble formulæ. Finally we are now also able to define when an epistemic ensemble formula (cf. Sect. 3) is satisfied by an ensemble configuration. As a preparation we define the semantics of guard-action sequences σ = ( ̂ ϕ 1 : η /epsilon1 1 ) . . . ( ̂ ϕ k : η /epsilon1 k ) relating classes of epistemic states inductively by

$$& [ \widehat { \varphi } \colon \epsilon ] ^ { a c t } _ { \dot { \Sigma } } = \{ ( \mathcal { K }, \mathcal { K } ) \in \mathcal { S } _ { \Sigma } \times \mathcal { S } _ { \Sigma } \, | \, \mathcal { K } \models _ { \Sigma } \widehat { \varphi } \} \,, \\ & [ \widehat { \varphi } \colon \eta ] ^ { a c t } _ { \dot { \Sigma } } = \{ ( \mathcal { K }, \mathcal { K } ^ { \prime } ) \in [ a c t ( \eta ) ] ] _ { \Sigma } \, | \, \mathcal { K } \models _ { \Sigma } \widehat { \varphi } \} \,, \\ & [ \sigma _ { 1 } \cdot \sigma _ { 2 } ] ^ { a c t } _ { \dot { \Sigma } } = [ \sigma _ { 1 } ] ] ^ { a c t } _ { \dot { \Sigma } } ; [ \sigma _ { 2 } ] ^ { a c t } _ { \dot { \Sigma } } \quad ( \text{relational composition} )$$

$$\left [ \sigma _ { 1 } \cdot \sigma _ { 2 } \right ] _ { \check { \Sigma } } ^ { a c t } = \left [ \sigma _ { 1 } \right ] _ { \check { \Sigma } } ^ { a c t } ; \left [ \sigma _ { 2 } \right ] _ { \check { \Sigma } } ^ { a c t } \quad ( \text{relational composition)}$$

The semantics of a compound ensemble action λ ∈ C ˇ Σ relating ensemble configurations relies on the definition of witnesses in Sect. 3 and is given by the relation

$$\left [ \lambda \right ] ^ { a c t } _ { \vec { \Sigma } } = \left \{ \left ( ( \vec { E }, \mathcal { K } ), ( \vec { E } ^ { \prime }, \mathcal { K } ^ { \prime } ) \right ) \, | \, ( \vec { E }, \sigma, \vec { E } ^ { \prime } ) \, \left \| \colon \lambda, \, ( \mathcal { K }, \mathcal { K } ^ { \prime } ) \in \left [ \sigma \right ] ^ { a c t } _ { \vec { \Sigma } } \right \}.$$

Lemma 3. Let ( /vector E, K ) be an ensemble configuration and λ ∈ C ˇ Σ .

- 1. If (( /vector E, { K } ) , ( /vector E , ′ K K )) ∈ /llbracket λ /rrbracket act ˇ Σ for some K ∈ K , then there are K ′ ∈ E Σ with K K = { K ′ } and K ∈ S ′ Σ with K ′ ∈ K ′ such that (( /vector E, K ) , ( /vector E , ′ K ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ .
- 2. If (( /vector E, K ) , ( /vector E, K ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ , then for each K ′ ∈ K ′ there is some K ∈ K with (( /vector E, { K } ) , ( /vector E , ′ { K ′ } )) ∈ /llbracket λ /rrbracket act ˇ Σ .

The satisfaction of an epistemic ensemble formula ψ ∈ D ˇ Σ by an ensemble configuration ( /vector E, K ) w.r.t. act : ⋃ N →A Σ is inductively defined along the form of ψ :

- ( /vector E, K | ) = act ˇ ϕ ⇐⇒ K | = Σ ϕ

$$( \vec { E }, \mathcal { K } ) \models _ { \vec { \Sigma } } ^ { a c t } \, \varphi & \Longleftrightarrow \, \mathcal { K } \models _ { \Sigma } \varphi \\ ( \vec { E }, \mathcal { K } ) \models _ { \vec { \Sigma } } ^ { a c t } \, \text{true} \\ ( \vec { E }, \mathcal { K } ) \models _ { \vec { \Sigma } } ^ { a c t } \, \neg \psi & \Longleftrightarrow \, \text{not} \, ( \vec { E }, \mathcal { K } ) \models _ { \vec { \Sigma } } ^ { a c t } \, \psi$$

$$( \vec { E }, \mathcal { K } ) \models _ { \Sigma } ^ { a c t } \, \psi _ { 1 } \wedge \psi _ { 2 } \, \Longleftrightarrow \, ( \vec { E }, \mathcal { K } ) \models _ { \Sigma } ^ { a c t } \, \psi _ { 1 } \, \text{and} \, ( \vec { E }, \mathcal { K } ) \models _ { \Sigma } ^ { a c t } \, \psi _ { 2 } \\ ( \vec { E }, \mathcal { K } ) \models _ { \Sigma } ^ { a c t } \, [ \lambda ] \psi \, \Longleftrightarrow \, ( \vec { E } ^ { \prime }, \mathcal { K } ^ { \prime } ) \models _ { \Sigma } ^ { a c t } \, \psi \\ & \quad \text{for all} \, ( \vec { E } ^ { \prime }, \mathcal { K } ^ { \prime } ) \, \text{such that} \, ( ( \vec { E }, \mathcal { K } ), ( \vec { E } ^ { \prime }, \mathcal { K } ^ { \prime } ) ) \in [ \lambda ] _ { \Sigma } ^ { a c t }$$

$$\tilde { \Sigma }$$

Example 12. Theensemble configuration ( Sys , K 0 x , 1 ) for the bit transmission ensemble Sys from Ex. 3 and the class of epistemic states K 0 x , 1 fromEx. 11 satisfies both dynamic ensemble formulæ of Ex. 5; the same is true for ( Sys , K 0 x , 1 ) .

Proposition 1. Let ( /vector E, K ) be an ensemble configuration. For all ψ ∈ D ˇ Σ it holds that ( /vector E, K | ) = act ˇ Σ ψ if, and only if, ( /vector E, { K } ) = | act ˇ Σ ψ for all K ∈ K .

## 6 Epistemic Ensembles in a Symbolic Environment

We are now going to execute ensembles in a symbolic environment which allows for a more compact representation of epistemic states represented by sets of epistemic formulæ, i.e., knowledge bases. For doing this we extend the approach of [14] to deal with ensembles. A symbolic epistemic signature ( Σ,Φ ) extends the epistemic signature Σ = ( Π,A ) by a finite set of epistemic formulæ Φ ⊆ F Σ which are in the focus of evaluation. Focusing to a finite set allows for effective computations and decisions.

Symbolic epistemic states. A symbolic epistemic state over ( Σ,Φ ) is a subset Γ ⊆ Φ which is true -closed , i. e., if true ∈ Φ , then true ∈ Γ . (If true ∈ Φ , but true / Γ ∈ , this would mean that we consider true not to hold.). The set of symbolic epistemic states over ( Σ,Φ ) is denoted by S Φ Σ .

The Boolean closure bcl ( Φ ) of Φ consists of the epistemic formulæ φ defined by

$$\phi \, \colon = \, \varphi \ | \, \text{ true }$$

The symbolic satisfaction relation Γ | = Φ Σ φ between symbolic states Γ ∈ S Φ Σ and formulæ φ ∈ bcl ( Φ ) is defined as:

$$\begin{array} {$$

Symbolic epistemic updates. Let u ∈ U Σ be an epistemic action and ϕ ∈ F Σ . A formula ρ ∈ F Σ is a weakest liberal precondition of u for ϕ if the following holds for all K ∈ E Σ :

$$( \mathfrak { w } \mathfrak { l } p ) \ \mathfrak$$

The set of the weakest liberal precondition formulæ of u for ϕ is denoted by Wlp Σ ( u , ϕ ) . Obviously, if ρ, ρ ′ ∈ Wlp Σ ( u , ϕ ) , then | = Σ ρ ↔ ρ ′ . There is indeed, for any u ∈ U Σ and any ϕ ∈ F Σ , a formula wlp Σ ( u , ϕ ) ∈ Wlp Σ ( u , ϕ ) that can be recursively computed by

the function wlp Σ : U Σ × F Σ → F Σ defined in accordance with the reduction rules originally stated in the context of dynamic epistemic logic (DEL) in [11, pp. 162sqq.] and [2, p. 37]:

```
\begin{array} { c } \cdot \\ \ w l p _ { \Sigma }
```

The symbolic epistemic update Γ /triangleleft Φ Σ u of a symbolic epistemic state Γ ∈ S Φ Σ by an epistemic action u ∈ U Φ Σ is defined as

$$\Gamma \lhd _ { \Sigma } ^ { \Phi } \, \math$$

/negationslash

/negationslash

Symbolic environments. For an epistemic action u ∈ U Σ define Pre ( u ) = { ρ ∈ F Σ | | = Σ pre ( u ) ↔ } ρ . We say that u ∈ U Σ is Φ -representable if (1) Pre ( u ) ∩ bcl ( Φ ) = ∅ and if (2) for all ϕ ∈ Φ it holds that Wlp Σ ( u , ϕ ) ∩ bcl ( Φ ) = ∅ . The class of such epistemic actions is denoted by U Φ Σ . An epistemic choice action α ∈ A Σ is Φ -representable if all u ∈ α are Φ -representable; the class of such epistemic choice actions is denoted by A Φ Σ .

Example 13. For the scenario of Ex. 3 consider the preliminary focus formulæ Φ (0) 2 = { K 1 x 1 , K 1 ¬ x 1 , K 2 x , 1 K K 1 2 x 1 } (as before we write K a x 1 for K a x 1 ∨ K a ¬ x 1 ). The epistemic actions occuring in snd 1 → 2 los ( K 1 x ) 1 , snd 1 → 2 los ( K 1 ¬ x ) 1 , and snd 2 → 1 rel ( K 2 x 1 ) are u q ϕ = ( U grp ( { 2 } , K 1 ϕ , q ) ) for ϕ ∈ { x 1 , ¬ x 1 } , q ∈ { k n , } and u 2 = ( U grp ( { 1 2 , } , K 2 x 1 ) , k ) . All these actions have a precondition that is expressible over Φ (0) 2 . Table 3 shows possible representatives ρ satisfying | = Σ 2 wlp Σ 2 ( u , ϕ ) ↔ ρ . 3 Indeed, u 2 is not Φ (0) 2 -representable, but becomes Φ 2 -representable for Φ 2 = Φ (0) 2 ∪ { K M 1 2 x 1 , K M 1 2 ¬ x 2 } .

The symbolic semantics of a Φ -representable epistemic choice action α ∈ A Φ Σ is given by the relation

$$[ \alpha ] _ { \Sigma } ^ { \phi } = \{ ( \Gamma, \Gamma \lhd ^ { \phi } _ { \Sigma } \, \mathfrak { u } ) \in \mathcal { S } _ { \Sigma } ^ { \phi } \times \mathcal { S } _ { \Sigma } ^ { \phi } \ | \, \mathfrak { u } \in \alpha, \, \text{ex.} \, \rho \in P r e ( \mathfrak { u } ) \cap b c l ( \Phi ) \, s. t. \, \Gamma \models _ { \Sigma } ^ { \phi } \, \rho \} \.$$

A symbolic epistemic ensemble signature ( ˇ Σ,Φ ) consists of an epistemic ensemble signature ( Σ, (N ) a a ∈ A ) and a set of focus formulæ Φ such that ( Σ,Φ ) is a symbolic epistemic signature. An ensemble /vector E over ˇ Σ is an ensemble over ( ˇ Σ,Φ ) if all guards occurring in /vector E are in bcl ( Φ ) . An epistemic action interpretation act : ⋃ N →A Σ is a Φ -interpretation if act ( η ) ∈ A Φ Σ for all η ∈ ⋃ N . A symbolic epistemic ensemble configuration over ( ˇ Σ,Φ ) is a pair ( /vector E,Γ ) of an ensemble over ( ˇ Σ,Φ ) and a symbolic epistemic state Γ ∈ S Φ Σ . The symbolic ensemble semantics over ( ˇ Σ,Φ ) w.r.t. a Φ -interpretation

3 Computed with a small Maude tool available at https://github.com/AlexanderKnapp/epistemic.git .

Table 3. Representatives ρ satisfying | = Σ 2 wlp Σ ( u , ϕ ) ↔ ρ

| ϕ u           | u k x 1               | u k ¬ x 1               | u n x 1                   | u n ¬ x 1                 | u 2                     |
|---------------|-----------------------|-------------------------|---------------------------|---------------------------|-------------------------|
| K 1 x 1       | true                  | ¬ K 1 ¬ x 1             | K 1 x 1                   | K 1 x 1                   | K 2 x 1 → K 1 M 2 x 1   |
| K 1 ¬ x 1     | ¬ K 1 x 1             | true                    | K 1 ¬ x 1                 | K 1 ¬ x 1                 | K 2 x 1 → K 1 M 2 ¬ x 1 |
| K 2 x 1       | true                  | true                    | K 2 x 1                   | K 2 x 1                   | true                    |
| K 1 K 2 x 1   | K 1 x 1 → K 1 K 2 x 1 | K 1 ¬ x 1 → K 1 K 2 x 1 | K 1 K 2 x 1               | K 1 K 2 x 1               | true                    |
| K 1 M 2 x 1   | true                  | ¬ K 1 ¬ x 1             | K 1 M 2 x 1               | ¬ K 1 ¬ x 1 ∧ K 1 M 2 x 1 | K 2 x 1 → K 1 M 2 x 1   |
| K 1 M 2 ¬ x 1 | ¬ K 1 x 1             | true                    | ¬ K 1 x 1 ∧ K 1 M 2 ¬ x 1 | K 1 M 2 ¬ x 1             | K 2 x 1 → K 1 M 2 ¬ x 1 |

act : ⋃ N →A Φ Σ is the ternary relation -→ act ˇ Σ,Φ between symbolic configurations, agent actions and (successor) configurations defined by interpreting the operational ensemble semantics, given by rule ( ∗ ) in Sect. 2, in the environment of symbolic epistemic states:

$$\vec { E }, \Gamma \xrightarrow { \eta } _ { \vec { \Sigma }, \phi } a c t \, \vec { E } ^ { \prime }, \Gamma ^ { \prime } \text{ \ if } \vec { E } \xrightarrow { \hat { \phi } \colon \eta } _ { \vec { \Sigma } } \vec { E } ^ { \prime }, \Gamma \models _ { \Sigma } ^ { \phi } \widehat { \phi }, \text{and} \left ( \Gamma, \Gamma ^ { \prime } \right ) \in \left [ a c t ( \eta ) \right ] _ { \Sigma } ^ { \phi }$$

Satisfaction of epistemic ensemble formulæ. The symbolic semantics of a guard-agent action sequence σ = ( ̂ φ 1 : η /epsilon1 1 ) . . . ( ̂ φ k : η /epsilon1 k ) with all guards ̂ φ i formulæ in bcl ( Φ ) w.r.t. the Φ -interpretation act is inductively given by

$$\underbrace { \left [ \widehat { \phi } \colon \epsilon \right ] _ { \Sigma, \Phi } ^ { a c t } = \left \{ ( \Gamma, \Gamma ) \in ( \mathcal { S } _ { \Sigma } ^ { \Phi } ) ^ { 2 } \, | \, \Gamma \models _ { \Sigma } ^ { \Phi } \, \widehat { \phi } \right \} } \,, \\ \underbrace { \_ \sim } \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \delta \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dists \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dts \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dclots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \ dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \ Dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \Dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \ddots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \ \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \, \dots \
\end{$$

$$\left [ \sigma _ { 1 } \cdot \sigma _ { 2 } \right ] _ { \check { \Sigma }, \Phi } ^ { a c t } = \left [ \sigma _ { 1 } \right ] _ { \check { \Sigma }, \Phi } ^ { a c t } ; \left [ \sigma _ { 2 } \right ] _ { \check { \Sigma }, \Phi } ^ { a c t } \quad ( \text{relational composition} )$$

$$& [ \widehat { \phi } \colon \eta ] _ { \widehat { \Sigma }, \Phi } ^ { a c t } = \{ ( \Gamma, \Gamma ^ { \prime } ) \in [ \begin{matrix} a c t ( \eta ) \end{matrix} ] _ { \Sigma } ^ { \Phi } & | \, \Gamma \models _ { \Sigma } ^ { \Phi } \, \widehat { \phi } \} \,, \\ & \pi \quad \ n a c t \quad \pi \quad \ n a c t \quad \pi \quad \ n a c t \quad \lambda \, \cdots \, \cdots \, \cdots$$

The set of compound ensemble actions λ ∈ C ˇ Σ with all tests in λ formulæ in bcl ( Φ ) is denoted C Φ ˇ Σ . The semantics of a λ ∈ C Φ ˇ Σ w.r.t. act is given by the relation

$$\left [ \lambda \right ] ^ { a c t } _ { \tilde { \Sigma }, \Phi } = \left \{ \left ( ( \vec { E }, \Gamma ), ( \vec { E } ^ { \prime }, \Gamma ^ { \prime } ) \right ) \, | \, ( \vec { E }, \sigma, \vec { E } ^ { \prime } ) \, \left \| \colon \lambda, \, ( \Gamma, \Gamma ^ { \prime } ) \in \left [ \sigma \right ] ^ { a c t } _ { \tilde { \Sigma }, \Phi } \right \}.$$

The epistemic ensemble formulæ D Φ ˇ Σ over ( ˇ Σ,Φ ) are the epistemic ensemble formulæ over ˇ Σ that only contain sub-formulæ φ ∈ F Σ that are in bcl ( Φ ) . The satisfaction of a ψ ∈ D Φ ˇ Σ by a symbolic epistemic ensemble configuration ( /vector E,Γ ) w.r.t. Φ -interpretation act : ⋃ N →A Φ Σ is inductively defined along the structure of ψ :

$$( \vec { E }, \Gamma ) \models _ { \vec { \Sigma }, \Phi } ^ { a c t } \, \phi \, \Longleftrightarrow \, \Gamma \models _ { \Sigma } ^ { \Phi } \, \phi$$

- ( /vector E,Γ ) = | act ˇ Σ,Φ true

$$( \vec { E }, \Gamma ) \models _ { \check { \Sigma }, \Phi } ^ { a c t } \neg \psi \iff \text{not} \, ( \vec { E }, \Gamma ) \models _ { \check { \Sigma }, \Phi } ^ { a c t } \, \psi$$

- ( /vector E,Γ ) = | act ˇ ψ 1 ∧ ψ 2 ⇐⇒ ( /vector E,Γ ) = | act ˇ ψ 1 and ( /vector E,Γ ) = | act ˇ ψ 2

Σ,Φ

$$( \dot { E }, \Gamma ) \models _ { \dot { \Sigma }, \Phi } ^ { a c t } \, \psi _ { 1 } \wedge \psi _ { 2 } \, \Longleftrightarrow \, ( \dot { E }, \Gamma ) \models _ { \dot { \Sigma }, \Phi } ^ { a c t } \, \psi _ { 1 } \, \text{and} \, ( \dot { E }, \Gamma ) \models _ { \dot { \Sigma }, \Phi } ^ { a c t } \, \psi _ { 2 } \\ ( \vec { E }, \Gamma ) \models _ { \dot { \Sigma }, \Phi } ^ { a c t } \, [ \lambda ] \psi \, \Longleftrightarrow \, ( \vec { E } ^ { \prime }, \Gamma ^ { \prime } ) \models _ { \dot { \Sigma }, \Phi } ^ { a c t } \, \psi \\ & \text{for all} \, ( \vec { E } ^ { \prime }, \Gamma ^ { \prime } ) \text{ such that} \, ( ( \vec { E }, \Gamma ), ( \vec { E } ^ { \prime }, \Gamma ^ { \prime } ) ) \in [ \lambda ] _ { \dot { \Sigma }, \Phi } ^ { a c t }$$

## 7 Relating Ensembles in Semantic and Symbolic Environments

We are now interested in relating ensembles which are executed in a semantic and in a symbolic environment. We first introduce a notion of equivalence between semantic and symbolic states and then lift this equivalence to ensemble configurations. Our main theorem states that both simulate each other and consequently equivalent configurations satisfy the same dynamic epistemic ensemble logic formulæ.

Epistemic state equivalence. Wesaythat an epistemic state class K ∈ S Σ and a symbolic epistemic state Γ ∈ S Φ Σ are Φ -equivalent , written K ≡ Φ Σ Γ , if for all K ∈ K and all ϕ ∈ Φ it holds that K | = Σ ϕ if, and only if, ϕ ∈ Γ .

Lemma 4. Let K ∈ S Σ and Γ ∈ S Φ Σ . Then K ≡ Φ Σ Γ if, and only if, for all K ∈ K and all φ ∈ bcl ( Φ ) it holds that K | = Σ φ iff Γ | = Φ Σ φ .

Corollary 1. Let K ∈ S Σ and Γ ∈ S Φ Σ with K ≡ Φ Σ Γ . Then it holds for all φ ∈ bcl ( Φ ) that K | = Σ φ if, and only if, Γ | = Φ Σ φ .

Lemma 5. Let K ⊆ E Σ , u ∈ U Σ , and ϕ ∈ F Σ . Then K | = Σ wlp Σ ( u , ϕ ) if, and only if, K /triangleleft Σ u | = Σ ϕ .

Lemma 6. Let K ∈ S Σ and Γ ∈ S Φ Σ with K ≡ Φ Σ Γ . Let u ∈ U Φ Σ . Then K /triangleleft Σ u ≡ Φ Σ Γ /triangleleft Φ Σ u .

Lemma 7. Let K ∈ E Σ and Γ ∈ S Φ Σ with K ≡ Φ Σ Γ . Let α ∈ A Φ Σ . Then the following holds:

1. If ( K K , ′ ) ∈ /llbracket α /rrbracket Σ , then there is a Γ ′ ∈ S Φ Σ such that ( Γ, Γ ′ ) ∈ /llbracket α /rrbracket Φ Σ and K ≡ ′ Φ Σ Γ ′ . 2. If ( Γ, Γ ′ ) ∈ /llbracket α /rrbracket Φ Σ , then there is a K ∈ S ′ Σ such that ( K K , ′ ) ∈ /llbracket α /rrbracket Σ and K ≡ ′ Φ Σ Γ ′ .

Ensemble configuration equivalence. As a consequence of Lem. 7 we can prove that semantic and symbolic ensemble configurations mutually simulate action execution while preserving Φ -equivalence.

Proposition 2. Let ( /vector E, K ) be an epistemic ensemble configuration over ˇ Σ and ( /vector E,Γ ) a symbolic epistemic ensemble configuration over ( ˇ Σ,Φ ) . Let η ∈ ⋃ N be an agent action, and let K ≡ Φ Σ Γ hold.

- 1. If ( /vector E, K - → ) η act ˇ Σ ( /vector E , ′ K ′ ) , then there is a Γ ′ ∈ S Φ Σ such that ( /vector E,Γ ) λ - → act ˇ Σ,Φ ( /vector E , Γ ′ ′ ) and K ≡ ′ Φ Σ Γ ′ .
- 2. If ( /vector E,Γ ) η - → act ˇ Σ,Φ ( /vector E , Γ ′ ′ ) , then there is a K ∈ S ′ Σ such that ( /vector E, K - → ) λ act ˇ Σ ( /vector E , ′ K ′ ) and K ≡ ′ Φ Σ Γ ′ .

The Φ -equivalence K ≡ Φ Σ Γ between semantic and symbolic epistemic states induces a ( Φ, act ) -equivalence between semantic and symbolic epistemic ensemble configurations defined as ( /vector E, K ≡ ) act ˇ Σ,Φ ( /vector E,Γ ) if K ≡ Φ Σ Γ . The next proposition lifts Prop. 2 to compound epistemic actions:

$$\text{Proposition} \, 3. \ L e t \, \lambda \in \mathcal { C } _ { \Sigma } ^ { \Phi } \, a n d \, l e t \, ( \vec { E }, \mathcal { K } ) \equiv _ { \check { \Sigma }, \Phi } ^ { a c t } \, ( \vec { E }, \Gamma ) \, h o l d.$$

- 1. If (( /vector E, K ) , ( /vector E , ′ K ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ , then there exists a Γ ′ ∈ S Φ Σ such that (( /vector E,Γ , ) ( /vector E , Γ ′ ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ,Φ and ( /vector E , ′ K ′ ) ≡ act ˇ Σ,Φ ( /vector E , Γ ′ ′ ) .
- 2. If (( /vector E,Γ , ) ( /vector E , Γ ′ ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ,Φ , then there exists a K ′ ∈ S Σ such that (( /vector E, K ) , ( /vector E , ′ K ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ and ( /vector E , ′ K ′ ) ≡ act ˇ Σ,Φ ( /vector E , Γ ′ ′ ) .

Finally, ( Φ, act ) -equivalent ensemble configurations satisfy the same dynamic ensemble logic formulæ. Thus symbolic epistemic ensemble configurations can be considered as correct realisations of semantic epistemic ensemble configurations.

Theorem 1. Let ( /vector E, K ) ≡ act ˇ Σ,Φ ( /vector E,Γ ) hold. Then for all ψ ∈ D Φ ˇ Σ , it holds that ( /vector E, K | ) = act ˇ Σ ψ ⇐⇒ ( /vector E,Γ ) = | act ˇ Σ,Φ ψ .

## 8 Conclusions

Epistemic ensembles are families of interacting knowledge-based processes. Starting with a syntactic operational semantics, we presented two complementary mathematical semantics for such ensembles: one in a semantic environment defined by classes of global epistemic states and the other one in a symbolic environment defined by a global knowledge base. As main result we showed that ensembles with Φ -equivalent configurations simulate each other and preserve Φ -equivalence.

In this paper we gave only small examples; in the future we want to tackle larger applications in behavioural ensemble specification (see, e.g., [19,13] and epistemic planning (see, e.g., [5]). We also intend to extend our approach to ensembles with distributed local states (see, e.g., [6]) and to LLM-assisted software development [3].

Acknowledgements. We would like to thank anonymous reviewers of this paper for valuable comments.

## References

- 1. Alexandru Baltag, Lawrence S. Moss, and Slawomir Solecki. The logic of public announcements and common knowledge and private suspicions. In Itzhak Gilboa, editor, Proc. 7 th Conf. Theoretical Aspects of Rationality and Knowledge (TARK) , pages 43-56. Morgan Kaufmann, 1998.
- 2. Alexandru Baltag and Bryan Renne. Dynamic epistemic logic. In Edward N. Zalta, Uri Nodelman, Colin Allen, and R. Lanier Anderson, editors, Stanford Encyclopedia of Philosophy . The Metaphysics Research Lab, Stanford University, 2016.

- 3. Lenz Belzner, Thomas Gabor, and Martin Wirsing. Large language model assisted software engineering: Prospects, challenges,and a case study. In Bernhard Steffen, editor, Proc. 1 st Intl. Conf. Bridging the Gap Between AI and Reality (AISoLA) , volume 14380 of Lect. Notes Comp. Sci. , pages 355-374. Springer, 2023.
- 4. Johan van Benthem, Jelle Gerbrandy, Tomohiro Hoshi, and Eric Pacuit. Merging frameworks for interaction. J. Philos. Log. , 38(5):491-526, 2009.
- 5. Thomas Bolander. A gentle introduction to epistemic planning: The DEL approach. In Sujata Ghosh and R. Ramanujam, editors, Proc. 9 th Ws. Methods for Modalities (M4M@ICLA) , volume 243 of EPTCS , pages 1-22, 2017.
- 6. Thomas Bolander and Mikkel Birkegaard Andersen. Epistemic planning for single and multiagent systems. J. Appl. Non Class. Logics , 21(1):9-34, 2011.
- 7. Luca Bortolussi, Rocco De Nicola, Vashti Galpin, Stephen Gilmore, Jane Hillston, Diego Latella, Michele Loreti, and Mieke Massink. CARMA: collective adaptive resource-sharing markovian agents. In Nathalie Bertrand and Mirco Tribastone, editors, Proc. 13 th Ws. Quantitative Aspects of Programming Languages and Systems (QAPL) , volume 194 of EPTCS , pages 16-31, 2015.
- 8. Tom´ as Bures, Ilias Gerostathopoulos, Petr Hnetynka, Jaroslav Keznikl, Michal Kit, and Frantisek Plasil. DEECO: an ensemble-based component system. In Proc. 16 th ACM SIGSOFT Symp. Component Based Software Engineering (CBSE) , pages 81-90. ACM, 2013.
- 9. Rocco De Nicola. Process algebras. In David Padua, editor, Encyclopedia of Parallel Computing , pages 1624-1636. Springer, 2011.
- 10. Edsger W. Dijkstra and Carle Scholten. Predicate Calculus and Program Semantics . Springer, 1990.
- 11. Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi. Dynamic Epistemic Logic , volume 337 of Synthese Library . Springer, 2008.
- 12. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge . MIT Press, 2003.
- 13. Rolf Hennicker, Alexander Knapp, and Martin Wirsing. Epistemic ensembles. In Tiziana Margaria and Bernhard Steffen, editors, Proc. 11 th Intl. Symp. Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). Part III: Adaptation and Learning , volume 13703 of Lect. Notes Comp. Sci. , pages 110-126. Springer, 2022.
- 14. Rolf Hennicker, Alexander Knapp, and Martin Wirsing. Symbolic realisation of epistemic processes. In Nikolaj Bjorner, Marijn Heule, and Andrei Voronkov, editors, Proc. 25 th Intl. Conf. Logic for Programming, Artificial Intelligence and Reasoning (LPAR) , volume 100 of EPiC Series in Comp. , pages 390-407, 2024.
- 15. Matthias M. H¨ olzl, Axel Rauschmayer, and Martin Wirsing. Software engineering for ensembles. In Martin Wirsing, Jean-Pierre Banˆ atre, Matthias M. H¨lzl, and Axel Rauschmayer, edo itors, Software-Intensive Systems and New Computing Paradigms - Challenges and Visions , volume 5380 of Lect. Notes Comp. Sci. , pages 45-63. Springer, 2008.
- 16. EmilianoLorini, Elise Perrotin, and Franc ¸ois Schwarzentruber. Epistemic actions: Comparing multi-agent belief bases with action models. In Gabriele Kern-Isberner, Gerhard Lakemeyer, and Thomas Meyer, editors, Proc. 19 th Intl. Conf. Principles of Knowledge Representation and Reasoning (KR) , 2022.
- 17. Rocco De Nicola, Diego Latella, Alberto Lluch-Lafuente, Michele Loreti, Andrea Margheri, Mieke Massink, Andrea Morichetta, Rosario Pugliese, Francesco Tiezzi, and Andrea Vandin. The SCEL language: Design, implementation, verification. In Wirsing et al. [20].
- 18. Rohit Parikh and Ramaswamy Ramanujam. A knowledge based semantics of messages. J. Logic, Lang. Inform. , 12:453-467, 2003.
- 19. Jan S¨ urmeli. Epistemic logic in ensemble specification. In Tiziana Margaria and Bernhard Steffen, editors, Proc. 9 th Intl. Conf. Leveraging Applications of Formal Methods, Verification

and Validation (ISoLA). Part II: Engineering Principles , volume 12477 of Lect. Notes Comp. Sci. , pages 329-343. Springer, 2020.

- 20. Martin Wirsing, Matthias M. H¨ olzl, Nora Koch, and Philip Mayer, editors. Software Engineering for Collective Autonomic Systems - The ASCENS Approach , volume 8998 of Lect. Notes Comp. Sci. Springer, 2015.
- 21. Martin Wirsing and Alexander Knapp. A reduction-based cut-free Gentzen calculus for dynamic epistemic logic. Log. J. IGPL , 31(6):1047-1068, 2023.
- 22. Andreas Witzel and Jonathan A. Zvesper. Epistemic logic and explicit knowledge in distributed programming. In Lin Padgham, David C. Parkes, J¨ org P. M¨ller, and Simon Parsons, u editors, Proc. 7 th Intl. Conf. Autonomous Agents and Multiagent Systems (AAMAS), Vol. 3 , pages 1463-1466. IFAAMAS, 2008.

## A Proofs

Lemma 1. If P ↪ ̂ ϕ η : - -→ ˇ Σ P ′ , then ags ˇ Σ ( P ) ⊆ ags Σ ( ̂ ϕ ) ∩ ags ˇ Σ ( η ) ∩ ags ˇ Σ ( P ′ ) .

Proof. We proceed by induction on the derivation of the conditional transition P ↪ ̂ ϕ η : - -→ ˇ Σ P ′ by the rules in Tab. 1.

For η.P true: η ↪ -- - → ˇ Σ P , we have ags ˇ Σ ( η.P ) = ags ˇ Σ ( η ) ∩ ags ˇ Σ ( P ) ⊆ ags Σ (true) ∩ ags ˇ Σ ( η ) ∩ ags ˇ Σ ( P ) .

For ϕ ⊃ P ↪ ̂ ϕ ∧ ϕ η : - - - -→ ˇ Σ P ′ , we have ags ˇ Σ ( P ) ⊆ ags Σ ( ̂ ϕ ) ∩ ags ˇ Σ ( η ) ∩ ags Σ ( P ′ ) as the induction hypothesis and thus we obtain ags ˇ Σ ( ϕ ⊃ P ) = ags Σ ( ϕ ) ∩ ags ˇ Σ ( P ) ⊆ ags Σ ( ϕ ) ∩ ags Σ ( ̂ ϕ ) ∩ ags ˇ Σ ( η ) ∩ ags ˇ Σ ( P ′ ) = ags Σ ( ̂ ϕ ∧ ϕ ) ∩ ags ˇ Σ ( η ) ∩ ags ˇ Σ ( P ′ ) .

For P 1 + P 2 ̂ ϕ η : ↪ - -→ ˇ Σ P ′ /lscript with /lscript ∈ { 1 2 , } , we have ags ˇ Σ ( P /lscript ) ⊆ ags Σ ( ̂ ϕ ) ∩ ags ˇ Σ ( η ) ∩ ags ˇ Σ ( P ′ /lscript ) as the induction hypothesis and thus we obtain ags ˇ Σ ( P 1 + P 2 ) = ags ˇ Σ ( P 1 ) ∩ ags ˇ Σ ( P 2 ) ⊆ ags Σ ( ̂ ϕ ) ∩ ags ˇ Σ ( η ) ∩ ags ˇ Σ ( P ′ /lscript ) .

↦

↦

For µX . P ̂ ϕ η : ↪ - -→ ˇ Σ P ′ , we have ags ˇ Σ ( P { X → µX . P } ) ⊆ ags Σ ( ̂ ϕ ) ∩ ags ˇ Σ ( η ) ∩ ags ˇ Σ ( P ′ ) as the induction hypothesis and thus ags ˇ Σ ( µX . P ) = ags ˇ Σ ( P ) ⊆ ags Σ ( ̂ ϕ ) ∩ ags ˇ Σ ( η ) ∩ ags ˇ Σ ( P ′ ) using that ags ˇ Σ ( P { X → µX . P } ) = ags ˇ Σ ( P ) .

## Lemma 2. Let K ∈ S Σ and α ∈ A Σ .

- 1. If ( { K } K , K ) ∈ /llbracket α /rrbracket Σ for some K ∈ K , then there are K ′ ∈ E Σ with K K = { K ′ } and K ∈ S ′ Σ with K ′ ∈ K ′ such that ( K K , ′ ) ∈ /llbracket α /rrbracket Σ .
- 2. If ( K K , ′ ) ∈ /llbracket α /rrbracket Σ , then for each K ′ ∈ K ′ there is some K ∈ K with ( { K } { , K ′ } ) ∈ /llbracket α /rrbracket Σ .

Proof. (1) Let ( { K } K , K ) ∈ /llbracket α /rrbracket Σ hold. Then there is a u ∈ α with K | = Σ pre ( u ) and K K = { K /triangleleft Σ u } . Furthermore, K | = Σ pre ( u ) and thus ( K K , /triangleleft Σ u ) ∈ /llbracket α /rrbracket Σ with K /triangleleft Σ u ∈ K /triangleleft Σ u .

(2) Let ( K K , ′ ) ∈ /llbracket α /rrbracket Σ hold and let K ′ ∈ K ′ . Then there is a u ∈ α with K | = Σ pre ( u ) and K ′ = K /triangleleft Σ u such that there is K ∈ K with K ′ = K /triangleleft Σ u and ( { K } { , K ′ } ) ∈ /llbracket α /rrbracket Σ .

Lemma 3. Let ( /vector E, K ) be an ensemble configuration and λ ∈ C ˇ Σ .

- 1. If (( /vector E, { K } ) , ( /vector E , ′ K K )) ∈ /llbracket λ /rrbracket act ˇ Σ for some K ∈ K , then there are K ′ ∈ E Σ with K K = { K ′ } and K ∈ S ′ Σ with K ′ ∈ K ′ such that (( /vector E, K ) , ( /vector E , ′ K ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ .
- 2. If (( /vector E, K ) , ( /vector E, K ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ , then for each K ′ ∈ K ′ there is some K ∈ K with (( /vector E, { K } ) , ( /vector E , ′ { K ′ } )) ∈ /llbracket λ /rrbracket act ˇ Σ .

Proof. The claims follow directly from Lem. 2 and the definition of the semantics of guard-action sequences σ .

Proposition 1. Let ( /vector E, K ) be an ensemble configuration. For all ψ ∈ D ˇ Σ it holds that ( /vector E, K | ) = act ˇ Σ ψ if, and only if, ( /vector E, { K } ) = | act ˇ Σ ψ for all K ∈ K .

Proof. We proceed by induction over the structure of ψ ∈ D ˇ Σ where ϕ , true , negation, and conjunction are straightforward. For a [ λ ψ ] , let first ( /vector E, K ) | = act ˇ Σ [ λ ψ ] hold. Let K ∈ K and (( /vector E, { K } ) , ( /vector E , ′ K K )) ∈ /llbracket λ /rrbracket act ˇ Σ . By Lem. 3(1) there is a K ′ ∈ E Σ with K K = { K ′ } and some K ′ ∈ S Σ with K ′ ∈ K ′ and (( /vector E, K ) , ( /vector E , ′ K ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ and thus ( /vector E , ′ K ′ ) | = act ˇ Σ ψ . By the induction hypothesis, ( /vector E , ′ { K ′ } ) | = act ˇ Σ ψ and thus ( /vector E, { K } ) | = act ˇ Σ [ λ ψ ] . -Let conversely, ( /vector E, { K } ) | = act ˇ Σ [ λ ψ ] hold for all K ∈ K . Let (( /vector E, K ) , ( /vector E , ′ K ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ . By Lem. 3(2) for each K ′ ∈ K ′ there is a K ∈ K with (( /vector E, { K } ) , ( /vector E , ′ { K ′ } )) ∈ /llbracket λ /rrbracket act ˇ Σ and thus ( /vector E, { K ′ } ) | = Σ ψ for all K ′ ∈ K ′ . By the induction hypothesis, ( /vector E , ′ K ′ ) = | act ˇ Σ ψ and thus ( /vector E, { K } ) = | act ˇ Σ [ λ ψ ] .

Lemma 4. Let K ∈ S Σ and Γ ∈ S Φ Σ . Then K ≡ Φ Σ Γ if, and only if, for all K ∈ K and all φ ∈ bcl ( Φ ) it holds that K | = Σ φ iff Γ | = Φ Σ φ .

Proof. ' ⇒ ': Assume K ≡ Φ Σ Γ and let K ∈ K . The proof is performed by structural induction on the form of φ .

Case φ = ϕ ∈ Φ : Then K | = Σ ϕ iff (since K ≡ Φ Σ Γ ) ϕ ∈ Γ iff Γ | = Φ Σ ϕ .

Case true : K | = Σ true and Γ | = Φ Σ true hold.

Case ¬ φ with ¬ φ / Φ ∈ : K | = Σ ¬ φ iff not K | = Σ φ iff (by induction hypothesis) not Γ | = Φ Σ φ iff (since ¬ φ / Φ ∈ ) Γ | = Φ Σ ¬ φ .

Case ϕ 1 ∧ ϕ 2 with ϕ 1 ∧ ϕ 2 / Φ ∈ : K | = Σ ϕ 1 ∧ ϕ 2 iff K | = Σ ϕ 1 and K | = Σ ϕ 2 iff (by induction hypothesis) Γ | = Φ Σ ϕ 1 and Γ | = Φ Σ ϕ 2 iff (since ϕ 1 ∧ ϕ 2 / Φ ∈ ) Γ | = Φ Σ ϕ 1 ∧ ϕ 2 .

' ⇐ ': Since Φ ⊆ bcl ( Φ ) , the assumption implies K | = Σ ϕ ⇐⇒ Γ | = Φ Σ ϕ ⇐⇒ ϕ ∈ Γ for all ϕ ∈ Φ and all K ∈ K ; hence, K ≡ Φ Σ Γ .

Corollary 1. Let K ∈ S Σ and Γ ∈ S Φ Σ with K ≡ Φ Σ Γ . Then it holds for all φ ∈ bcl ( Φ ) that K | = Σ φ if, and only if, Γ | = Φ Σ φ .

Proof. Let φ ∈ bcl ( Φ ) . Since K /negationslash = ∅ , there is a K ∈ K and it holds that K | = Σ φ if, and only if, Γ | = Φ Σ φ if, and only if, K ′ | = Σ φ for all K ′ ∈ K by Lem. 4.

Lemma 5. Let K ⊆ E Σ , u ∈ U Σ , and ϕ ∈ F Σ . Then K | = Σ wlp Σ ( u , ϕ ) if, and only if, K /triangleleft Σ u | = Σ ϕ .

/negationslash

/negationslash

Proof. Let first K | = Σ wlp Σ ( u , ϕ ) hold, i.e., K | = Σ wlp Σ ( u , ϕ ) for all K ∈ K , or, equivalently, K | = Σ pre ( u ) or K /triangleleft Σ u | = Σ ϕ . Let K ′ ∈ K /triangleleft Σ u , i. e., K ′ = K /triangleleft Σ u with K ∈ K and K | = Σ pre ( u ) . Then K /triangleleft Σ u | = Σ ϕ . -Let now conversely K /triangleleft Σ u | = Σ ϕ hold, i.e., K /triangleleft Σ u | = Σ ϕ for all K ∈ K with K | = Σ pre ( u ) . Let K ∈ K . If K | = Σ pre ( u ) , then K | = Σ wlp Σ ( u , ϕ ) ; if K | = Σ pre ( u ) , then K /triangleleft Σ u | = Σ ϕ and thus again K | = Σ wlp Σ ( u , ϕ ) .

Lemma 6. Let K ∈ S Σ and Γ ∈ S Φ Σ with K ≡ Φ Σ Γ . Let u ∈ U Φ Σ . Then K /triangleleft Σ u ≡ Φ Σ Γ /triangleleft Φ Σ u .

Proof. Let ϕ ∈ F Σ . Then

$$\mathcal { K } \lhd _ { \Sigma } \mathfrak { u } \models _ { \Sigma } \varphi \iff \mathcal { K } \models _ { \Sigma } \, \text{wlp} _ { \Sigma } ( \mathfrak { u }, \varphi ) \iff \\ f. \, \text{a. } \rho \in \text{Wlp} _ { \Sigma } ( \mathfrak { u }, \varphi ) \colon \mathcal { K } \models _ { \Sigma } \, \rho \iff \mathfrak { u } \, \text{repr.} \, \text{Cor. } 1 \\ \text{ex.} \, \rho \in \text{Wlp} _ { \Sigma } ( \mathfrak { u }, \varphi ) \cap b c l ( \Phi ) \, \text{s.t.} \, \Gamma \models _ { \Sigma } \, \rho \iff \varphi \in \Gamma \lhd _ { \Sigma } \, \mathfrak { u } \,.$$

Lemma 7. Let K ∈ E Σ and Γ ∈ S Φ Σ with K ≡ Φ Σ Γ . Let α ∈ A Φ Σ . Then the following holds:

1. If ( K K , ′ ) ∈ /llbracket α /rrbracket Σ , then there is a Γ ′ ∈ S Φ Σ such that ( Γ, Γ ′ ) ∈ /llbracket α /rrbracket Φ Σ and K ≡ ′ Φ Σ Γ ′ . 2. If ( Γ, Γ ′ ) ∈ /llbracket α /rrbracket Φ Σ , then there is a K ∈ S ′ Σ such that ( K K , ′ ) ∈ /llbracket α /rrbracket Σ and K ≡ ′ Φ Σ Γ ′ .

Proof. (1) Let ( K K , ′ ) ∈ /llbracket α /rrbracket Σ . Then there is a u ∈ α such that K ′ = K /triangleleft Σ u and K | = Σ pre ( u ) . By Lem. 4 and u ∈ U Φ Σ it holds that there is a ρ ∈ Pre ( u ) ∩ bcl ( Φ ) such that Γ | = Φ Σ ρ and hence ( Γ, Γ ′ ) ∈ /llbracket α /rrbracket Φ Σ with Γ ′ = Γ /triangleleft Φ Σ u . By Lem. 6, K /triangleleft Σ u ≡ Φ Σ Γ /triangleleft Φ Σ u , i. e., K ≡ ′ Φ Σ Γ ′ .

(2) Let ( Γ, Γ ′ ) ∈ /llbracket α /rrbracket Φ Σ . Then there is a u ∈ α such that Γ ′ = Γ /triangleleft Φ Σ u and Γ | = Φ Σ ρ for some ρ ∈ Pre ( u ) ∩ bcl ( Φ ) . By Lem. 4, K /negationslash = ∅ , and u ∈ U Φ Σ it holds that K | = Σ pre ( u ) and hence ( K K , ′ ) ∈ /llbracket α /rrbracket Σ with K ′ = K /triangleleft Σ u . By Lem. 6, K /triangleleft Σ u ≡ Φ Σ Γ /triangleleft Φ Σ u , i. e., K ≡ ′ Φ Σ Γ ′ .

Proposition 2. Let ( /vector E, K ) be an epistemic ensemble configuration over ˇ Σ and ( /vector E,Γ ) a symbolic epistemic ensemble configuration over ( ˇ Σ,Φ ) . Let η ∈ ⋃ N be an agent action, and let K ≡ Φ Σ Γ hold.

- 1. If ( /vector E, K - → ) η act ˇ Σ ( /vector E , ′ K ′ ) , then there is a Γ ′ ∈ S Φ Σ such that ( /vector E,Γ ) λ - → act ˇ Σ,Φ ( /vector E , Γ ′ ′ ) and K ≡ ′ Φ Σ Γ ′ .
- 2. If ( /vector E,Γ ) η - → act ˇ Σ,Φ ( /vector E , Γ ′ ′ ) , then there is a K ∈ S ′ Σ such that ( /vector E, K - → ) λ act ˇ Σ ( /vector E , ′ K ′ ) and K ≡ ′ Φ Σ Γ ′ .

Proof. (1) Let ( /vector E, K ) η - → act ˇ Σ ( /vector E , ′ K ′ ) be given. Then there is a /vector E ↪ ̂ ϕ η : - -→ ˇ Σ /vector E ′ with K | = Σ ̂ ϕ and ( K K , ′ ) ∈ /llbracket act ( η ) /rrbracket Σ . Since K ≡ Φ Σ Γ , K /negationslash = ∅ , and ̂ ϕ ∈ bcl ( Φ ) we have, by Lem. 4, Γ | = Φ Σ ̂ ϕ and, by Lem. 7(1), there exists a Γ ′ ∈ S Φ Σ such that ( Γ, Γ ′ ) ∈ /llbracket act ( η ) /rrbracket Φ Σ and K ≡ ′ Φ Σ Γ ′ . Therefore ( /vector E,Γ ) η - → act ˇ Σ,Φ ( /vector E , Γ ′ ′ ) and K ≡ ′ Φ Σ Γ ′ .

(2) Let ( /vector E,Γ ) η - → act ˇ Σ,Φ ( /vector E , Γ ′ ′ ) be given. Then there is a /vector E ↪ ̂ φ η : - -→ ˇ Σ /vector E ′ with Γ | = Φ Σ ̂ φ and ( Γ, Γ ′ ) ∈ /llbracket act ( η ) /rrbracket Φ Σ . Since K ≡ Φ Σ Γ and K /negationslash = ∅ we have, by Lem. 4, K | = Σ ̂ φ and, by Lem. 7(2), there exists K ∈ S ′ Σ such that ( K K , ′ ) ∈ /llbracket act ( η ) /rrbracket Σ and K ≡ ′ Φ Σ Γ ′ . Therefore ( /vector E, K - → ) η act ˇ Σ ( /vector E , ′ K ′ ) and K ≡ ′ Φ Σ Γ ′ .

Proposition 3. Let λ ∈ C Φ ˇ Σ and let ( /vector E, K ≡ ) act ˇ Σ,Φ ( /vector E,Γ ) hold.

- 1. If (( /vector E, K ) , ( /vector E , ′ K ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ , then there exists a Γ ′ ∈ S Φ Σ such that (( /vector E,Γ , ) ( /vector E , Γ ′ ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ,Φ and ( /vector E , ′ K ′ ) ≡ act ˇ Σ,Φ ( /vector E , Γ ′ ′ ) .
- 2. If (( /vector E,Γ , ) ( /vector E , Γ ′ ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ,Φ , then there exists a K ′ ∈ S Σ such that (( /vector E, K ) , ( /vector E , ′ K ′ )) ∈ /llbracket λ /rrbracket act ˇ Σ and ( /vector E , ′ K ′ ) ≡ act ˇ Σ,Φ ( /vector E , Γ ′ ′ ) .

Proof. This follows by structural induction on the form of λ ∈ C ˇ Σ , where η ∈ ⋃ N is covered by Prop. 2, φ ? with φ ∈ bcl ( Φ ) by Lem. 4, and all other cases follow directly from the induction hypothesis.

Theorem 1. Let ( /vector E, K ) ≡ act ˇ Σ,Φ ( /vector E,Γ ) hold. Then for all ψ ∈ D Φ ˇ Σ , it holds that ( /vector E, K | ) = act ˇ Σ ψ ⇐⇒ ( /vector E,Γ ) = | act ˇ Σ,Φ ψ .

Proof. This follows by structural induction on the form of ψ ∈ D Φ ˇ Σ , where [ λ ψ ] is a consequence of Prop. 3.
Rolf Hennicker Alexander Knapp Martin Wirsing
Epistemic Ensembles in Semantic and Symbolic Environments (Extended Version with Proofs)
An epistemic ensemble is composed of knowledge-based agents capable of
retrieving and sharing knowledge and beliefs about themselves and their peers.
These agents access a global knowledge state and use actions to communicate and
cooperate, altering the collective knowledge state. We study two types of
mathematical semantics for epistemic ensembles based on a common syntactic
operational ensemble semantics: a semantic environment defined by a class of
global epistemic states, and a symbolic environment consisting of a set of
epistemic formul{\ae}. For relating these environments, we use the concept of
{\Phi}-equivalence, where a class of epistemic states and a knowledge base are
{\Phi}-equivalent, if any formula of {\Phi} holds in the class of epistemic
states if, and only if, it is an element of the knowledge base. Our main
theorem shows that {\Phi}-equivalent configurations simulate each other and
satisfy the same dynamic epistemic ensemble formulae.