Efficient Representations for the Modal Logic S5

1 Introduction

The epistemic modal logic S5 is the logic of monoagent knowledge [Fagin et al., 1995], allowing for statements such as (Kp _Kp) ^ (≻K(p ^ q)), which means that the agent knows that p is true or knows that p is false (i.e., it knows the value of p), but does not know that p^q is true (it knows that p^q is false, or does not knowwhether it is true or false).

A particular setting where the logic S5 arises naturally is that of contingent planning [Herzig et al., 2003; Petrick and Bacchus, 2004; Hoffmann and Brafman, 2005; Iocchi et al., 2004; Bonet and Geffner, 2014], which is the problem of computing a plan towards a given goal, using two kinds of actions. Ontic actions change the actual state of the world in a nondeterministic fashion, and epistemic actions give the agent feedback about the actual state. The plan sought for can be conditional on the feedbacks received from the epistemic actions.

It is not hard to see that at any moment, an agent executing a contingent plan has a unique set of states which are candidates for being the actual state of the environment. Such a set is called a belief state in the planning literature. For instance, if the agent knows that the initial state satisfies p^q, and executes an ontic action switch which nondeterministically switches either the value of p or that of q, then the resulting belief state can be described by (p^q)_(p^q). If the agent then executes the epistemic action test, which indicates whether p^r is true, and receives the feedback that it is the case, then the resulting set can be described by (p^q^r).

When planning, or verifying the validity of a plan, it is also useful to consider the evolution of several possible belief states at the same time, a process usually called offline progression. For instance, if the initial belief state is p^q, then the ontic action switch leads to (p^q)_(p^q) as above, but the epistemic action test leads to two possible belief states, depending on its feedback: either (p ^ q ^ r) as above, or (p^q)_(p^q^r) if feedback p_r is received. So, in planning and in other applications, it is important to be able to handle general S5 formulas, which represent sets of belief states. In the example above, we would use the representation K(p^q^r)_K((p^q)_(p^q^r)) (note that planning usually does not use only-knowing [Levesque, 1990]: goals being typically positive, knowing more is always better-in particular, one often needs only positive knowledge formulas).

Motivated by such uses in planning, we investigate several representations of (subjective) S5 formulas from the point of view of space and time efficiency. We consider the s-S5-DNFDNF↪CNF representation proposed by Bienvenu et al. [2010], as well as its natural variant s-S5-DNFOBDD↪OBDD. We moreover introduce a new representation (Sections 3 and 4), using structures that we call Epistemic Splitting Diagrams (ESDs), which use ideas similar to Binary Decision Diagrams. We investigate these three languages from the point of view of knowledge compilation [Darwiche and Marquis, 2002], comparing their ability to support queries and transformations efficiently (Section 5) and to represent S5 formulas succinctly (Section 6). Finally, we report on experiments, which confirm in practice the properties of the different languages (Section 7). Our results show that each language has its pros and cons; they also show that ESDs are more compact than previous representations for positive S5 formulas.

2 Preliminaries

S5 The reader is supposed to be acquainted with the basic concepts of propositional logic. We consider the language of propositional S5 [Fagin et al., 1995], in which formulas are built on a set of propositional atoms X with the usual connectives ≻↪_↪^ and the knowledge modality K. For instance, (Kx1 ^≻K(x2 _x3))_≻K(x1) is an S5 formula. We denote by Var(F) the set of propositional atoms mentioned in a formula F (i.e., ¶x1↪x2↪x3♦ in the previous example). For space reasons, and motivated by the representations typically needed in planning, we restrict our study to subjective S5, in which one can express statements about the knowledge of agents, but not about the actual state of the world (even though our study could be rather directly extended to general S5 formulas). We thus only consider formulas in which all propositional atoms appear in the scope of K: e.g., x1 ^Kx2 is not a subjective formula. Since any S5 formula is equivalent to one without nested modalities, we use the following definition.

Definition 1. A subjective S5 formula over X is a Boolean combination, using ≻, _ and ^, of epistemic atoms of the form Kj, where each j is a propositional formula over X.

We use uppercase (resp. lowercase) Greek letters F↪Y↪ ▷ ▷ ▷ (resp. j↪y↪ ▷ ▷ ▷ ) to denote S5 (resp. propositional) formulas. Due to the axiomatic of S5, subjective formulas are naturally interpreted over structures, which are simply nonempty subsets of 2 X , that is, nonempty sets of propositional assignments (we silently assume that structures are over the set of all propositional atoms under consideration). Intuitively, a structure represents a belief state, i.e., a set of assignments that the agent considers as candidates for being the actual state of the world; an S5 formula represents a set of such belief states.

A structure M is said to satisfy an epistemic atom Kj if all propositional assignments m 2 M satisfy j under the standard propositional semantics; M satisfies F^Y (resp. F_Y) if it satisfies F and Y (resp. F or Y), and ≻F if it does not satisfy F. Note that M satisfies ≻Kf if it contains at least one propositional countermodel of j (intuitively, the agent does not know f if f is false in at least one state which may be the actual one), and that this is different from satisfying K≻j.

We write M ♣= F if the structure M satisfies the subjective S5 formula F; it is a model of F, and we denote by Mod(F) the set of models of F. When Mod(F) = Mod(Y), F and Y represent the same set of belief states; we call them logically equivalent, written F ⌘ Y. When Mod(F) ✓ Mod(Y), we say that F entails Y, written F ♣= Y. A formula is tautological if all structures satisfy it. Notably useful in planning are positive S5 formulas, i.e., formulas equivalent to some WiKji; it can be shown that those are exactly the formulas whose model set is closed by taking (nonempty) subsets.

Propositional languages A propositional formula (over X) is in the NNF (Negation Normal Form) language if it is a combination by _ and ^ of propositional literals of the form x or x (x 2 X). Identical subformulas are shared in NNF formulas: they are not trees but rather directed acyclic graphs (DAGs), and the size ♣j♣ of a formula j is thus its number of nodes. A term (resp. clause) is a conjunction (resp. disjunction) of literals. A formula is in disjunctive (resp. conjunctive) normal form if it is a disjunction of terms (resp. a conjunction of clauses); the corresponding language is called DNF (resp. CNF). Conditioning a formula j by a literal ` is, intuitively, deciding on the value of the corresponding atom; it can be done syntactically by replacing every instance of ` (resp. `) by > (resp. ?). The result is denoted by j♣`. We also write

>

?

>

>

Figure 1: An EBDD (left) and two ESDs. Dots are to right children of ite's and spl's, and leaves are duplicated only for clarity.

M♣` for the structure obtained from a structure M by keeping only the assignments satisfying `, then removing ` from them.

A Binary Decision Diagram (BDD) is a constant or a formula of the form (x^N)_(x^N0 ), where N↪N0 are BDDs; the latter is written ite(x↪N↪N0 ). A BDD can be seen as a DAG over nodes labeled with atoms (e.g., on Figure 1, left, the DAG rooted at x1 is a BDD). A BDD is an ordered BDD (OBDD) if atoms are encountered at most once and in the same order along all paths from the root to a leaf. It is wellknown that any NNF j can be represented as an OBDD (over any atom ordering), using the Shannon expansion.

S5-DNF Bienvenu et al. [2010] give the first study of effective representations for S5 formulas, notably introducing the following parameterized language:

Definition 2. Let L↪L0 be two (propositional) sublanguages of NNF; an S5 formula is in s-S5-DNFL↪L0 if it is a disjunction of terms, each consisting of at most one positive epistemic literal Kj and of an arbitrary number of negative epistemic literals ≻Kyi, where j is in L and each yi is in L0 .

They study the properties of s-S5-DNFL↪L0 in a general setting, in terms of the properties of L and L0 ; they also focus on a specific instantiation, s-S5-DNFDNF↪CNF (we denote it by EDNF for short), which turns out to have good properties for the operations involved in planning. Another natural instantiation is s-S5-DNFOBDD↪OBDD (denoted here by EBDD); Bienvenu et al. [2010] did not explicitly consider it, but most of their general results directly apply to it. Figure 1 (left) gives an EBDD for (K(x1 _ x3) ^ ≻K(x2 _ x3)) _ (≻K(x2 _ x3) ^ K(x2)).

3 Epistemic Splitting Diagrams

We now introduce a new language, written ESD, for representing subjective S5 formulas. As pointed out by Bienvenu et al. [2010, Example 15], the Shannon expansion cannot be used for S5 formulas at the epistemic level, but we introduce the related notion of splitting. Intuitively, a split over a propositional atom x divides a structure M into M♣x and M♣x. For instance, with M1 = ¶x2x3↪x2x3♦ and M2 = ¶x2x3♦, spl(x1↪M1↪M2) represents the structure ¶x1x2x3↪x1x2x3↪x1x2x3♦. More generally, we allow splits to represent sets of structures of a specific form: spl(x↪M↪M0 ) represents the set ¶spl(x↪M↪M0 ) ♣ M 2M↪M0 2M0 ♦.

As splits are not enough for obtaining a complete language, ESD also uses the _ connective. Moreover, since the model set of an S5-formula contains structures, which are themselves sets, we have four constant formulas: the usual constants ? and >, which are satisfied by no structure and by all structures, respectively, and two new ones, D and -, respectively satisfied exactly by the empty structure, and by all nonempty structures. The two latter constants are notably used as children of splitting nodes; for instance, on Figure 1 (right), the ESD rooted at the bottom left x2 node is satisfied by all structures which contain an assignment satisfying x2. Formally:

Definition 3. The language ESD of epistemic splitting diagrams is defined inductively as follows:

• ÷ >, -, ?, and D are ESDs;
• ÷ if F1↪ ▷ ▷ ▷ ↪Fn are ESDs, then Wn i=1Fi is an ESD.
• ÷ if F1 and F2 are ESDs, then spl(x↪F1↪F2) is an ESD;

A structure M satisfies an ESD F, denoted by M ♣= F, if either (i) F is - (resp. D) and M is not ? (resp. is ?); or (ii) F is spl(x↪F1↪F2) and M♣x ♣=F1 and M♣x ♣=F2 hold; or (iii) F is Wn i=1Fi and M satisfies Fi for at least one i 2 ¶1↪ ▷ ▷ ▷ ↪n♦. Additionally, M always satisfies > and never satisfies ?.

Recall that S5 formulas are interpreted over nonempty structures. However, for ease of exposition we allow the empty structure M? as a model of some ESDs. This is harmless since F^- has the same models as F except for M?, and can be computed efficiently (Proposition 14).

Figure 1 (right) gives an example of an ESD: the left child of its root is satisfied exactly by the structures M such that (i) M♣x1 is empty or contains an assignment satisfying x2, and (ii) M♣x1 contains an assignment satisfying x3. Remark that, like OBDDs, we view ESDs as DAGs, and we assume that identical subgraphs are systematically shared.

Definition 3 places no specific syntactic restriction on ESDs; it is however useful to consider reduced ESDs.

Definition 4. An ESD F is said to be reduced if none of the following rules applies to it:

• ÷ simplify using (?_F)⌘F, (>_F)⌘>, spl(x↪D↪D)⌘ D, spl(x↪>↪>) ⌘>, spl(x↪F↪?) ⌘ spl(x↪?↪F) ⌘?;
• ÷ replace spl(x↪F↪Y1) _ spl(x↪F↪Y2) by spl(x↪F↪Y1 _ Y2), and dually when it is right children that match;
• ÷ remove duplicates among children of _-nodes, and flatten (F1 _· · ·_(Y1 _· · ·_Yk)_· · ·_Fm) into (F1 _· · ·_ Y1 _ · · · _Yk _ · · · _Fm), W¶F♦ into F, and W ? into ?;
• ÷ replace (F1 _ · · · _D_ · · · _Fk) by (F1 _ · · · _Fk) if some Fi is satisfied by M?;
• ÷ replace (F1 _· · ·_-_· · ·_Fk) by > if some Fi is satisfied by M? and by - otherwise.

It is easily seen that all these rules preserve logical equivalence, and can be enforced in linear time. Another important property (obtained by a simple structural induction), is that the only reduced ESD equivalent to ? (resp. to D) is ? itself (resp. D itself). Contrastingly, as is the case for EDNF and EBDD, there are several reduced ESDs equivalent to > or -. For instance (abusing notation), spl(x↪Ky↪D) _

spl(x↪>↪-) _ spl(x↪≻Ky↪>) is reduced but logically equivalent to K(x^y)_≻Kx_≻K(x_y), which is tautological.

As for OBDD, we can impose ESDs to be ordered. Given a total ordering < on X, an ESD is said to be <-ordered if the propositional atoms appear in (strict) increasing order wrt < along each path from the root to a leaf.

In this paper, we only consider reduced ordered ESDs. We write ESD for the language consisting of all ESDs which are reduced and ordered (leaving < implicit). For instance, the ESDs on Figure 1 are reduced, and ordered wrt x1 < · · · < xn.

ESDs share many features with OBDDs. An important difference is in the status of stuttering nodes. A node ite(x↪j↪j) can be eliminated from an OBDD (and replaced by j), but the same is not true for ESDs: in general, we have spl(x↪F↪F) 6♣= F. For instance, with F ⌘ Ky_Ky, we have that M = ¶xy↪ xy♦ satisfies spl(x↪F↪F) (since M♣x = ¶y♦ satisfies Ky and hence F, and M♣x = ¶y♦ satisfies Ky and hence F), but M does not satisfy F (since in M both y and y are possible). Due to this, in order to be efficient, some transformations require that (reduced, ordered) ESDs have a specific form.

Definition 5. Let < be a total order on X, with x1 < · · · < xn. An ESD F is said to be explicitly <-ordered if it is <-ordered and for each path P from the root to a leaf, the set of atoms appearing along P is ¶x1↪ x2↪ ▷ ▷ ▷ ↪ xi♦ for some i 2 ¶1↪ ▷ ▷ ▷ ↪ n♦.

For instance, on the ESD of Figure 1 (right), the third path from the left, (_↪x1↪_↪x2↪-), is explicitly ordered with respect to x1 < x2 < x3, but the fourth one, (_↪x1↪x3↪-), is not (x2 is missing). Hence the ESD is not explicitly ordered.

In the rest of the paper, we always consider OBDDs and ESDs ordered over the same (implicit) atom ordering. Unless specified, we do not require the ESDs to be explicitly ordered.

4 Compiling Epistemic Atoms into ESDs

Arguably, it is natural to specify formulas such as goals, initial states, etc., in the form of S5 logical formulas. Manipulating ESDs thus requires to first compile [Marquis, 2015] standard epistemic representations into the ESD language. We show in this section how to compile epistemic atoms as ESDs; Section 5 will show how to combine them using connectives.

Since compiling propositional formulas into OBDD is a well-studied problem [Bryant, 1992; Meinel and Theobald, 1998; Huang and Darwiche, 2005], we assume that epistemic atoms are in the form Kj, where j is an OBDD over the atom ordering that we want for the ESD. Building j is hard, but once it is done, Kj can be obtained very efficiently:

Proposition 6. Given a formula j in OBDD, one can build in linear (resp. quadratic) time an ordered ESD (resp. an explicitly ordered ESD) logically equivalent to Kj _D or to ≻Kj.

Proof. Let us build an ESD F from j by replacing the ? leaf by D and each node ite(x↪f1↪f2) by spl(x↪F1↪F2), with F1↪F2 obtained recursively from f1↪f2. Then we can show by induction that F is equivalent to Kj _D because (i) by replacing ? by D we prevent any countermodel of j to be in a satisfying structure, and (ii) by keeping the > leaf we allow any model of j to be or not to be in a satisfying structure. The result follows fromM ♣=Kj_D,M✓Mod(j).

For ≻Kj, we build an ESD Y from j by replacing ? by -, > by ?, and each node ite(x↪f1↪f2) by spl(x↪Y1↪>) _ spl(x↪>↪Y2), with Y1↪Y2 obtained recursively. An easy induction shows that a structure M satisfies Y exactly if it contains at least one countermodel of j, hence Y⌘≻Kj.

Observe that both constructions do not require j to be a reduced OBDD. Hence, the resulting ESD is explicitly ordered if j is first made explicitly ordered, by recursively replacing all nodes ite(xi↪y↪ ·), where y = ite(xk↪j1↪j2), by ite(xi↪ ite(xj↪y↪y)↪ ·), as long as there is a j such that xi < x j < xk holds (and dually for the other child). This clearly increases the size of j by a factor ♣Var(j)♣ at most.

Moreover, an interesting feature of ESDs is that they can efficiently represent "only-know" atoms. Recall that Oj is satisfied by a single structure, namely Mod(j): the agent knows j, but does not know more [Levesque, 1990]. Mixing K and O modalities requires specific inference rules, while representing Oj using K modalities requires the conjunction Kj ^ Vm♣=j ≻K≻m (in general, exponentially long). So the ability to represent Oj naturally is unique to ESD.

Proposition 7. Given an OBDD j, one can build an explicitly ordered ESD logically equivalent to Oj in quadratic time.

Proof. We first make j fully explicit: for each path in j, we proceed as in Proposition 6, but also until the leaves are reached (e.g., we recursively replace ite(xi↪>↪ ·) by ite(xi↪ ite(x j ↪>↪>)↪ ·)). Then we replace ? by D, > by -, and each ite(x↪f1↪f2) by spl(x↪F1↪F2), with F1↪F2 obtained recursively. The resulting ESD is satisfied exactly by Mod(j) because D prevents the countermodels of j to be in a satisfying structure, and - forces its models to be in.

Observing that any formula F is equivalent to WM♣=FOjM, where jM is an OBDD with Mod(j) = M, we easily deduce:

Proposition 8. ESD is complete for subjective S5: for any subjective S5 formula F, there exists an ESD Y with Y ⌘ F.

5 Queries and Transformations

With EDNF, EBDD, and ESD, we have three available languages for representing subjective S5 formulas. Before comparing their ability to represent formulas compactly (Section 6), we study how efficiently they support queries (i.e., reasoning tasks) and transformations; this is summarized in Table 1 to allow for easy comparison. Most results for EDNF and EBDD

come from Bienvenu et al. [2010], hence we focus on ESD. The first result is easy, so we omit the proof (simply recall from Section 3 that ? and D have unique reduced ESDs).

Proposition 9. Given a formula F in either EDNF, EBDD or ESD, it can be decided in polynomial time whether F is satisfiable, and whether it is satisfied by a structure M given in extension (i.e., as a set of propositional assignments).

Proposition 10. Given a satisfiable formula in EDNF, EBDD, or ESD, a structure satisfying it can be computed in polytime (in particular, a polysize model always exists).

Proof. For EDNF (resp. EBDD), we choose a satisfiable term Kj ^ Vi ≻Kyi, and we build M by taking one model of j ^ ≻yi for each i, which is polytime since j is in DNF and yi in CNF (resp. since both are OBDDs). For ESD, at each subnode we select a satisfiable child, and at each node spl(x↪F1↪F2), we build M from M♣x and M♣x, obtained recursively.

We now turn to validity and entailment checking:

Proposition 11. Given a formula F in ESD, it is coNP-hard to decide whether F is tautological, and to decide whether Ky ♣= F holds for y in NNF or OBDD.

Proof. Let f = Vi2I ci be a propositional CNF, where each ci is a clause, and let F be the ESD D_ Wi2I Fi, where Fi is equivalent to ≻Kci. Since F can be built in polytime (Prop. 6), and it can be shown that F is tautological if and only if f is unsatisfiable, we get the first statement. For the second one, remark that F is tautological if and only if K> entails F.

Proposition 12. For any fixed k, given an explicitly ordered ESD F and a disjunction Y of at most k atoms Kji or ≻Kji, where all ji's are OBDDs, it is polytime to decide F ♣=Y.

Proof. Since it is polytime to compute the negation of the atoms in Y (Prop. 6), and since bounded conjunction and satisfiability are polytime on ESD (Prop. 14, 9), we can decide efficiently whether F^≻Y is unsatisfiable.

However, we conjecture that unbounded clausal entailment (CE) is hard on ESD. Note that EBDD supports bounded CE (similar proof as Prop. 12); EDNF supports unbounded CE for another representation of atoms [Bienvenu et al., 2010].

We finally consider combinations and transformations.

Proposition 13. Given k ESDs F1↪ ▷ ▷ ▷ ↪Fk, an ESD equivalent to Wk i=1Fi can be computed in linear time, but an ESD of size polynomial in  k i=1 ♣Fi♣ and equivalent to Vk i=1Fi does not always exist. Also, given an ESD F, an ESD equivalent to ≻F and of size polynomial in ♣F♣ does not always exist.

Proof sketch. This is clear for disjunction: ESD allows the _ connective. For conjunction, let Fi be an ESD equivalent to K(xi = yi)_K(xi 6= yi). Clearly, Â k i=1 ♣Fi♣ is linear in k; yet it can be shown that the smallest ESD equivalent to Vk i=1Fi has size exponential in k. Finally, since Vk i=1 Fi ⌘ ≻ Wk i=1≻Fi, if negation were polysize, conjunction also would.

However, bounded conjunction can be computed efficiently on ESDs that are explicitly ordered:

Proposition 14. Given two explicitly ordered ESDs F1↪F2, an explicitly ordered ESD for F1 ^F2 can be computed in quadratic time.

Proof sketch. One can design an algorithm akin to "apply" on OBDDs [Bryant, 1986], relying on rules (i) (Y1 _Y2)^Y⌘ (Y1 ^Y)_(Y2 ^Y) and (ii) spl(x↪Y1↪Y2)^spl(x↪Y3↪Y4) ⌘ spl(x↪Y1^Y3↪Y2^Y4) (explicit ordering guarantees that the current split atom is the same).

We finally consider forgetting. Given a variable x and a structure M, Fo(x↪M) is defined to be the structure M♣x [M♣x. For a subjective formula F, Fo(x↪F) is any formula Y satisfying Mod(Y) = ¶Fo(x↪M) ♣ M 2 Mod(F)♦; this is naturally extended to forgetting sets of variables. Forgetting turns out to be polytime for explicitly ordered ESD, but only when restricted to a bounded number of variables.

Proposition 15. Given an explicitly ordered ESD F and a propositional variable x, an ESD for Fo(x↪F) can be computed in polytime. However, given a set Y of variables, it is not guaranteed that there is a polysize ESD for Fo(Y↪F).

Proof. Clearly, forgetting distributes over _. Now let F = spl(y↪F1↪F2). If x>y, then spl(y↪Fo(x↪F1)↪Fo(x↪F2)) is appropriate, and x < y cannot occur because F is explicitly ordered, so let F = spl(x↪F1↪F2). It follows from the definitions that Fo(x↪F) is equivalent to Y=F1 ✏F2 defined by Mod(Y)=¶M1[M2 ♣M1 ♣=F1↪M2 ♣=F2♦. Finally, it can be shown that binary ✏ can be applied efficiently on explicitly ordered ESDs, using an algorithm similar to the one sketched above for binary ^. Now the negative result can be lifted from OBDD, by considering the case Fo(Y↪Kj) ⌘ K(Fo(Y↪ j)).

6 Succinctness

We now turn to the comparison of the three languages with respect to their ability to represent S5 formulas compactly.

Definition 16. A language L1 is at least as succinct as another language L2, denoted by L1 s L2, if and only if there exists a polynomial P verifying that for any formula F2 in L2, there exists an equivalent F1 in L1 such that ♣F1♣ P(♣F2♣).

The succinctness relation is a preorder; we write L1 6?s L2 if both L1 ⇥s L2 and L1 ⇤s L2 hold, that is, if the two languages are incomparable with respect to succinctness. The following proposition shows that it is the case for two pairs of our three languages when restricted to positive epistemic formulas (we denote by L+ the language L restricted to positive formulas).

Proposition 17. EDNF+ 6?s EBDD+ and EDNF+ 6?s ESD+ hold.

Proof. We first show EBDD+ ⇥s EDNF+. Let (jn)n be a family of DNFs such that for no polynomial P does there exist a family of OBDDs (yn)n with 8n↪yn ⌘ jn and ♣yn♣  P(♣fn♣) (such a family exists since OBDD 6?s DNF, see Darwiche and Marquis [2002]). Consider the family (Kjn)n of formulas in EDNF+ (actually, of epistemic atoms). It can be shown that the smallest representations of Kjn in EBDD are of the form Kyn for some OBDD yn ⌘ jn. Since by assumption such yn is exponentially larger than jn, we indeed get EBDD+ ⇥s EDNF+.

We can show EDNF+ ⇥s EBDD+ similarly, using OBDDs which have no equivalent polysize DNFs. Now, for ESD, using the construction of Prop. 6 we can show that a smallest ESD for Kj (j 2 OBDD) has essentially the same size as j, hence the proof of EDNF+ 6?s EBDD+ works for EDNF+ 6?s ESD+.

As a corollary, we get ESD 6?s EDNF (since if any ESD could be turned into a polysize EDNF, it would be the case in particular for positive formulas, and conversely), and we recover EBDD 6?s EDNF [Bienvenu et al., 2010, Prop. 17].

We are thus left with comparing ESD and EBDD. We show that they are incomparable in general, but that ESD is strictly more succinct on positive formulas.

Proposition 18. It holds that ESD⇥s EBDD.

Proof sketch. Let F be the EBDD Vn i=1≻K(ji), with ji an OBDD for x $ xi, and assume 8i↪x < xi. The smallest ESD equivalent to F is WI✓¶1↪▷▷▷↪n♦ spl(x↪ Vi2I ≻Kxi↪ Vi ◁2I ≻Kxi) (not proven here for space reasons), which is exponentially larger than F.

Proposition 19. ESD+ is strictly more succinct than EBDD+ (and, as a corollary, it holds that EBDD 6?s ESD).

Proof. A formula in EBDD+ is simply a disjunction of positive atoms Kfi, with each fi an OBDD. From Proposition 6 and the fact that _ is a connective in ESD, we get ESD+ s EBDD+.

Now consider the family of formulas (Fn)n, with Fn = Vn i=1(Kxi _Kxi). It can be seen that the only EBDD equivalent to Fn is Wt(Kt), where t ranges over all 2 n terms on x1↪ ▷ ▷ ▷ ↪xn (represented as OBDDs). Now, it can also be seen that the ESD of Figure 1 (middle) is equivalent to Fn and has size linear in n; hence ESD+ ⇤s EBDD+. This in turn entails ESD ⇤s EBDD, and EBDD 6?s ESD with Proposition 18.

Interestingly, note that representing in s-S5-DNFL↪L0 the family (Fn)n used in the previous proof requires exponential space for any choice of L↪L0 , since the proof works at the epistemic level. This shows that even the language built as the union of all s-S5-DNFL↪L0 languages (over all languages L↪L0 ) is not at least as succinct as ESD for representing positive epistemic formulas. This spatial efficiency of ESD does not hold only for positive epistemic formulas: as seen in the previous section, ESD can succinctly represent atoms of the form Oj, while s-S5-DNFL↪L0 cannot (whatever L↪L0 ). This gives an example of formulas which are not positive and on which ESD is more succinct than s-S5-DNFL↪L0 as a whole.

Finally, the following result intuitively shows that while transforming a positive ESD into an equivalent EBDD can require exponential space, it is not actually difficult.

Proposition 20. There exist a polynomial P and an algorithm transforming any formula F in ESD+ into the (unique) equivalent formula Y in EBDD+ in time bounded by P(♣F♣↪ ♣Y♣).

Proof. The algorithm simply consists in "pushing the disjunctions upwards" in the ESD, i.e., replacing bottom-up each node spl(x↪F1 _F2↪F3) by spl(x↪F1↪F3) _ spl(x↪F2↪F3) (and symmetrically for disjunctions in the other child). Clearly, this process converges to an equivalent ESD which is structurally equal to Y. Since the size of the ESD only increases at each step, the process is output-polynomial.

This gives an interesting perspective about the relation between the two languages: while EBDD+ can support queries that ESD+ does not support, this proposition guarantees that ESD+ will only perform polynomially worse than EBDD+ on these queries. All in all, positive formulas are generally more compact in ESD, and in the worst case we can always "uncompress" the formula and fall back on EBDD.

7 Experiments

To investigate the languages in practice, we ran experiments on randomly drawn scenarios inspired from planning. Our first set of experiments focused on positive formulas, by running offline progressions of belief states by actions test(ji). For each run, we drew m actions of the form test(ji) (i = 1↪ ▷ ▷ ▷ ↪m), with ji a random (uniform, satisfiable) term of a given size t. Then, starting from F0 =>, we iteratively computed the belief state Fi, i = 1↪ ▷ ▷ ▷ ↪m, by progressing Fi-1 through test(ji), that is, by computing Fi-1 ^(Kji _K≻ji). For instance, with t = 3, a possible term was x4 ^ x1 ^ x2, yielding progression by K(x4 ^ x1 ^ x2) _ K(x4 _ x1 _ x2).

We ran experiments with a moderate and a larger number of variables (n=15 and n=30; recall that there are 2 2 n structures over n atoms!) with term sizes t = 1↪3↪7, and numbers of actions m = 1↪ ▷ ▷ ▷ ↪ 18. For each tuple (n↪ t ↪ m), we averaged the results over 100 runs. Figure 2 plots the size of the final belief state Fm, and the time taken for computing it iteratively from F0. It can be seen that ESD provides the most compact representations, especially for small terms: as terms get larger (e.g., t = 7), feedbacks Kji are most constrained and the set of belief states shrinks, masking the differences between ESDs and EBDDs. On the other hand, it can be seen that in practice, EDNF does not provide compact representations. For running time, the advantage of ESD over EBDD and EDNF is not so clear; the gain in compactness in ESD comes with some computational overhead in practice (notably, reduction operations).

We also experimented on entailment: at the end of each run, we decided Fm ♣= (Kxi _K≻xi) for all atoms xi. The results (not reported here for lack of space) show that all three languages are very efficient at this, even when Fm is large.

We performed a second set of experiments, with the same setup except that for each feedback Kji and K≻ji, a polarity was drawn uniformly: for instance, the i-th action could yield an epistemic progression by Kji _≻K≻ji. Results (again not reported in detail) show that for this setting the most interesting language is EBDD, both in succinctness and computation time. Both EDNF and ESD are clearly worse, and EDNFs tend to be more compact but not more efficient than ESDs.

Finally, we experimented interleaving progression by test(ji)'s (with positive feedbacks) and progression by ontic actions similar to conditional STRIPS actions, such as y = (x1 ^x02 ^x03 )_(x1 ^x01 ^x03 ), which sets x2↪x3 to > in states satisfying x1, and x1 to > and x3 to ? in other states. Progressing a belief state Fi-1 by an ontic action y essentially consists in computing Fi-1 ^Ky and forgetting all nonprimed atoms in the result. We thus aimed at measuring the efficiency of forgetting in all three languages. The results show that forgetting is cheap for all languages, and we observed the same trends as in the first set of experiments.

8 Conclusion

We introduced the language ESD of epistemic splitting diagrams for representing subjective S5 formulas. We investigated ESD and the known languages s-S5-DNFDNF↪CNF and s-S5-DNFOBDD↪OBDD (called EDNF and EBDD here), both from the viewpoint of knowledge compilation and with experiments on random scenarios inspired from contingent planning. This is to our knowledge the first empirical study on effective S5 representations, although work in planning addressed specific issues of representation [e.g. Hoffmann and Brafman, 2005].

Our theoretical and empirical results complement each other. On positive formulas, ESD is more succinct than EBDD, while supporting mostly the same queries and transformations; this was confirmed by the experiments. On the other hand, both are incomparable to EDNF for succinctness, yet in practice EDNFs are clearly less compact. Experiments also show that computations are heavier on ESD, partly balancing succinctness. The picture is different on general formulas, for which EBDD turns out to be very succinct and efficient.

A short-term perspective of this work is to revisit with efficient representations, and notably EBDD and ESD, the standard planning approaches that (explicitly or not) use S5 reasoning.