Figures (8)  Tables (4)

    • Figure 1. 

      Left: Initial pointed Kripke model $ {\cal{M}} $. Right: Updated model $ {\cal{M}}^U $ (the actual world $ v $ is dark gray). A formula $ \varphi $ within a circle representing a world means that $ \varphi $ is true in this world. A light-gray rectangle with $ n $ in the top left corner is the cluster that is numbered $ n $. A double arrow from such cluster $ n $ to cluster $ m $ represents a set of accessibility arrows with the same agent's label from every world of cluster $ n $ to every world of cluster $ m $.

    • Figure 2. 

      Left: Initial (pointed) Kripke model $ {\cal{M}} $ where agent $ a $ and $ b $ are uncertain about whether $ p $ or $ \lnot p $ is true. Right: (Pointed) action model $ {\cal{U}} $ for a private message $ p $ to $ a $: agent $ a $ learns $ p $, while $ b $ believes that nothing happened. A formula $ \varphi $ within a square representing an event $ \beta $ is the precondition for this event, i.e., $ \text{pre}(\beta) = \varphi $.

    • Figure 3. 

      Left: First product update $ {\cal{M}} \otimes {\cal{U}} $ of Kripke model $ {\cal{M}} $ with action model $ {\cal{U}} $. Right: Second product update $ ({\cal{M}} \otimes {\cal{U}}) \otimes {\cal{U}} $ with the same action model $ {\cal{U}} $. $ p $ is true in all worlds that start from $ p $ and false in all worlds that start from $ \lnot p $.

    • Figure 4. 

      Third product update $ \bigl(({\cal{M}} \otimes {\cal{U}})\otimes {\cal{U}}\bigr)\otimes {\cal{U}} $ with the same action model $ {\cal{U}} $.

    • Figure 5. 

      Successful update synthesis $ {\cal{M}}\odot {\cal{U}}_\varphi, (v,0) \vDash \varphi $ by applying pointed update with pointed action model $ ({\cal{U}}_ \varphi,0) $ for DBI formula (1) from Example 8 to $ ({\cal{M}},v) $ from Fig. 1 (left).

    • Figure 6. 

      Balder-Loki-Thor updated model using product updates $ {\cal{M}} \otimes {\cal{U}}_\varphi $.

    • Figure 7. 

      Sketch of the result of the iterated product update operation $ ({\cal{M}} \otimes {\cal{U}}_\varphi) \otimes {\cal{U}}_\varphi $. Grey rectangles are a compact way to represent sub-models originating from worlds in the previous model. Dotted arrows are meant to capture the direction of the arrows and the agents involved. Unlike double arrows, they do not represent arrows from and to all worlds in the rectangle, but only from and to some of these worlds. We leave to the reader their identification. Finally, note that the sink is a copy of the previous model.

    • Figure 8. 

      Modal syntactic trees.

    • // initially add the model’s point
      1: $ E^\varphi := \{0\} $
      2: for all $ i \in {\cal{A}} $ do
      3: $ Q^\varphi_{i} := \varnothing $
      4: $ pre(0) := \top $
      5: $ {\text{CreateActionModel (}} \varphi $, $ \langle E^\varphi, R^\varphi, pre^\varphi \rangle $, $ {\text{0)}} $
      6: $ {\text{AddSink}} (\langle E^\varphi, Q^\varphi, pre^\varphi \rangle)$
      7: return $ (\langle E^\varphi, Q^\varphi, pre^\varphi\rangle, 0) $

      Table 1. 

      $ {\text{SynthesizeActionModel}} (\varphi) $.

    • // $\langle E^\varphi, Q^\varphi, pre^\varphi\rangle$ are passed by reference
      1: if $ \varphi = B_i \xi $ for propositional formula $ \xi $ then
      2: $ u':=\text{ComputeAccState}(\langle E^{\varphi},Q^{\varphi},pre^{\varphi}\rangle, u,i) $
      3: $ pre^\varphi(u') := \xi $
      4: else if $ \varphi = B_i \varphi' $ then
      5: $ u' := { \text{ComputeAccState}}(\langle E^\varphi, Q^\varphi, pre^\varphi\rangle, u, i) $
      6: $ { \text{CreateActionModel}}(\varphi', \langle E^\varphi, Q^\varphi, pre^\varphi\rangle, u') $
      7: else if $ \varphi = B_i (\xi \wedge \varphi') $ then
      8: $ u':=\text{ComputeAccState}(\langle E^{\varphi},Q^{\varphi},pre^{\varphi}\rangle, u,i) $
      9: $ \text{CreateActionModel}(\varphi', \langle E^\varphi, Q^\varphi, pre^\varphi\rangle, u') $
      10: $ pre^\varphi(u') := \xi $
      11: else if $ \varphi = \varphi_1 \wedge \varphi_2 $ then
      12: $ { \text{CreateActionModel}}(\varphi_1, \langle E^\varphi, Q^\varphi, pre^\varphi\rangle, u) $
      13: $ { \text{CreateActionModel}}(\varphi_2, \langle E^\varphi, Q^\varphi, pre^\varphi\rangle, u) $

      Table 2. 

      $ {\text{CreateActionModel}} (\varphi, \langle E^\varphi, Q^\varphi, pre^\varphi\rangle, u) $.

    • // $\langle E^\varphi, Q^\varphi, pre^\varphi\rangle$ are passed by reference
      1: create new state $ u' $ (s.t. $ u' \ne 0 $ and $ u' \ne -1 $) with $ \text{pre}^\varphi(u') = \top $
      2: $ E^\varphi := E^\varphi \cup \{u'\} $
      3: $ Q^\varphi_i := Q^\varphi_i \cup \{(u, u'), (u', u')\} $
      4: return $ u' $

      Table 3. 

      $ \text{ComputeAccState}(\left\langle E^{\varphi},Q^{\varphi},pre^{\varphi}\right\rangle, u,i) $.

    • 1: create state $ -1 $, where $ pre^\varphi(-1) = \top $
      2: $ E^\varphi := E^\varphi \cup \{-1\} $
      3: for all $ i \in {\cal{A}} $ do
      4: $ Q^\varphi_i := Q^\varphi_i \cup \{(-1, -1)\} $
      5: for all $ s \in E^\varphi $ do
      6: for all $ i \in {\cal{A}} $ do
      7: if $ (\forall s' \in E^\varphi)\ (s, s') \not\in Q^\varphi_i $ then
      8: $ Q^\varphi_i := Q^\varphi_i \cup \{(s, -1)\} $

      Table 4. 

      $ {\text{AddSink}} $($ \langle E^\varphi, Q^\varphi, pre^\varphi \rangle $).