Tuning the program transformers from LCC to PDL

Tuning the Program Transformers from LCC to PDL Pere Pardo Ruhr-Universität Bochum, Germany. [email protected] Enrique Sarrión-Morillo, Fernando Soler-Toscano Universidad de Sevilla, Spain. {esarrion,fsoler}@us.es Fernando R. Velázquez-Quesada Universiteit van Amsterdam, The Netherlands. [email protected] Abstract This work proposes an alternative definition of the so-called program transformers used to obtain reduction axioms in the Logic of Communication and Change (LCC). Our proposal uses an elegant matrix treatment of Brzozowski’s equational method instead of Kleene’s translation from finite automata to regular expressions. The two alternatives are shown to be equivalent, with Brzozowski’s method having the advantage of generating smaller expressions for models with average connectivity. Keywords: Logic of communication and change, dynamic epistemic logic, propositional dynamic logic, action model, program transformer, reduction axiom 1 Introduction Dynamic Epistemic Logic [1, 2] (DEL) encompasses several logical frameworks whose main aim is the study of different single- and multi-agent epistemic attitudes and the way they change due to diverse epistemic actions. These frameworks typically have two building blocks: a ‘static’ component, using some ‘epistemic’ model to Vol. 5 No. 1 2018 Journal of Applied Logics — IFCoLog Journal of Logics and their Applications Pardo, Sarrión-Morillo, Soler-Toscano and Velázquez-Quesada represent the notion to be studied (e.g., knowledge or belief), and a ‘dynamic’ component, using model operations to represent actions that affect such notion (e.g., announcements or belief revision).1 Among the diverse existing DEL frameworks, the Logic of Communication and Change (LCC) of [6] stands as one of the most interesting. It consists of Propositional Dynamic Logic [7] (PDL), interpreted epistemically (its ‘static’ component), and the action models machinery [8, 9] for representing knowledge about actions (its ‘dynamic’ component). The LCC framework allows us to model not only diverse epistemic actions (as public, private or secret announcements) but also factual change. A key feature of this logic is that it characterises the effect of an action model’s execution via reduction axioms: valid formulas through which it is possible to rewrite a formula with action model (update) modalities as an equivalent one without them, thus reducing LCC to PDL and hence providing a compositional analysis for a wide range of informational events. For example, the reduction axiom for conjunction tells us that φ∧ψwill be the case true after the pointed action model (U,ei)is executed, [U,ei](φ∧ψ), if and only if both φand ψare true after executing such action, [U,ei]φ∧[U,ei]ψ. For another example, the reduction axiom for atoms p effectively reduces an LCC formula [U,ei]pinto a formula about the conditions of the action eiand its effect on p(see Table 1). As one might expect, the crucial reduction axiom is the one characterising the effect of an action model over epistemic modalities π(i.e. over PDL programs): [U,ei][π]φ↔ n−1 ∧ j=0 [TU ij (π)][U,ej]φ This axiom, presented in detail in what follows, characterises the epistemic change that the action model Ubrings about: after the pointed action model (U,ei)is executed, every π-path in the resulting epistemic model leads to a φ-world, [U,ei][π]φ, if and only if, for every action ejin the action model U, every TU ij (π)-path in the original epistemic model ends in a world that, after the execution of (U,ej), will satisfy φ. The axiom is based on the correspondence between action models and finite automata observed in [10]; its main component, the so-called program transformer function TU ij , follows Kleene’s translation from finite automata to regular expressions [11].2 1This form of representing the dynamics is different from other approaches as, e.g., epistemic temporal logic [3, 4] (ETL), in which the static model already describes not only the relevant notion but also all the possible ways it can change due to the chosen epistemic action(s). See [5] for a comparison between DEL and ETL. 2See [12] for a deep discussion about the meaning of Kleene’s theorem. 72 Tuning the Program Transformers from LCC to PDL The present work proposes an alternative definition of program transformer, using instead a matrix treatment of Brzozowski’s equational method for obtaining an expression representing the language accepted by a given finite automaton [13, 14]. Structure of the paper The paper starts in Section 2 by recalling the LCC framework together with its reduction axioms and its definition of program transformers. Section 3 explains how we can obtain, through Brzozowski’s equational method, the corresponding expressions for Kleene closure, and then Section 4 introduces this paper’s proposal, used to define an alternative translation from LCC to PDL. Section 5 comments on the computational complexity of this approach; the computational costs of the two methods are also compared using Prolog with different test-cases. Section 6 presents a summary and a discussion of further topics for research. 2 Logic of Communication and Change This section recalls LCC’s semantic structure, its language and semantic interpretation, and its axiom system. Throughout this paper, Var will denote a set of atoms (propositional variables), and Ag will denote a finite set of agents. We start the definition of LCC by introducing the involved structures. First, the structure over which LCC formulas are interpreted. Definition 1 (Epistemic model).An epistemic model Mis a triple (W, ⟨Ra⟩a∈Ag, V ) where W=∅is a set of worlds, Ra⊆(W×W)is an epistemic relation for each agent a∈Ag and V:Var →℘(W)is an atomic evaluation. Note how the epistemic relations Raare not required to satisfy any particular property. As usual, each possible world can be interpreted as a possible state of affairs (each one of them defined by the atomic valuation), and each relation Ra represents agent a’s uncertainty about the situation: at world w, for agent aall worlds usuch that wRauare epistemically possible, i.e. are seen as possible by this agent. Figure 1 shows an example of an epistemic model. Here is the structure for representing the knowledge about actions in the system. Definition 2 (Action model).Let Lbe a language built upon Var and Ag that can be interpreted over epistemic models. An Laction model Uis a tuple (E,⟨Ra⟩a∈Ag,pre,sub) 73 Pardo, Sarrión-Morillo, Soler-Toscano and Velázquez-Quesada ...... p.¬p . abc . abc . bc Figure 1: An epistemic model Mwith an actual p-world (gray) and a possible world with ¬p(white). The arrows represent accessibility relations Ra,Rband Rc, so only agent aknows that currently p, while band cignore whether p. where E={e0, . . . , en−1}is a finite non-empty set of actions, Ra⊆(E×E)is a relation for each a∈Ag,pre :E→ L is a precondition map assigning a formula pre(e)∈ L to each action e∈E, and sub : (E×Var)→ L is a postcondition map assigning a formula sub(e, p)∈ L to each atom p∈Var at each action e∈E. The postcondition map should only change a finite number of atoms, so sub(e, p)=p can hold only for a finite number of p∈Var.3We emphasise that, in this definition, the language Lis just a parameter. Just as each relation Radescribes agent a’s uncertainty about the situation, each relation Rarepresents a’s uncertainty about the executed action: eRafindicates a cannot distinguish ffrom e. Note, again, how the relation is not required to satisfy any particular property. Example 1 (Announcements).Figure 2 illustrates three action models for announcements in a set of three agents Ag ={a, b, c}. Each of the actions, say f, is purely epistemic (i.e., fact-preserving), so sub(f, p) = pfor any p∈Var. Labeled arrows denote accessibility relations Ra,Rbor Rc; a gray circle denotes the action that is actually being executed, while other actions (wrongly believed by some agents to possibly take place) are represented by white circles. The preconditions are written below the corresponding actions. As mentioned, action models represent both the actions and the knowledge agents have about these actions. Action models modify epistemic models in the following way. Definition 3 (Update execution).Let M= (W, ⟨Ra⟩a∈Ag, V )be an epistemic model and U= (E,⟨Ra⟩a∈Ag,pre,sub)an Laction model, both over Var and Ag. Recall 3These ‘finiteness’ requirements (finite domain and only a finite number of atoms affected by the postcondition function) are needed to allow the pointed action model (U,e)—a pair with Uan Laction model and ea distinguished action in it— to be associated to a syntactic object and thus to be used within formulae. For details, the reader is referred to the discussion about action models in Section 6.1 of [1]. 74 Tuning the Program Transformers from LCC to PDL ...... p!a Ag . p!a b . ¬p!a b .p†a b .p!a b . skipa . p.¬p .p . p . ¬p . ⊤ . abc . abc . abc . c .a . ab . abc . b . c . c Figure 2: (Top left) A truthful public announcement by athat p, denoted p!a Ag. (Bottom left) A private announcement by ato babout p, denoted p!a b; here agent c only knows about the ‘topic’ of the message. (Right) A secret lie about pmade by ato b, denoted p†a b, is accepted by bas truthful, i.e. as if it was p!a b; agent cis not aware of any communication between aand b. that Lis any language built upon Var and Ag that can be interpreted over epistemic models, so we can assume the existence of a function [·]Mreturning those worlds in Min which each formula of Lholds. The update execution of Uon Mproduces an epistemic model (M⊗U) = (WM⊗U,⟨RM⊗U a⟩a∈Ag, V M⊗U) given, for every a∈Ag and p∈Var, by WM⊗U:= {(w, e)∈W×E|w∈[pre(e)]M} RM⊗U a:= {⟨(w, e),(v, f)⟩ ∈ WM⊗U×WM⊗U|wRavand eRaf} VM⊗U(p):= {(w, e)∈WM⊗U|w∈[sub(e, p)]M} Thus, the update execution of Uon Mproduces an epistemic model M⊗U whose domain is the restricted cartesian product of the original models’ domains.4 In M⊗U, a world (w, e)satisfies an atom pif and only if wsatisfied the formula sub(e, p)in M; finally, an agent asees a world (u, f)as possible from (w, e)if and only if she sees ufrom w(in M) and sees ffrom e(in U). If one works with a particular class of epistemic models in which the epistemic relations satisfy specific properties, then the chosen action models should be such that the update execution preserves these properties. This is straightforward in some cases as, e.g., reflexivity, transitivity and symmetry are preserved by update execution when the relations in 4If there is no world in Msatisfying pre(e)for some action ein U, then the resulting structure is not an epistemic model, as its domain is empty. 75 Pardo, Sarrión-Morillo, Soler-Toscano and Velázquez-Quesada the action models are reflexive, transitive and symmetric, respectively. But this is not always the case: for example, seriality is not preserved, even when the involved action models are serial. See Figure 3 for an illustration of different updates in an epistemic model. ...... p . ¬p . p . ¬p . e.p!a b .¬p!a b . ¬p . p . ¬p . p7→ ⊥ . p . p . ¬p . M . U . M⊗U . abc . abc . bc . abc . abc . bc . abc . abc . abc .c . abc . abc . abc . c Figure 3: Two illustrations of update execution in the epistemic model Mfrom Fig. 1 (topmost row here), where only agent aknows that p. (Left) Action erepresents a public (i.e. publicly observable) change to ¬p; note that the postcondition is written on top of the action. After execution, it becomes common knowledge that ¬p. (Right) A private announcement by ato babout presults in a new model where it is public that bnow knows whether p, and only cremains ignorant about p. With the semantic structures already defined, it is time now to define the language that will be used to describe them. Note that the formulas (and programs) of the language LLCC are defined simultaneously with the notion of an LLCC action model (i.e. an action model using LLCC for its precondition and postcondition maps). Definition 4 (Language LLCC).The formulas φand programs πof the language LLCC are given by, respectively: φ::= ⊤ | p| ¬φ|φ∧φ|[π]φ|[U,e]φ π::= a|?φ|π;π|π∪π|π∗ where p∈Var,a∈Ag and (U,e)is a pair with an LLCC action model Uand an action ein this model.5 5More precisely, the language is defined by a double induction starting from the language PDL0=PDL, then defining L0 LCC as PDL0plus modalities of the form [U,e]for UaPDL0action model, then defining PDL1as L0 LCC plus tests ?φfor φ∈ L0 LCC, then defining L1 LCC as PDL1plus modalities of the form [U,e]for UaPDL1action model, and so on. The full language LLCC is then the union of all languages Li LCC with ifinite. 76 Tuning the Program Transformers from LCC to PDL As the definition states, the set of LCC formulas contains the atomic propositions and ⊤, and it is closed under negation, conjunction, and modalities [π](for πa program) and [U,e](for Uan LLCC action model and ean action in it).6On the other hand, the set of LCC programs contains basic programs for agents aand ‘tests’ ?φ(with φa formula), and it is closed under sequential composition (;), non-deterministic choice (∪) and Kleene closure (∗). It is only left to define the [·]Mfunction associated to LLCC that collects the worlds of a given epistemic model Min which a given LLCC formula holds. In the case of LCC, this function also indicates which pairs of worlds are related by a given LLCC program. Definition 5 (Semantics of LLCC).Let M= (W, ⟨Ra⟩a∈Ag, V )be an epistemic model and U= (E,⟨Ra⟩a∈Ag,pre,sub)an action model. The function [·]M, returning both those worlds in Win which an LLCC formula holds and those pairs in W×Win which an LLCC program holds, is given by [⊤]M:= W[a]M:= Ra [p]M:= V(p)[?φ]M:= Id[φ]M [¬φ]M:= W\[φ]M[π1;π2]M:= [π1]M◦[π2]M [φ1∧φ2]M:= [φ1]M∩[φ2]M[π1∪π2]M:= [π1]M∪[π2]M [[π]φ]M:= {w∈W| ∀v((w, v)∈[π]M⇒v∈[φ]M)}[π∗]M:= ([π]M)∗ [[U,e]φ]M:= {w∈W|w∈[pre(e)]M⇒(w, e)∈[φ]M⊗U} where ◦and ∗are the composition and the reflexive transitive closure operator, respectively, and IdUis the identity relation on U⊆W. Notice two special cases for test:[?⊥]M=∅and [?⊤]M=IdW. Even though LCC can be seen abstractly as the logic of regular programs (the PDL part) plus action models (modalities of the form [U,e]), it is also illustrative to discuss its epistemic interpretation, in particular, that of its PDL programs. Basic ‘agent’ programs a∈Ag produce formulas of the form [a]φ, read simply as “agent aknows/believes φ”as in standard Epistemic Logic. More complex programs also have epistemic readings. Formulas of the form [π1;π2]φ, relying on the sequential composition π1and then π2, can be read as “π1knows/believes that π2knows/believes φ”, and thus can be used to express nested knowledge/belief; formulas of the form [π1∪π2]φ, relying on the union of the relations for π1and π2, can be read as “both π1 and π2know/believe φ”, and thus can be used to express general knowledge/belief among a group; finally, formulas of the form [π∗]φ, relying on the reflexive and 6From now on, all action models are assumed to be LLCC action models. 77 Pardo, Sarrión-Morillo, Soler-Toscano and Velázquez-Quesada transitive closure of the relations for π, can be read as “φis the case, πknows it, πknows that she knows it, and so on”, and thus can be used to express common knowledge (or, if π+:= π;π∗is used instead of π∗,common belief). The modalities involving action models simply state the action’s effects, with formulas of the form [U,e]φreading “φis the case after any execution of the pointed action (U,e)”. Axiom system The axiom system for LCC, shown in Table 1, combines the known axiom system of its PDL fragment (the left column; [7]) with recursion axioms for its action model fragment (the right column). Intuitively, recursion axioms are valid formulae characterising a situation after an update execution in terms of a situation before such update, and thus indicating how to rewrite a formula with an action model modality as a provably equivalent one without them. Then, while soundness follows from the validity of these new axioms, completeness follows from the completeness of the basic system.7 (taut) propositional tautologies (top)[U,e]⊤ ↔ ⊤ (K)[π](φ1→φ2)→([π]φ1→[π]φ2)(atm)[U,e]p↔(pre(e)→sub(e, p)) (test)[?φ1]φ2↔(φ1→φ2)(neg)[U,e]¬φ↔(pre(e)→ ¬[U,e]φ) (seq)[π1;π2]φ↔[π1][π2]φ(conj)[U,e](φ1∧φ2)↔([U,e]φ1∧[U,e]φ2) (choice)[π1∪π2]φ↔[π1]φ∧[π2]φ(KU)[U,e](φ1→φ2)→([U,e]φ1→[U,e]φ2) (mix)[π∗]φ↔φ∧[π][π∗]φ(prog)[U,ei][π]φ↔∧n−1 j=0 [TU ij(π)][U,ej]φ (ind)φ∧[π∗](φ→[π]φ)) →[π∗]φ(NU) From ⊢φinfer ⊢[U,e]φ (MP) From ⊢φ1and ⊢φ1→φ2infer ⊢φ2 (Nπ) From ⊢φinfer ⊢[π]φ Table 1: LCC calculus in [6] is that of PDL (left column) plus reduction axioms and necessitation rule for [U,e](right column). In our particular case, recursion axioms for atomic propositions and boolean constants/operators are standard for action models with ontic (i.e., valuation) change [16]: while axiom (atm) states that an atom pwill be the case after any update execution with action model Uand action e,[U,e]p, if and only if, before the update, the formula sub(e, p)holds whenever pre(e)holds, pre(e)→sub(e, p), axioms (neg) and (conj) state that update execution commutes with negation (modulo its precondition) and distributes over conjunction, respectively. 7The reader is referred to Chapter 7 of [1] (see also [15]) for an extensive explanation of this technique. 78 Tuning the Program Transformers from LCC to PDL The most important recursion axiom, (prog), characterises the effect of an action model over LCC programs. It states that after any update execution with Uon ei every π-path in the resulting model will lead to a φ-world, [U,ei][π]φ, if and only if, before the update, every TU ij (π)-path leads to a world that will satisfy φafter any update execution with Uon ejwhere ejis any action on U,∧n−1 j=0 [TU ij (π)][U,ej]φ. In this axiom, the program transformer TU ij is crucial, taking an LCC program π representing a path on M⊗Uand returning an LCC program TU ij (π)representing a ‘matching’ path on M, taking additional care that such path can be also reproduced in the action model U. A program transformer follows Kleene’s translation from finite automata to regular expressions [11], and it is formally defined as follows. Note also that the (valid) formula KUis not listed among the LCC axioms in [6]. It has been added here not only because it cannot be derived from the rest of the system, but also because it allows the derivation of the crucial rule χ↔ψ [U,e]χ↔[U,e]ψREU This rule is needed for the inside-out translation of nested action model modalities (see footnote 10). The fact that KUis not derivable from the rest of the system is stated in [15] (in particular, its Thm. 29), a paper which examines axiom systems for PAL, the logic of public announcements [φ!]. Their analysis of completeness proofs is based on a reduction from PAL, and thus it applies to LCC as well. (Of course, another alternative is to add REUdirectly since, following [15, Prop. 3], KU is derivable from REUand the original LCC system, Table 1 minus KU.) That the system on Table 1 is indeed sound and (weakly) complete w.r.t. the given semantic interpretation can be shown using the same technique as [15, Corollary 12]. Definition 6 (Program transformer [6]).Let U= (E,⟨Ra⟩a∈Ag,pre,sub)be an action model with E={e0, . . . , en−1}. The program transformer TU ij (i, j ∈ {0, . . . , n −1}) on the set of LCC programs is defined as: TU ij(a) := {?pre(ei);aif eiRaej ?⊥otherwise TU ij(?φ) := {?(pre(ei)∧[U,ei]φ)if i=j ?⊥otherwise TU ij(π1;π2) := ∪n−1 k=0(TU ik(π1);TU kj(π2)) TU ij(π1∪π2) := TU ij(π1)∪TU ij(π2) TU ij(π∗) := KU ijn(π) with KU ijn inductively defined as follows: 79 Pardo, Sarrión-Morillo, Soler-Toscano and Velázquez-Quesada The function SU k(with 0≤k≤n), defined as SU k(M|A) :=    Aif k=n SU k+1(Subsk(Ardk(M|A))) otherwise (22) receives an argument M|Aand performs an iterative process applying Arden’s Theorem to row k(via function Ardk:Mn×2n→ Mn×2n) and substituting rows different from k(via function Subsk:Mn×2n→ Mn×2n) until a k=n, then returning the right part of the augmented matrix. The two auxiliary functions, Ardkand Subsk, are given by Ardk(N)[i, j] :=                N[i, j]if i=k ?⊥if i=k=j N[i, j]if i=k=jand N[k, k] = ?⊥ N[k, k]∗⊙N[i, j]otherwise (23) Subsk(N)[i, j] :=          N[i, j]if i=k ?⊥if i=k=j ⊕{N[i, k]⊙N[k, j], N[i, j]}otherwise (24) The operators ‘⊕’ and ‘⊙’ used in the previous definition are versions of nondeterministic choice and sequential composition that remove unnecessary occurrences of ?⊥and ?⊤; thus returning programs that are (potentially) syntactically shorter but nevertheless semantically equivalent to their PDL counterparts ‘∪’ and ‘;’, as the following propositions show. Proposition 1. Let Mbe an epistemic model and Γa set of LCC programs. Then, [⊕Γ]M=[∪Γ]M Proof. Take any epistemic model M. Equation (17) states that ⊕Γis a nondeterministic choice of the LCC programs in Γthat returns ∪(Γ\{?⊥})when Γis different from both ∅and {?⊥}, and ?⊥otherwise. In the first case, [⊕Γ]M=[∪Γ]M because [∪Γ]M=[∪(Γ \ {?⊥})]M; in the second, [⊕Γ]M=[∪Γ]Mbecause [∪∅]M=[∪{?⊥}]M=[?⊥]M=∅. Proposition 2. Let Mbe an epistemic model and σ, ρ two LCC programs. Then, [σ;ρ]M=[σ⊙ρ]M 86 Tuning the Program Transformers from LCC to PDL Proof. Take any epistemic model M. Equation (19) states that σ⊙ρdiffers from σ;ρonly when either σor else ρis ?⊥or ?⊤. But, in such cases: •[σ;?⊥]M=[?⊥;σ]M=[?⊥]M; hence, [σ;ρ]M=[σ⊙ρ]M. •[σ;?⊤]M=[?⊤;σ]M=[σ]M; hence, [σ;ρ]M=[σ⊙ρ]M. The rest of this section is devoted to prove that the function µUreturns an LCC program that is semantically equivalent to the one returned by the program transformer TUof [6]. Lemma 1. Let U= (E,R,pre,sub)be an action model with ei,ej∈E; let πbe an LCC program. For any epistemic model M, [TU ij (π)]M=[µU(π)[i, j]]M Proof. By induction on the complexity of π. Let Mbe an epistemic model; then (Base Cases: aand ?φ) Trivial, as the definitions of TU ij and µU(π)[i, j]are identical for both aand ?φ. (Ind. Case π1∪π2) Suppose (Ind. Hyp.) the claim holds for π1and π2. Then [TU ij (π1∪π2)]M=[TU ij (π1)∪TU ij (π2)]M(Def. 6) =[TU ij (π1)]M∪[TU ij (π2)]M(Def. of [·]M) =[µU(π1)[i, j]]M∪[µU(π2)[i, j]]M(Ind. Hyp.) =[µU(π1)[i, j]∪µU(π2)[i, j]]M(Def. of [·]M) =[⊕{µU(π1)[i, j], µU(π2)[i, j]}]M(Prop. 1) =[µU(π1∪π2)[i, j]]M(Def. of µU(π1∪π2)in (16)) (Ind. Case π1;π2) Suppose (Ind. Hyp.) the claim holds for π1and π2. Then 87 Pardo, Sarrión-Morillo, Soler-Toscano and Velázquez-Quesada [TU ij (π1;π2)]M=[∪n−1 k=0(TU ik(π1);TU kj(π2))]M(Def. 6) =∪n−1 k=0 ([TU ik(π1)]M◦[TU kj(π2)]M)(Def. of [·]M) =∪n−1 k=0 ([µU(π1)[i, k]]M◦[µU(π2)[k, j]]M)(Ind. Hyp.) =[∪n−1 k=0 (µU(π1)[i, k];µU(π2)[k, j])]M(Def. of [·]M) =[∪n−1 k=0 (µU(π1)[i, k]⊙µU(π2)[k, j])]M(Prop. 2) =[⊕{µU(π1)[i, k]⊙µU(π2)[k, j]|0≤k≤n−1}]M(Prop. 1) =[µU(π1;π2)[i, j]]M(Def. of µU(π1;π2)in (18)) (Ind. Case π∗) Suppose (Ind. Hyp.) the claim holds for πand observe how [π∗]M= [?⊤∪(π;π∗)]M. Now, [TU ij (π∗)]M=[TU ij (?⊤∪π;π∗)]M =[TU ij (?⊤)]M∪[∪n−1 k=0(TU ik(π);TU kj(π∗))]M(Def. 6) =[TU ij (?⊤)]M∪∪n−1 k=0 ([TU ik(π)]M◦[TU kj(π∗)]M)(Def. of [·]M) =[TU ij (?⊤)]M∪∪n−1 k=0 ([µU(π)[i, k]]M◦[TU kj(π∗)]M)(Ind. Hyp.) The last equality produces n2relational equations. By abbreviating [TU ij (π∗)]Mas Xij for every 0≤i, j ≤n−1, we get Xij =[TU ij (?⊤)]M∪ n−1 ∪ k=0 ([µU(π)[i, k]]M◦Xkj)(25) Thus, it is enough to prove that [µU(π∗)[i, j]]Mis a solution for Xij. This is shown in the following three propositions about the functions building µU(π∗). Proposition 3. Take Ω= (µU(π)|AU)(see (20)). Then, Xij =[Ω[i, j +n]]M∪ n−1 ∪ k=0 ([Ω[i, k]]M◦Xkj)(26) Proof. It will be shown that the right-hand side (r.h.s.) of (25) and (26) coincide. Their respective rightmost parts are equivalent since, for 0≤k≤n−1,Ω[i, k] = µU(π)[i, k](recall that Ωis built by adding additional columns at the right of the nfirst columns of µU(π), and the matrix’s indexes start from 0). For the leftmost parts, 88 Tuning the Program Transformers from LCC to PDL [TU ij (?⊤)]M={[?(pre(ei)∧[U,ei]⊤)]Mif i=j [?⊥]Motherwise (Def. 6) ={[?pre(ei)]Mif i=j [?⊥]Motherwise (as [U,ei]⊤is trivially true) =[AU[i, j]]M=[Ω[i, j +n]]M((21) and Def. of Ω) Proposition 4. For 0≤k≤n−1, if Nis a matrix of size n×2nwith all cells in columns 0, . . . , k−1equal to ?⊥, then Subsk(Ardk(N)) contains all cells in columns 0, . . . , k equal to ?⊥. Proof. Start with Ardk(N). Observe in (23) that the only modified cells are in the kth row. Cell Ardk(N)[k, k]in the kth column is converted into ?⊥. With respect to cells in columns from 0to k−1, if they were ?⊥, they continue being ?⊥: those cells N[i, j]do not change, if N[k, k] =?⊥, or otherwise are converted by (23) into N[k, k]∗⊙N[i, j]and, by (19), if N[i, j] =?⊥, then N[k, k]∗⊙N[i, j] =?⊥. Now, call N′the output of Ardk(N)and observe Subsk(N′)’s definition (24): the only cells that change are in rows different to k. With respect to any such row i, the position in the kth column is made ?⊥. For cells in previous columns, j < k, the last case in the definition returns ⊕{N′[i, k]⊙N′[k, j], N′[i, j]}. But as N′is the result of Ardk(N),N′[k, j]is ?⊥(because, as argued above, Ardk(N)works over the kth row and keeps the ?⊥in columns before k). Also, N′[i, j] =?⊥, as columns j < k are filled with ?⊥. So ⊕{N′[i, k]⊙N′[k, j], N′[i, j]}becomes ⊕{N′[i, k]⊙?⊥,?⊥} and, by (17) and (19), it is ?⊥. Proposition 5. Given an n×2nmatrix Nof LCC programs, the equations built using (26), with Ω=Subsk(Ardk(N)),0≤k≤n−1, are correct transformations of the equations built in the same way with Ω=N. Proof. As argued in the proof of Proposition 4, Ardk(N)works only on the kth row. If N[k, k] =?⊥, nothing is done, so according to (26) the equations for Xkj (0≤j≤n−1) do not change. Otherwise, the kth row of Nchanges: all cells N[k, j] with j=kbecome N[k, k]∗⊙N[k, j], except N[k, k]which becomes ?⊥. Then, for every 0≤j≤n−1, the equation for Xkj becomes (using index tinstead of kand removing [?⊥]M◦Xkj from the union): Xkj =[N[k, k]∗⊙N[k, j +n]]M∪∪ 0≤t≤n−1 t=k([N[k, k]∗⊙N[k, t]]M◦Xtj) 89 Pardo, Sarrión-Morillo, Soler-Toscano and Velázquez-Quesada By Proposition 2 and [·]M’s definition, this can be rewritten as Xkj = ([N[k, k]]M)∗◦[N[k, j +n]]M∪ ∪0≤t≤n−1 t=k(([N[k, k]]M)∗◦[N[k, t]]M◦Xtj)(27) which is an application of Arden’s Theorem [20] to the corresponding equation for the original row in N: Xkj =[N[k, j +n]]M∪∪ 0≤t≤n−1([N[k, t]]M◦Xtj)(28) Arden’s Theorem (which works on regular algebras, such as LCC programs) gives X=A∗◦Bas a solution for X= (A◦X)∪B. In (28), Xis Xkj,Ais [N[k, k]]M, and Bis the union of all terms in the r.h.s. of (28) except [N[k, k]]M◦Xkj. Besides Arden’s Theorem, from (28) to (27) we use ◦’s distribution over ∪,A◦(B∪C) = (A◦B)∪(A◦C). Now denote by N′the output of Ardk(N). We move to Subsk(N′)to show that the equations obtained from it with (26) are correct transformations of the equations built from N′. The only modified cells in Subsk(N′)are in rows different to k, so it only affects equations for Xij with i=k. According to (26), if Ω=N′, these equations are (using tinstead of k): Xij =[N′[i, j +n]]M∪ n−1 ∪ t=0 ([N′[i, t]]M◦Xtj)(29) The same equation for Ω=Subsk(N′)becomes the following (we remove from the union the term [?⊥]M◦Xkj, as it is equivalent to ∅): Xij =[⊕{N′[i, k]⊙N′[k, j +n], N′[i, j +n]}]M∪ ∪ 0≤t≤n−1 t=k([⊕{N′[i, k]⊙N′[k, t], N′[i, t]}]M◦Xtj)(30) By using Propositions 1 and 2 and the properties of [·]M, equation (30) becomes Xij = ([N′[i, k]]M◦[N′[k, j +n]]M)∪[N′[i, j +n]]M∪ ∪ 0≤t≤n−1 t=k((([N′[i, k]]M◦[N′[k, t]]M)∪[N′[i, t]]M)◦Xtj)(31) 90 Tuning the Program Transformers from LCC to PDL But note that in the equation for Xkj, which is the same at N′and Subsk(N′), the kth row of N′is not changed by Subsk(N′): Xkj =[N′[k, j +n]]M∪∪ 0≤t≤n−1 t=k([N′[k, t]]M◦Xtj)(32) We have eliminated the term [N′[k, k]]M◦Xkj in (32) because N′=Ardk(N)and by (23), N′[k, k] =?⊥, which produces [N′[k, k]]M◦Xkj =∅. Observe that (31) can be obtained from (29) by replacing Xkj by the r.h.s. of (32) and applying the distribution of ◦over ∪. So the modified equation (30) is equivalent to correct transformations of the original one (29). The proof of the case π∗in Lemma 1 can be finished now. Take the set of relational equations given by (25). By (20), µU(π∗)operates by iterating calls to SU k(with kfrom 0to n) with Ω= (µU(π)|AU)as the initial argument. Let M−1 be Ωand Mkthe output of SU k(Mk−1). By Proposition 3, (26) gives equations equivalent to (25). By Proposition 5, the equations are correct for each successive Mk(0≤k≤n−1). As the calls to SU kare done iteratively with kfrom 0to n−1, Proposition 4 guarantees that, in Mn−1, all cells in columns for 0to n−1are equal to ?⊥. Thus, equations (26) for Mn−1are: Xij =[Mn−1[i, j +n]]M(33) The rightmost union in (26) has disappeared (M[i, k] =?⊥for 0≤k≤n−1, and [?⊥]M=∅). Now, by SU k’s definition in (22), Mn−1[i, j+n] = Mn[i, j] = µU(π∗)[i, j], so Xij =[µU(π∗)[i, j]]M. Then, since Xij represents [TU ij (π∗)]M, [TU ij (π∗)]M=[µU(π∗)[i, j]]M which completes the proof. We can now define new translation functions t′, r′as follows. Note that t′and r′ are defined as the translation functions t, r for formulas φand programs πproposed in [6], with the only exception of formulas of the form [U,ei][π]φ.10 Note also the inside-out approach in the case t([U,e][U′,f]φ) = t([U,e]t([U′,f]φ)), which requires rule REU(with χ= [U′,f]φand ψ=t(χ)) in order to prove that the translation is indeed provably equivalent (i.e. ⊢ϕ↔t(ϕ)). 10Two minor typos for the cases [U,e]pand [U,ei][π]φare also corrected here w.r.t. [6] (the first was given by t(pre(e)) →sub(e, p), and the second by ∧n−1 j=0 [TU ij(r(π))]t([U,ej]φ)). 91 Pardo, Sarrión-Morillo, Soler-Toscano and Velázquez-Quesada t′(⊤) = ⊤r′(a) = a t′(p) = p r′(B) = B t′(¬φ) = ¬t′(φ)r′(?φ) =?t′(φ) t′(φ1∧φ2) = t′(φ1)∧t′(φ2)r′(π1;π2) = r′(π1);r′(π2) t′([π]φ) = [r′(π)]t′(φ)r′(π1∪π2) = r′(π1)∪r′(π2) t′([U,e]⊤) = ⊤r′(π∗) = (r′(π))∗ t′([U,e]p) = t′(pre(e)) →t′(sub(e, p)) t′([U,e]¬φ) = t′(pre(e)) → ¬t′([U,e]φ) t′([U,e](φ1∧φ2)) = t′([U,e]φ)∧t′([U,e]φ2) t′([U,ei][π]φ) = ∧0≤j≤n−1 µU(π)[i,j]=?⊥ [r′(µU(π)[i, j])]t′([U,ej]φ) t′([U,e][U′,e′]φ) = t′([U,e]t′([U′,e′]φ)) Corollary 1. The translation functions t′, r′reduce the language of LCC to that of PDL. This translation is correct. Proof. The effective reduction from LCC to PDL is immediate by inspection. Its correctness follows from that in [6], with Lemma 1 for the case [U,ei][π]φ. Definition 8. We define a new axiom system for LCC by replacing the reduction axiom for PDL programs with the following [U,ei][π]φ↔∧ 0≤j≤n−1 µU(π)[i,j]=?⊥ [µU(π)[i, j]][U,ej]φ(prog) Corollary 2. The axiom system for LCC from Def. 8 is sound and complete. Proof. The only new axiom, that for PDL-programs, is sound by Lemma 1. For completeness, the proof system for PDL is complete, and every LCC formula is provably equivalent to a PDL formula using Corollary 1. 5 Complexity of the new transformers The original program transformers in [6] require exponential time due to the use of Kleene’s method [11]. Moreover, the size of the transformed formulas of type π∗is also exponential because of the definition of KU ijn (Def. 6). In order to study the complexity of our program transformers, we first implemented in Prolog both the original program transformers and our matrix calculus. Figure 5 shows the result for our transformers for two kinds of models, complete and chain models, from 1 to 20 states. The graph’s vertical axis, which is shown in 92 Tuning the Program Transformers from LCC to PDL logarithmic scale, presents the number of PDL operators in the transformed program µU(π∗)[n−1,0] for nthe number of states in the model. Figure 5: Number of PDL connectives in µU(π∗)for different action models A model is complete when it is fully connected, i.e., when each µU(π)[i, j] = s(i, j) is an atomic expression (which is not further analysed by the implementations). All values s(i, j)in µU(π)are assumed to be different, avoiding simplifications of repeated patterns. The number of operators in µU(π∗)[n−1,0] is in the order of 22n. In the worst case our transformers produce an exponential output, which implies that the required time is also exponential. In a chain model, each state is connected with itself, the previous and next one. Thus, µU(π)[i, j]is s(i, j)when i=jor |i−j|= 1, and ?⊥otherwise. Now the number of operators in µU(π∗)[n−1,0] is in the order of 2n2, so in this case the length of the output is polynomial. We chose models with chain-like structure because it makes it easier to generate models of increasing size with limited connectivity. Similar results can be obtained for other kinds of models with similar average connectivity, as the key is the number of instances of ?⊥spread along the matrices. The results for the original program transformers are not shown in Figure 5 as they are, for both the complete and chain models, as our worst case. (The reason is that they do not benefit from removing superfluous ?⊥.) An advantage of our transformers is that they do not require exponential space in cases other than the worst one, in contrast with the original transformers which always perform in the same (exponential) way. An additional advantage can be found in the reusability of the information produced during program transformations. As we argued, working with matrices allows to perform several operations in parallel. Indeed, matrix µU(π)contains the transformation of program πwithin all states in the action model U. As building the matrix with the transformations of a given program involves building the matrices for its subprograms, the information 93 Pardo, Sarrión-Morillo, Soler-Toscano and Velázquez-Quesada of each generated matrix is properly stored, and then it can be reused in the same or subsequent transformations within the same action model. This is a practical way to reduce the computation time required for program transformation. 6 Summary and Future Work In this work, we presented an alternative definition of the program transformers used to obtain reduction axioms in LCC. The proposal uses a matrix treatment of Brzozowski’s equational method in order to obtain a regular expression representing the language accepted by a finite automaton. While Brzozowski’s method and that used in the original LCC paper [6] are equivalent, the first is computationally more efficient in cases different to the worst one; moreover, the matrix treatment presented here is more synthetic, simple and elegant, thus allowing a simpler implementation. Towards future work, some definitions used by program transformers (particularly the ⊙operation) can be modified to obtain even simpler expressions. For example, σ⊙ρmight be defined as σif σ= ?⊤=ρand as ρif σ= ?⊤. Moreover, the algorithm implementing Ardkand Subskfunctions can be improved by disregarding the N[i, j]elements with j < k or j > n +k(being N[i, j]an×2nmatrix), since those are necessarily equal to ?⊥. These changes, despite not lowering the translation’s complexity order, would nevertheless make it more efficient. Acknowledgements We would like to thank two anonymous reviewers for their helpful comments. This work is supported by the Spanish Ministry of Economy and Competitiveness, under Research Project FFI2014-56219-P. The research of P. Pardo was supported by a Sofja Kovalevkaja award of the Alexander von Humboldt-Foundation, funded by the German Ministry for Education and Research. This paper is an extended version of a previous conference paper [21] at JELIA 2014. References [1] H. van Ditmarsch, W. van der Hoek, B. Kooi, Dynamic Epistemic Logic, Vol. 337 of Synthese Library Series, Springer, 2007. [2] J. van Benthem, Logical Dynamics of Information and Interaction, Cambridge University Press, 2011. [3] R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi, Reasoning about knowledge, The MIT Press, Cambridge, Mass., 1995. 94 Tuning the Program Transformers from LCC to PDL [4] R. Parikh, R. Ramanujam, A knowledge based semantics of messages, Journal of Logic, Language and Information 12 (4) (2003) 453–467. [5] J. van Benthem, J. Gerbrandy, T. Hoshi, E. Pacuit, Merging frameworks for interaction, Journal of Philosophical Logic 38 (5) (2009) 491–526. doi:10.1007/ s10992-008-9099-x. [6] J. van Benthem, J. van Eijck, B. Kooi, Logics of communication and change, Information and Computation 204 (11) (2006) 1620–1662. doi:10.1016/j.ic.2006.04.006. [7] D. Harel, D. Kozen, J. Tiuryn, Dynamic Logic, MIT Press, Cambridge, MA, 2000. [8] A. Baltag, L. S. Moss, S. Solecki, The logic of public announcements and common knowledge and private suspicions, in: I. Gilboa (Ed.), TARK, Morgan Kaufmann, San Francisco, CA, USA, 1998, pp. 43–56. [9] A. Baltag, L. S. Moss, Logics for epistemic programs, Synthese 139 (2) (2004) 165–224. [10] J. van Benthem, B. Kooi, Reduction axioms for epistemic actions, in: R. Schmidt, I. Pratt-Hartmann, M. Reynolds, H. Wansing (Eds.), Advances in Modal Logic (Number UMCS-04-09-01 in Technical Report Series), Department of Computer Science, University of Manchester, 2004, pp. 197–211. [11] S. Kleene, Representation of events in nerve nets and finite automata, in: C. E. Shannon, J. McCarthy (Eds.), Automata Studies, Princeton University Press, Princeton, NJ, 1956, pp. 3–41. [12] J. Sakarovitch, Automata and rational expressions, CoRR abs/1502.03573. URL http://arxiv.org/abs/1502.03573 [13] J. A. Brzozowski, Derivatives of regular expressions, Journal of the ACM 11 (4) (1964) 481–494. [14] J. H. Conway, Regular Algebra and Finite Machines, Chapman and Hall, 1971. [15] Y. Wang, Q. Cao, On axiomatizations of public announcement logic, Synthese 190 (1) (2013) 103–134. doi:10.1007/s11229-012-0233-5. [16] H. van Ditmarsch, B. Kooi, Semantic results for ontic and epistemic change, in: G. Bonanno, W. van der Hoek, M. Wooldridge (Eds.), Logic and the Foundations of Game and Decision Theory (LOFT7), Vol. 3 of Texts in Logic and Games, Amsterdam University Press, Amsterdam, The Netherlands, 2008, pp. 87–117. [17] H. Gruber, M. Holzer, Finite automata, digraph connectivity, and regular expression size, in: L. Aceto, I. Damgård, L. A. Goldberg, M. M. Halldórsson, A. Ingólfsdóttir, I. Walukiewicz (Eds.), Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, Vol. 5126 of Lecture Notes in Computer Science, Springer, 2008, pp. 39–50. doi:10.1007/978-3-540-70583-3_4. [18] H. Gruber, M. Holzer, Provably shorter regular expressions from finite automata, International Journal of Foundations of Computer Science 24 (8) (2013) 1255–1279. doi:10.1142/S0129054113500330. [19] D. Kozen, On kleene algebras and closed semirings, in: B. Rovan (Ed.), MFCS, Vol. 95