Abstract
In dynamical multi-agent systems, agents are controlled by protocols. In choosing a class of formal protocols, an implicit choice is made concerning the types of agents, actions and dynamics representable. This paper investigates one such choice: An intensional protocol class for agent control in dynamic epistemic logic (DEL), called ‘DEL dynamical systems’. After illustrating how such protocols may be used in formalizing and analyzing information dynamics, the types of epistemic temporal models that they may generate are characterized. This facilitates a formal comparison with the only other formal protocol framework in dynamic epistemic logic, namely the extensional ‘DEL protocols’. The paper concludes with a conceptual comparison, highlighting modeling tasks where DEL dynamical systems are natural.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Notes
When constructing an action model that produces a pointed Kripke model isomorphic to a particular level in the to-be-generated ETL model, Proposition 3.2 of [21] (which states, roughly, that for almost any two pointed Kripke models, there exists an action model with postconditions that will produce one from the other using product update) is not applicable. The proposition is not applicable as the transforming action model allows only the designated state to survive, from which the desired Kripke model is unfolded. The resulting generated ETL models would therefore (most often) not be ETL isomorphic to the original ETL model, as ETL isomorphisms require that the temporal structure is preserved.
References
Ågotnes, T., van Ditmarsch, H., Wang, Y. (2017). True lies. Synthese, 195(10), 4581–4615.
Artemov, S., Davoren, J., Nerode, A. (1997). Modal logics and topological semantics for hybrid systems. Technical report, Cornell University.
Aucher, G., & Bolander, T. (2013). Undecidability in epistemic planning. In Proceedings of the twenty-third international joint conference on artificial intelligence (pp. 27–33). AAAI Press.
Aucher, G., Maubert, B., Pinchinat, S. (2014). Automata techniques for epistemic protocol synthesis. In Proceedings 2nd international workshop on strategic reasoning, SR 2014, Grenoble, France, April 5–6, 2014 (pp. 97–103).
Baltag, A., & Moss, L.S. (2004). Logics for epistemic programs. Synthese, 139(2), 165–224.
Baltag, A., & Renne, B. (2016). Dynamic epistemic logic. In E.N. Zalta (Ed.) , The Stanford encyclopedia of philosophy. Fall 2016 edition.
Baltag, A., & Smets, S. (2008). A qualitative theory of dynamic interactive belief revision. In G. Bonanno, W. van der Hoek, M. Wooldridge (Eds.) , Logic and the foundations of game and decision theory (LOFT 7), Texts in logic and games (Vol. 3, pp. 9–58). Amsterdam University Press.
Baltag, A., & Smets, S. (2009). Group belief dynamics under iterated revision: fixed points and cycles of joint upgrades. In Proceedings of the 12th conference on theoretical aspects of rationality and knowledge, TARK ’09 (pp. 41–50). New York: ACM.
van Benthem, J. (2002). “One is a lonely number”: logic and communication. In Z. Chatzidakis, P. Koepke, W. Pohlers (Eds.) , Logic colloquium ’02. Lecture notes in logic, 27 (pp. 95–128). Association for Symbolic Logic.
van Benthem, J. (2011). Logical dynamics of information and interaction. Cambridge: Cambridge University Press.
van Benthem, J. (2016). Oscillations, logic, and dynamical systems. In S. Ghosh, & J. Szymanik (Eds.) The facts matter (pp. 9–22). College Publications.
van Benthem, J., & Dégremont, C. (2010). Bridges between dynamic doxastic and doxastic temporal logics. In Logic and the foundations of game and decision theory–LOFT 8 (pp. 151–173). Berlin: Springer.
van Benthem, J., & Smets, S. (2015). Dynamic logics of belief change. In H. van Ditmarsch, J.Y. Halpern, W. van der Hoek, B. Kooi (Eds.) , Handbook of logics for knowledge and belief (pp. 299–368). College Publications.
van Benthem, J., van Eijck, J., Kooi, B. (2006). Logics of communication and change. Information and Computation, 204(11), 1620–1662.
van Benthem, J., Gerbrandy, J., Hoshi, T., Pacuit, E. (2009). Merging frameworks for interaction. Journal of Philosophical Logic, 38(5), 491–526.
Baltag, A., Moss, L.S., Solecki, S. (1998). The logic of public announcements, common knowledge, and private suspicions (extended abstract). In Proceedings of the international conference of TARK 1998 (pp. 43–56). Morgan Kaufmann Publishers.
Blackburn, P., de Rijke, M., Venema, Y. (2001). Modal logic. Cambridge: Cambridge University Press.
Bolander, T., & Birkegaard, M. (2011). Epistemic planning for single- and multi-agent systems. Journal of Applied Non-Classical Logics, 21(1), 9–34.
Bolander, T., Jensen, M.H., Schwarzentruber, F. (2015). Complexity results in epistemic planning. In Proceedings of IJCAI 2015 (24th international joint conference on artificial intelligence).
Dégremont, C. (2010). The temporal mind: observations on the logic of belief change in interactive systems. PhD thesis, University of Amsterdam.
van Ditmarsch, H., & Kooi, B. (2008). 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 (LOFT 7). Texts in logic and games (Vol. 3, pages 87–117). Amsterdam University Press.
van Ditmarsch, H., van der Hoek, W., Kooi, B. (2008). Dynamic epistemic logic. Berlin: Springer.
van Ditmarsch, H., Ghosh, S., Verbrugge, R., Wang, Y. (2014). Hidden protocols: modifying our expectations in an evolving world. Artificial Intelligence, 208, 18–40.
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y. (1995). Reasoning about knowledge. Cambridge: The MIT Press.
Fernández-Duque, D. (2012). A sound and complete axiomatization for Dynamic Topological Logic. Journal of Symbolic Logic, 77(3), 1–26.
Fernández-Duque, D. (2012). Dynamic topological logic of metric spaces. Journal of Symbolic Logic, 77(1), 308–328.
Fernández-Duque, D. (2014). Non-finite axiomatizability of dynamic topological logic. ACM Transactions on Computational Logic, 15(1), 1–18.
Galeazzi, P., & Lorini, E. (2016). Epistemic logic meets epistemic game theory: a comparison between multi-agent Kripke models and type spaces. Synthese, 193(7), 2097–2127.
Gerbrandy, J., & Groeneveld, W. (1997). Reasoning about information change. Journal of Logic, Language and Information, 6(2), 147–169.
Gierasimczuk, N. (2010). Knowing one’s limits. Phd thesis, Institute for Logic, Language and Computation, University of Amsterdam.
Goranko, V., & Otto, M. (2008). Model theory of modal logic. In P. Blackburn, J. van Benthem, F. Wolter (Eds.) , Handbook of modal logic. Elsevier.
Halpern, J.Y., & Moses, Y. (1990). Knowledge and common knowledge in a distributed environment. Journal of the ACM, 37(3), 549–587.
Halpern, J.Y., & Vardi, M.Y. (1988). Reasoning about knowledge and time in asynchronous systems. In Proceedings of the 20th ACM symposium on theory of computing, STOC ’88 (pp. 53–65). ACM.
Halpern, J.Y., & Vardi, M.Y. (1989). The complexity of reasoning about knowledge and time. I. Lower bounds. Journal of Computer and System Sciences, 38 (1), 195–237.
Halpern, J.Y., van der Meyden, R., Vardi, M.Y. (2004). Complete axiomatizations for reasoning about knowledge and time. SIAM Journal of Computation, 33(3), 674–703.
Hintikka, J. (1962). Knowledge and belief: an introduction to the logic of the two notions, 2nd, 2005 edition. London: College Publications.
Hoshi, T. (2009). Epistemic dynamics and protocol information. PhD thesis, ILLC, Universiteit van Amsterdam.
Hoshi, T. (2010). Merging DEL and ETL. Journal of Logic, Language and Information, 19(4), 413–430.
Klein, D., & Rendsvig, R.K. (2017). Convergence, continuity and recurrence in dynamic epistemic logic. In A. Baltag, & J. Seligman (Eds.) , Logic and rational interaction (LORI VI). Lecture Notes in Computer Science. Berlin: Springer.
Klein, D., & Rendsvig, R.K. (2017). Metrics for formal structures, with an application to dynamic epistemic logic. arXiv:1704.00977.
Kremer, P., & Mints, G. (1997). Dynamical topological logic. Bulleting of Symbolic Logic, 3, 371–372.
Kremer, P., & Mints, G. (2007). Dynamic topological logic. In M. Aiello, I. Pratt-Hartmann, J. van Benthem (Eds.) , Handbook of spatial logics, chapter 10 (pp. 565–606).
Liu, F., Seligman, J., Girard, P. (2014). Logical dynamics of belief change in the community. Synthese, 191(11), 2403–2431.
van der Meyden, R. (1994). Axioms for knowledge and time in distributed systems with perfect recall. In Proceedings ninth annual IEEE symposium on logic in computer science (pp. 448–457).
van der Meyden, R. (1997). Constructing finite state implementations of knowledge-based programs with perfect recall. In Intelligent agent systems theoretical and practical issues (pp. 135–151). Berlin: Springer.
van der Meyden, R., & Wong, K.-S. (2003). Complete axiomatizations for reasoning about knowledge and branching time. Studia Logica, 75(1), 93–123.
Mohalik, S., & Ramanujam, R. (2010). Automata for epistemic temporal logic with synchronous communication. Journal of Logic, Language and Information, 19 (4), 451–484.
Moss, L.S. (2015). Dynamic epistemic logic. In van Ditmarsch, H., J.Y. Halpern, W. van der Hoek, B. Kooi (Eds.) , Handbook of epistemic logic. College Publications.
Osbourne, M.J., & Rubinstein, A. (1994). A course in game theory. Cambridge: The MIT Press.
Parikh, R., & Ramanujam, R. (1985). Distributed processes and the logic of knowledge. In Parikh, R. (Ed.) , Logics of programs (pp. 256–268). Heidelberg: Berlin.
Parikh, R., & Ramanujam, R. (2003). A knowledge based semantics of messages. Journal of Logic, Language and Information, 12(4), 453–467.
Plaza, J.A. (1989). Logics of public communications. In M.L. Emrich, M.S. Pfeifer, M. Hadzikadic, Z.W. Ras (Eds.) , Proceedings of the 4th international symposium on methodologies for intelligent systems (pp. 201–216).
Rendsvig, R.K. (2013). Aggregated beliefs and informational cascades. In D. Grossi, O. Roy, R.K. Rendsvig (Eds.) , Logic, rationality, and interaction. Lecture Notes in Computer Science (pp. 337–341). Berlin: Springer.
Rendsvig, R.K. (2014). Diffusion, influence and best-response dynamics in networks: an action model approach. In R. de Haan (Ed.) , Proceedings of the ESSLLI 2014 student session. arXiv:1708.01477 (pp. 63–75).
Rendsvig, R.K. (2014). Pluralistic ignorance in the bystander effect: informational dynamics of unresponsive witnesses in situations calling for intervention. Synthese, 191(11), 2471–2498.
Rendsvig, R.K. (2015). Model transformers for dynamical systems of dynamic epistemic logic. In W. van der Hoek, W.H. Holliday, W.F. Wang (Eds.) , Logic, rationality, and interaction (LORI 2015, Taipei), LNCS (pp. 316–327). Berlin: Springer.
Rendsvig, R.K. (2018). Logical dynamics and dynamical systems. PhD thesis, Lund University.
Rodenhäuser, B. (2011). A logic for extensional protocols. Journal of Applied Non-Classical Logics, 21(3–4), 477–502.
Sadzik, T. (2006). Exploring the iterated update universe. ILLC Report PP-2006-263, pp. 1–34.
Sarenac, D. (2011). Modal logic for qualitative dynamics. In O. Roy, P. Girard, M. Marion (Eds.) , Dynamic formal epistemology, volume 351 of Synthese Library (pp. 75–101). Berlin: Springer.
Wang, Y. (2010). Epistemic modelling and protocol dynamics. Phd thesis, Universiteit van Amsterdam.
Wooldridge, M., & Lomuscio, A. (1999). Reasoning about visibility, perception, and knowledge. In International workshop on agent theories, architectures and languages (pp. 1–12). Berlin: Springer.
Acknowledgments
The Center for Information and Bubble Studies is funded by the Carlsberg Foundation. The contribution of R.K. Rendsvig to the research reported in this article was also funded by the Swedish Research Council through the framework project ‘Knowledge in a Digital World’ (Erik J. Olsson, PI): A previous version of this paper occurs in the thesis [57]. We thank Alexandru Baltag, Johan van Benthem, Thomas Bolander, Vincent F. Hendricks and Dominik Klein for valuable comments on elements of this paper, as well as the participants of the 2016 CADILLAC and the 2016 LogiCIC workshops, held in Christiania, Denmark, and Amsterdam, the Netherlands, respectively.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Appendix: Proofs
Appendix: Proofs
Proposition 1
Let (X, f, x) be a pointed DEL dynamical system given by multi-pointed action model . Then there exists a singleton uniform DEL protocol that produces the orbit of f from x.
Proof
For each \(k\in \mathbb {N}\), let σk ∈Γ be such that fk(x)⊧pre(σk). As is X-deterministic, for each k there is at most one such σk. Define a uniform DEL protocol p as the smallest protocol for which pk(s) = Σσk (for all s ∈ x) whenever σk exists. Then when p is sequentially applied to x using product update, it produces the sequence \(\langle f^{k}(x)\rangle _{k\in \mathbb {N}}\) of pointed Kripke models (up to the deletion of redundant states not connected to the designated states, cf. Section 2).□
Proposition 2
If saturated ETL model \((\mathcal {H},\underline {H})\) is generated by a pointed DEL dynamical system, then \((\mathcal {H},\underline {H})\) satisfies seven of the eight properties of Section 4.2, namely Synchronicity, Connected Time-Steps, Perfect Recall, Local No Miracles, Precondition Describable, Precondition Describable, and Point Bisimulation Invariance.
Proof
Let (X, f, x) be a pointed DEL dynamical system with orbit \((f^{k}(x))_{k\in \mathbb {N}}\). The length of a state s in fk(x) is len(s) := k + 1.
Let \((\mathcal {H},\underline {H})\) be the saturated ETL model generated by (X, f, x). Given the construction of γ in Def. 6, there exists a family of isomorphisms \(\{g_{k}\}_{k\in \mathbb {N}}\) with each gk mapping [[fk(x)]] to Hk := {h ∈ H : len(h) = k} satisfying g1(s) = es and gk+ 1((s, σ)) = gk(s)eσ. Using this family, it is shown that \((\mathcal {H},\underline {H})\) satisfies the listed properties in order:
- Synchronicity. :
-
Assume for arbitrary h, h′∈ H that hih′. Then by the construction of the generated i (Def. 6), \(\exists k\in \mathbb {N}:g_{k}^{-1}(h)R_{i}g_{k}^{-1}(h^{\prime })\). Hence \(g_{k}^{-1}(h),g_{k}^{-1}(h^{\prime })\in \left [{\kern 3.5pt}[ f^{k}(x)\right ]{\kern 3.5pt}] \). Thus, \(len(g_{k}^{-1}(h))=len(g_{k}^{-1}(h^{\prime }))\). Hence, by the construction of g, len(h) = len(h′).
- Perfect Recall. :
-
Assume for arbitrary he, h′e′∈ H that heih′e′. Then \(\exists k\in \mathbb {N}:g_{k}^{-1}(he)R_{i}g_{k}^{-1}(h^{\prime }e^{\prime })\). By construction of f, for the multi pointed action model. As \(g_{k}^{-1}(he)R_{i}g_{k}^{-1}(h^{\prime }e^{\prime })\), by definition of ⊗ and clean maps, \(g_{k-1}^{-1}(h)R_{i}g_{k-1}^{-1}(h^{\prime })\). Hence, by definition of i, it follows that hih′.
- Local No Miracles. :
-
Assume that 1) hih′, 2) h1eih2e′ and 3) h∗h1 for arbitrary he, h′e′, h1e, h2e′∈ H. 1) implies that 1*) \(g_{k}^{-1}(h)R_{i}g_{k}^{-1}(h^{\prime })\) for k = len(h). 3) implies that len(h) = len(h1) by Synchronicity. In conjunction with 2), this implies that 2*) \(g_{k+1}^{-1}(h_{1}e)R_{i}g_{k+1}^{-1}(h_{2}e^{\prime })\).
By construction of f, . By 2*) and the definition of ⊗ and clean maps, there must be 4) σe, such that \(\sigma _{e}\mathsf {R}_{i}\sigma _{e^{\prime }}\), for σe the σ such that gk+ 1((s, σ)) = h1e, for some s ∈ [[fk(x)]], and \(\sigma _{e^{\prime }}\) the σ′ such that gk+ 1((t, σ′)) = h2e′, for some t ∈ [[fk(x)]].
Now assume that \((g_{k}^{-1}(h),\sigma _{e}),(g_{k}^{-1}(h^{\prime }),\sigma _{e^{\prime }})\in \left [{\kern 3.5pt}[ f^{k+1}(x)\right ]{\kern 3.5pt}] \). Then 1*), 4) and Def. ⊗ jointly imply that \((g_{k+1}^{-1}(h),\sigma _{e})R_{i}(g_{k+1}^{-1}(h^{\prime }),\sigma _{e^{\prime }})\). By the definition of the generated i, it thus follows that heih′e′.
- Connected Time-Steps. :
-
For arbitrary h, h′∈ H assume len(h) = len(h′). Let \(k\in \mathbb {N}\) such that h, h′∈ Hk. Then \(g_{k}^{-1}(h),g_{k}^{-1}(h^{\prime })\in [{\kern 3.5pt}[ f^{k}(x)]{\kern 3.5pt}]\). By definition of product update ⊗, clean maps and the fact that x is connected, \(g_{k}^{-1}(h)R^{*}g_{k}^{-1}(h^{\prime })\). By definition of \((\mathcal {H},\underline {H})\) it follows that h∗h′.
- Precondition Describable. :
-
For arbitrary e ∈ E, let δe = pre(σe). Recall that by definition of ⊗, \(\forall k\in \mathbb {N}\), \((g_{k}^{-1}(h),\sigma _{e})\in [{\kern 3.5pt}[ f^{k+1}(x)]{\kern 3.5pt}]\) iff \(g_{k}^{-1}(h)\models \mathsf {pre}(\sigma _{e})\) and σe ∈Σk+ 1 (∗). Assume ∃h′∈ H : h′e ∈ H and let h ∈ H such that h′∗h.
⇒: Assume for some \(k\in \mathbb {N}\) that (Hk, h)⊧δe. Then \(g_{k}^{-1}(h)\models \mathsf {pre}(\sigma _{e})\). By assumption, σe ∈Σk+ 1. By (∗), thus \((g_{k}^{-1}(h),\sigma _{e})\in [{\kern 3.5pt}[ f^{k+1}(x)]{\kern 3.5pt}]\). Therefore, he ∈ H.
⇐: Assume he ∈ H. Then for some \(k\in \mathbb {N}\), \(g_{k+1}^{-1}(he)=(g_{k}^{-1}(h),\sigma _{e})\in [{\kern 3.5pt}[ f^{k+1}(x)]{\kern 3.5pt}]\). By (∗), \(g_{k}^{-1}(h)\models {{\mathsf {pre}}}(\sigma _{e})\). And thus h⊧δe.
- Precondition Describable. :
-
For arbitrary he ∈ H (in specific for some \(k\in \mathbb {N}\), he ∈ Hk+ 1) let \(\delta _{D_{e}}=\mathsf {post}(\sigma _{e})\) where De = D1 ∪ D2, for p, q ∈Φ such that D1 = {p : h∉V (p), he ∈ V (p)} and D2 = {¬q : h ∈ V (q), he∉V (q)}.
Consider an arbitrary p ∈ D1. Then by definition of the generated ETL model \((\mathcal {H},\underline {H})\), \(g_{k}^{-1}(h)\not \in [{\kern 3.5pt}[ p]{\kern 3.5pt}]_{k}\) and \(g_{k+1}^{-1}(he)\in [{\kern 3.5pt}[ p]{\kern 3.5pt}]_{k+1}\) (∗). By construction, \(g_{k+1}^{-1}(he)=(g_{k}^{-1}(h),\sigma )\) for some σ ∈∇k+ 1 (∗∗). By definitions of \((\mathcal {H},\underline {H})\) and ⊗, \((g_{k}^{-1}(h),\sigma )\in [{\kern 3.5pt}[ p]{\kern 3.5pt}]_{k+1}\) iff post(σ)⊧p. Then, by (∗) and (∗∗), post(σ)⊧p. As p ∈ D1 was arbitrary, post(σ)⊧D1.
The argument for post(σ)⊧D2 is identical. Conclude that post(σ)⊧De and thus \(\delta _{D_{e}}\models D_{e}\).
- Point Bisimulation Invariance. :
-
Let arbitrary \(C(\mathcal {H}h)\underline {h}=(H_{k},\underline {h})\) and \(C(\mathcal {H}h^{\prime })\underline {h^{\prime }}=(H_{l},\underline {h^{\prime }})\) be such that . Hence (∗).
Further, assume for arbitrary h ∈ Hk and h′∈ Hl that .
⇒: Assume he ∈ H. By construction of g and definition of clean maps, both Hk and Hl are connected components, i.e, ∀h, h′∈ Hk : h∗h′ and idem for Hl. By the Hennessy-Milner Theorem (see Section 7), it follows that h and h′ satisfy exactly the same modal formulas. Hence, by construction of g and the definition of \(\mathcal {H}\), \(g_{k}^{-1}(h)\) and \(g_{l}^{-1}(h^{\prime })\) satisfy exactly the same modal formulas as well. Now as he ∈ H, \(g_{k+1}^{-1}(he)\in \left [{\kern 3.5pt}[ f^{k+1}(x)\right ]{\kern 3.5pt}] \) and thus \(g_{k}^{-1}(h)\models \mathsf {pre}(\sigma _{e})\). Hence \(g_{l}^{-1}(h^{\prime })\models \mathsf {pre}(\sigma _{e})\) (∗∗). By (∗) and (∗∗), it follows that \((g_{l}^{-1}(h^{\prime }),\sigma _{e})\in \left [{\kern 3.5pt}[ f^{l+1}(x)\right ]{\kern 3.5pt}] \). Hence h′e ∈ H.
⇐: By the same argument, h′e ∈ H implies he ∈ H.
This concludes the proof of Proposition 2. □
Proposition 3
Not all saturated ETL models generated by DEL dynamical systems are Component Collection Describable.
Proof
Let Ms and f be as in Fig. 7 (cf. [56]) and X be the orbit of f from Ms. Then the ETL model generated by the DEL dynamical system (X, f) from initial model Ms is not Component Collection Describable.
Consider A = {fn(Ms) : n is even}. There does not exist a φ such that for all x ∈ X, x⊧φ iff x ∈ A: Assume the modal depth of φ is k. Let m > k. Then fm(Ms)⊧φ iff fm+ 1(Ms)⊧φ as two such models will not differ in the first m + 1 relational steps from the point. Hence the ETL model generated by (X, f) from Ms is not Component Collection Describable. □
Proposition 4
If \((\mathcal {H},\underline {H})\) is a saturated ETL model that satisfies all eight properties of Section 4.2, then there exists a pointed DEL dynamical system that generates \((\mathcal {H},\underline {H})\).
Proof
Proposition 4 is shown by constructing a DEL dynamical system (X, f) with f the clean map of a X-deterministic multi-pointed action model and an initial Kripke model x ∈ X such that the saturated ETL model \((\mathcal {H}^{\prime },\underline {H}^{\prime })=(E^{\prime },H^{\prime },\mathtt {R}^{\prime },V^{\prime },\underline {H}^{\prime })\) generated by (X, f) from x is ETL isomorphic to \((\mathcal {H},\underline {H})\). The latter is shown by induction on len(h) of \(h\in \mathcal {H}\) for a map γ∗ : E→E′. As in Def. 5, for h = e0...en, write γ∗(h) := γ∗(e0)...γ∗(en).
As \((\mathcal {H},\underline {H})\) satisfies property Connected Time-Steps, the ETL model is a saturated component branch. To emphasize this, in this proof \((\mathcal {H},\underline {H})\) is written \((\mathcal {H}_{\mathbf {b}},\underline {H})\).
- 1.
Initial Kripke model
To obtain a practical and consistent naming of states, the initial Kripke model x = ([[x]], R, [[⋅]], s) is set to be a re-naming of the initial component of b: Let \([{\kern 3.5pt}[ x]{\kern 3.5pt}]=\{\sigma _{e}:e\in \mathbf {b}_{0}\underline {h}\}\). For the relations and valuation of the initial model, simply copy over the relations and valuation from the initial component of b: For all \(i\in \mathcal {A}\), let \(\sigma _{e}R_{i}\sigma _{e^{\prime }}\) iff eie′, and for all p ∈Φ, let σe ∈ [[p]] iff e ∈ V (p). Finally, let the point of x be the copy of the point of \(\mathbf {b}_{0}\underline {h}\): Let \(s=\sigma _{\underline {h}}\).
- 2.
Constructing (X, f)
To define the DEL dynamical system (X, f), first construct a multi-pointed action model . In words, construct so that for each time-step bk of the component branch b, Γ contains a designated action \(\underline {\sigma }_{k}\) connected to a set of actions [[Σk]] ⊆ [[Σ]] such that the single -pointed action model \({\Sigma }^{\prime }{{~}_{\{\underline {\sigma }_{k}\}}}\) obtained from restricting Σ to [[Σk]] produces the equivalent of \(\mathbf {b}_{k+1}\underline {h}\) from the Kripke model-equivalent of \(\mathbf {b}_{k}\underline {h}\). In the precondition of \(\underline {\sigma }_{k}\), include a formula \(\delta _{\mathbf {b}_{k}\underline {h}}\) characterizing \(\mathbf {b}_{k}\underline {h}\). As \((\mathcal {H}_{\mathbf {b}},\underline {H})\) is Component Collection Describable by assumption, such a formula exists.
Formally, construct piece-wise as follows: Let \(\mathbf {b}_{k}\underline {h}\) and \(\mathbf {b}_{k+1}\underline {h}\) be given. Σk+ 1σ is constructed such that C(fk(x) ⊗Σkσ)s′ mirrors the structure of \(\mathbf {b}_{k+1}\underline {h}\):
Let the single-pointed action model \({\Sigma }_{k+1}\underline {\sigma }_{k+1}\) be ([[Σk+ 1]], Rk+ 1, prek+ 1, \(\mathsf {post}_{k+1},\underline {\sigma }_{k+1})\), given by
with δe and \(\delta _{\mathbf {b}_{k}\underline {h}}\) given by Precondition Describable and Component Collection Describable, respectively.
- \(\mathsf {post}(\sigma _{e})=\delta _{D_{e}}\) :
-
as given Postcondition Describable.
Let the multi-pointed action model be given by, for , and \({\Gamma }={\bigcup _{k:\mathbf {b}_{k}\in \mathbf {b}}\{\underline {\sigma }_{k}\}}\). This is well-defined: For pre and post, this follows from Precondition Describable and Postcondition Describable.
Let X be the closure of {x} under the operation . On X, is guaranteed to be deterministic as any two characteristic formulas \(\delta _{\mathbf {b}_{k}\underline {h}}\) and \(\delta ^{\prime }_{\mathbf {b}_{k^{\prime }}\underline {h^{\prime }}}\) are not simultaneously satisfiable. Finally, let f be the clean map of on X. Then (X, f) is a DEL dynamical system with x ∈ X.
- 3.
Constructing the Isomorphism
Let \((\mathcal {H}^{\prime },\underline {H}^{\prime })=(E^{\prime },H^{\prime },\mathtt {R}^{\prime },V^{\prime },\underline {H}^{\prime })\) be the saturated ETL model generated by (X, f) from x. Define the two mappings: γ‡ : E→[[Σ]] with γ‡(e) = σe and γ : [[Σ]]→E′ for γ(σ) = eσ cf. Def. 6. From these, define γ∗ : E→E′ as γ∗ := γ ∘ γ‡.
Define subsets of E based on history length: For all \(k\in \mathbb {N}\) let E0 = {e : e ∈b0} and Ek+ 1 ≥ 1 = {e : h ∈bk, he ∈bk+ 1}⊆ E. Let \(E^{\prime }_{k},k\in \mathbb {N},\) be given mutatis mutandis. Let \(\gamma _{k}^{\dagger }:E_{k}\longrightarrow [{\kern 3.5pt}[{\Sigma }_{k}]{\kern 3.5pt}]\), \(\gamma _{k}:[{\kern 3.5pt}[{\Sigma }_{k}]{\kern 3.5pt}]\longrightarrow E_{k}^{\prime }\) and \(\gamma _{k}^{*}:E_{k}\longrightarrow E_{k}^{\prime }\) be the restrictions of γ‡, γ and γ∗ to Ek × [[Σk]], \([{\kern 3.5pt}[{\Sigma }_{k}]{\kern 3.5pt}]\times E^{\prime }_{k}\) and \(E_{k}\times E^{\prime }_{k}\), respectively. Then, of course, \(\gamma ^{*}=\bigcup _{k\in \mathbb {N}}\gamma _{k}^{*}\), whereby \(\gamma ^{*}(e)=e^{\prime }_{\sigma _{e}}\). By induction on len(h), \(h\in \mathcal {H}\), it is now shown that γ∗ is an ETL isomorphism.
Claim: The mapγ∗is a bijection. By the construction of γ‡ and γ, each \(\gamma _{k}^{*}\) is an injection: if e ≠ e′, then \(\gamma _{k}^{*}(e)\neq \gamma _{k}^{*}(e^{\prime })\). By construction, it is also guaranteed that \(\gamma _{k}^{*}\) is a surjection: \(\forall e^{\prime }\in E^{\prime }\exists e\in E:\gamma _{k}^{*}(e)=e^{\prime }\). Hence for each \(k\in \mathbb {N}\), \(\gamma _{k}^{*}\) is a bijection.
Furthermore, γ∗ is a total map: if e ∈ Ek ∩ Em, then \(\gamma _{k}^{\dagger }(e)=\gamma _{m}^{\dagger }(e)\) (i.e., σe ∈ [[Σk]] ∩ [[Σm]]) and γk(σe) = γm(σe). Thus γ ∘ γ‡(e) is well-defined and in \(E_{k}^{\prime }\cap E_{m}^{\prime }\).
Finally, γ∗ inherits injectivity and surjectivity from its restrictions. Hence, the map γ∗ is a bijection.
Claim: The mapγ∗is an ETL isomorphism. The claim is shown by 4 inductive sub-proofs.
- 1)
Domain and Temporal Structure.
Base. Let h ∈ H0. This is the case iff γ‡(h) ∈ f0(x) (by construction of initial Kripke model) iff \(\gamma \circ \gamma ^{\dagger }(h)\in H^{\prime }_{0}\) (by Def. 6).
Step. It is shown that he ∈ Hk+ 1 iff \(\gamma ^{*}(he)\in H^{\prime }_{k+1}\).
⇒: Assume he ∈ Hk+ 1. Then h ∈ Hk. By the induction hypothesis, γ‡(h) ∈ [[fk(x)]]. By construction of Σk+ 1, γ‡(e) ∈ [[Σk+ 1]]. By the same construction and Precondition Describable, γ‡(h)⊧pre(σe). Hence (γ‡(h), γ‡(e)) ∈ [[fk+ 1(x)]]. By Def. 6, in particular the construction of Hk+ 1, \(\gamma ((\gamma ^{\dagger }(h),\gamma ^{\dagger }(e)))\in H^{\prime }_{k+1}\).
⇐: Assume \(\gamma ((\gamma ^{\dagger }(h),\gamma ^{\dagger }(e)))\in H^{\prime }_{k+1}\). Then (γ‡(h), γ‡(e)) ∈ [[fk+ 1(x)]] by Def. 6, so γ‡(h) ∈ [[fk(x)]] and γ‡(e) ∈ [[Σk+ 1]]. By the induction hypothesis, h ∈ Hk. If he∉Hk+ 1, a contradiction is reached: pre(γ‡(e)) is satisfied by exactly those γ‡(h) ∈ [[fk(x)]] such that (γ‡(h), γ‡(e)) ∈ [[fk+ 1(x)]] – by the construction of action models in this proof and as \((\mathcal {H}_{\mathbf {b}},\underline {H})\) is Precondition Describable. So he ∈ Hk+ 1.
- 2)
Epistemic relations.
Base. It follows by construction of initial Kripke model and Def. 6.
Step. It is shown that ∀he, h′e′∈bk+ 1, heih′e′ iff \(\gamma ^{*}(he)\mathtt {R}^{\prime }_{i}\gamma ^{*}(h^{\prime }e^{\prime })\).
⇒: Assume that heih′e′. By Perfect Recall, hih′. By the induction hypothesis, γ‡(h)Riγ‡(h′). By construction of Σk+ 1, γ‡(e)Riγ‡(e′). By definition of ⊗, (γ‡(h), γ‡(e))Ri(γ‡(h′), γ‡(e′)). By Def. 6, γ((γ‡(h), γ‡(e)))iγ((γ‡(h′), γ‡(e′))).
⇐: Assume γ((γ‡(h), γ‡(e)))iγ((γ‡(h′), γ‡(e′))). By Def. 6, (γ‡(h), γ‡(e))Ri(γ‡(h′), γ‡(e′)). By definition of ⊗, both γ‡(h)Riγ‡(h′) and γ‡(e)Riγ‡(e′). So by construction of Σk+ 1, ∃h1e, h2e′∈bk+ 1 : h1eih2e′. By the induction hypothesis, hih′. Further, note that ∀h, h′∈bk : h∗h′. Hence, by Local No Miracles, heih′, e′.
- 3)
Valuation.
Base. It follows by construction of initial Kripke model and Def. 6.
Step. It is shown that ∀he ∈bk+ 1, he ∈ V (p) iff γ(he) ∈ V′(p).
⇒: Assume he ∈ V (p) . Either i) h ∈ V (p) or ii) h∉V (p). If i), then by the induction hypothesis, γ ∘ γ‡(h) ∈ V′(p). By construction of Σk+ 1, post(γ‡(e))⊮¬p. Hence (γ‡(h), γ‡(e)) ∈ [[p]]k+ 1. By Def. 6, γ((γ‡(h), γ‡(e))) ∈ V′(p). If ii), then by the induction hypothesis, γ‡(h)∉ [[p]]k. As \((\mathcal {H}_{\mathbf {b}},\underline {H})\) is Postcondition Describable, by construction of Σk+ 1, post(γ‡(e))⊧p. Thus (γ‡(h), γ‡(e)) ∈ [[p]]k+ 1. By Def. 6, γ((γ‡(h), γ‡(e))) ∈ V′(p).
⇐: Assume γ((γ‡(h), γ‡(e))) ∈ V′(p). Then (γ‡(h), γ‡(e)) ∈ [[p]]k+ 1 by Def. 6. Again, either i) γ‡(h) ∈ [[p]]k or ii) γ‡(h)∉ [[p]]k. If i), then by the induction hypothesis, h ∈ V (p). For a contradiction, suppose he∉V (p). Then post(γ‡(e))⊧¬p. But by construction of Σk+ 1, post(γ‡(e))⊮¬p. This is a contradiction. Hence he ∈ V (p). If ii), then by the definition of ⊗, post(γ‡(e))⊧p. By the induction hypothesis, h∉V (p). If it was the case that he∉V (p), then post(γ‡(e))⊮p. Contradiction. Thus he ∈ V (p).
- 4)
Points.
Base. It follows by construction of initial Kripke model and Def. 6.
Step. It is shown that \(\underline {he}\in \underline {H}_{k+1}\) iff \(\gamma ^{*}(\underline {he})\in \underline {H}_{k+1}^{\prime }\). Let fk(x) = Nt and fk+ 1(x) = Ms.
⇒: Assume \(\underline {he}\in \underline {H}_{k+1}\). By the induction hypothesis, \(\gamma ^{\dagger }(\underline {h})=t\). By saturation of bk, \(\exists e\in E:\underline {h}e\in \mathbf {b}_{k+1}\cap \underline {H}\). By construction of Σk+ 1, γ‡(e) ∈ [[Σk+ 1]] and, as \((\mathcal {H}_{\mathbf {b}},\underline {H})\) is Precondition Describable, \(\gamma ^{\dagger }(\underline {h})\models \mathsf {pre}(\gamma ^{\dagger }(e))\). By construction of f, fk+ 1(x) = C(Nt ⊗ (Σk+ 1, γ‡(e))) = C(N ⊗Σk+ 1, (t, γ‡(e))) = Ms. By Def. 6, \(\gamma (s)=\gamma (\gamma ^{\dagger }(\underline {he}))\in \underline {H}^{\prime }_{k+1}\).
⇐: Assume \(\gamma (\gamma ^{\dagger }(\underline {he}))\in \underline {H}^{\prime }_{k+1}\). By Def. 6, \(f^{k+1}(x)=(C(N\otimes {\Sigma }_{k+1}),(t,\gamma ^{\dagger }(\underline {e})))\). By induction hypothesis, \(\gamma ^{\dagger -1}(t)=h\in \underline {H}_{k}\). By construction of the Action Model, \(\gamma ^{\dagger }(\underline {e})=\gamma ^{-1}(e)\) for e such that \(\exists h^{\prime }:h^{\prime }e\in \underline {H}_{k+1}\) and \(h^{\prime }\in \underline {H}_{k}\). As points in Hm are unique for all m by Def. 7, h′ must be h. Thus \(he\in \underline {H}_{k+1}\).
This concludes the proof of Proposition 4.Footnote 1□
Lemma 1
If there exists an image-finite and concluding pointed DEL dynamical system that generates \((\mathcal {H},\underline {H})\), then \((\mathcal {H},\underline {H})\) is image-finite and concluding.
Proof
As the DEL dynamical system is image-finite, for all \(k\in \mathbb {N}\) with fk(x) = Ms, Ri is image-finite (for all i ∈ I). The construction of the generated ETL model (see Definition 6) ensures that for all Hk, i is image-finite (for all i ∈ I,). Hence \((\mathcal {H},\underline {H})\) is image-finite.
If the DEL dynamical system terminates, then there is a \(k\in \mathbb {N}\) such that fk(x) is undefined. Let fk− 1(x) = Ms and \(\gamma (s)=\underline {h}\). As fk(x) is undefined, there is no σ such that γ(s)γ(σ) ∈ H. Hence, there is no e such that \(\underline {h}e\in H\). Note that by construction of \(\underline {{\underline {H}}}\), for all \(\underline {h}^{\prime }\in \underline {H}\): \(\underline {h}^{\prime }\sqsubseteq \underline {h}\). Thus, all \(\underline {h}^{\prime }\in \underline {H}\) are finite and hence \((\mathcal {H},\underline {H})\) concludes.
If the DEL dynamical system is periodic, fk(x) = fk+m(x) for some k ≥ 0 and m > 0. Let fk(x) = Ms and fk+m(x) = M′s′, and let \(\gamma (s)=\underline {h}\) and \(\gamma (s^{\prime })=\underline {h}^{\prime }\). By construction, \(\underline {h}\sqsubseteq \underline {h}^{\prime }\). From Ms = M′s′ it follows that . Thus, all \(\underline {h}^{\prime \prime }\in \underline {H}\) such that \(\underline {h}^{\prime \prime }\sqsubseteq \underline {h}\) are repeating. Furthermore, note that for all \(n\in \mathbb {N}\), fk+n(x) = fk+m+n(x). Now for arbitrary \(n\in \mathbb {N}\), let fk+n(x) = Mnsn and fk+m+n(x) = Mn′sn′, and let \(\gamma (s^{n})=\underline {h}^{n}\) and \(\gamma (s^{n\prime })=\underline {h}^{n\prime }\). By same argument as above, \(\underline {h}^{n}\) is repeating. As n is arbitrary, all \(\underline {h}^{\prime \prime }\in \underline {H}\) such that \(\underline {h}^{\prime \prime }\sqsupseteq \underline {h}\) are repeating. Thus, all \(\underline {h}^{\prime \prime }\in \underline {H}\) are repeating and hence \((\mathcal {H},\underline {H})\) concludes. □
Lemma 2
If a saturated ETL model \((\mathcal {H},\underline {H})\) is image-finite, concluding and satisfies Connected Time-Steps, then \((\mathcal {H},\underline {H})\) is Component Collection Describable.
Proof
Let \((\mathcal {H},\underline {H})\) be an image-finite and concluding saturated ETL model. Set \(\mathcal {B}:=\{C(\mathcal {H}h):h\in \underline {H}\}\), the set of all connected components in \((\mathcal {H},\underline {H})\). As all \(C(\mathcal {H}h)\in \mathcal {B}\) are image-finite, by the Hennessy-Milner Theorem (see Section 7), for each pair \(\underline {h}_{1},\underline {h}_{2}\in \underline {H}\) if , there exists a formula \(\varphi _{\underline {h}_{1},\underline {h}_{2}}\) distinguishing between \(\underline {h}_{1}\) and \(\underline {h}_{2}\): \(\underline {h}_{1}\models \varphi _{\underline {h}_{1},\underline {h}_{2}}\) while \(\underline {h}_{2}\not \models \varphi _{\underline {h}_{1},\underline {h}_{2}}\).
Let be the equivalence class . Then, since \((\mathcal {H},\underline {H})\) is concluding, the set is finite. Therefore, the conjunction is well-defined for any \(\underline {h}_{1}\in \underline {H}\). This conjunction distinguishes \(\underline {h}_{1}\) from any point in \(\underline {H}\) that is not bisimilar to \(\underline {h}_{1}\). Denote this formula \(\varphi _{\underline {h}{}_{1}}\).
Moreover, as is finite, all sets \(A\subseteq \underline {H}\) for which \(\underline {h}\in A\) and implies \(\underline {h}^{\prime }\in A\) are finite. Hence, for any such A, the disjunction \(\bigvee _{\underline {h}_{1}\in A}\varphi _{\underline {h}{}_{1}}\) is well-defined. This disjunction distinguishes the connected components in A from those not in A. □
Lemma 3
Let {(Xj, fj)}j ∈ J be minimal in generating \(\mathcal {H}\) and let (Xj, fj, xj) generate the saturated ETL model \((\mathcal {H}_{j},\underline {H}_{j})\). Then \((\mathcal {H}_{j},\underline {H}_{j})\) is the component branch sub-model for some saturated component branch \((\mathbf {b},\underline {H})\) of \(\mathcal {H}\).
Proof
Let \(\mathcal {H}=(E,H,\mathtt {R},V)\) be generated by {(Xj, fj)}j ∈ J. Let bj be the sequence of connected components \(\mathbf {b}_{j,k}=C(\mathcal {H},h)\) for all \(h_{k}\in \underline {H}_{j}\), ordered on history length k. Suppose for proof by contradiction that bj is both non-maximal and finite (cf. Def. 7). As bj is finite, there is a \(k\in \mathbb {N}\) such that for all h ∈bj, k there is no e ∈ E such that he ∈bj, k+ 1. However, as bj is non-maximal, there is a h ∈bj, k and some e ∈ E such that \(\underline {h}e\in H\). This implies that there is an ETL model \((\mathcal {H}_{j^{\prime }},\underline {H}_{j^{\prime }})\) that extends \((\mathcal {H}_{j},\underline {H}_{j})\). Hence there is a DEL dynamical system \((X_{j^{\prime }},f_{j^{\prime }})\), j′∈ J, such that \({f_{j}^{n}}(x_{j})=f_{j^{\prime }}^{n}(x_{j})\) for all n ≤ k − 1. Hence, (Xk, fk) is redundant in generating \(\mathcal {H}\), contradicting the assumption that {(Xj, fj)}j ∈ J is minimal. Thus, \((\mathbf {b}_{j},\underline {H}_{j})\) is a saturated component branch that gives \((\mathcal {H}_{j},\underline {H}_{j})\). □
Theorem 2
Let an image-finite and concluding ETL model \(\mathcal {H}\) be given. \(\mathcal {H}\) is generatable up to ETL isomorphism by a family of image-finite and concluding pointed DEL dynamical systems, if, and only if, there exists a saturation of each component branch b of \(\mathcal {H}\) such that \((\mathcal {H}_{\mathbf {b}},\underline {H})\) satisfies all eight properties of Section 4.2.
Proof
Left-to-right: Suppose \(\mathcal {H}\) is generatable by a family of image-finite and concluding DEL dynamical systems {(Xj, fj)}j ∈ J. Let \((\mathcal {H}_{j},\underline {H}_{j})\) be the saturated ETL model generated by (Xj, fj) (cf. Def. 6). By Lemma 3, \((\mathcal {H}_{j},\underline {H}_{j})\) is a component branch sub-model of \(\mathcal {H}\) for some saturated component branch \((\mathbf {b},\underline {H}_{k})\) of \(\mathcal {H}\). As \((\mathcal {H}_{j},\underline {H}_{j})\) was generated by an image-finite and concluding DEL dynamical system, the saturation \(\underline {H}_{j}\) of \(\mathcal {H}_{j}\) makes \((\mathcal {H}_{j},\underline {H}_{j})\) satisfy all 8 properties of Section 4.2 by Proposition 2 and Lemma 2.
Right-to-left: Let B be the set of all component branches of \(\mathcal {H}\) and assume that for each b ∈ B, there exists a saturation such that \((\mathcal {H}_{\mathbf {b}},\underline {H}_{\mathbf {b}})\) satisfies all eight properties of Section 4.2. As \(\mathcal {H}\) is image-finite and concluding, also each \((\mathcal {H}_{\mathbf {b}},\underline {H}_{\mathbf {b}})\) is image-finite and concluding. By the constructions in the proof of Prop. 4, it follows that each \((\mathcal {H}_{\mathbf {b}},\underline {H}_{\mathbf {b}})\) is generatable up to ETL isomorphism by a DEL dynamical system that is image-finite and concluding.
Let (Xb, fb, xb) be the pointed DEL dynamical system that generates \((\mathcal {H}_{\mathbf {b}},\underline {H}_{\mathbf {b}})\) up to isomorphism, as given by the construction in the proof of Prop. 4. Let \((\mathcal {H}^{\prime }_{\mathbf {b}},\underline {H}^{\prime }_{\mathbf {b}})\) be the specific ETL model generated by (Xb, fb, xb), as given by Def. 6. It will now be shown that the union structure UB = (EB, HB, B, i, VB)i ∈ I of \(\{(\mathcal {H}^{\prime }_{\mathbf {b}},\underline {H}^{\prime }_{\mathbf {b}})\}_{\mathbf {b}\in \mathbf {B}}\) is isomorphic to \(\mathcal {H}=(E,H,\mathtt {R}_{i},V)_{i\in I}\). To this end, the existence of a bijection g : H→HB will be shown.
Let gb be the isomorphism between \((\mathcal {H}_{\mathbf {b}},\underline {H}_{\mathbf {b}})\) and \((\mathcal {H}^{\prime }_{\mathbf {b}},\underline {H}^{\prime }_{\mathbf {b}})\), guaranteed to exist by Prop. 4 and specifically given by 1) the construction of a DEL dynamical system from a saturated component branch of the proof of Prop. 4 and 2) the construction for generating an ETL model from a DEL dynamical system of Def. 6. Combining the state-history naming schemes used in these two constructions yield gb given by
The history names from \(\mathcal {H}_{\mathbf {b}}\) are hereby carried over as indices to the histories of \(\mathcal {H}^{\prime }_{\mathbf {b}}\).
Define the mapping g : H→HB by g(h) = gb(h) for \(h\in \mathcal {H}_{\mathbf {b}}\). This mapping is well-defined as either i) for exactly one b ∈B, \(h\in \mathcal {H}_{\mathbf {b}}\) (in which case g(h) is well-defined), or ii) if \(h\in \mathcal {H}_{\mathbf {b}}\) and \(h\in \mathcal {H}_{\mathbf {b^{\prime }}}\), then \(g_{\mathbf {b}}(h)=g_{\mathbf {b}^{\prime }}(h)\). The latter is ensured as history names are carried over in exactly the same way by gb and \(g_{\mathbf {b}^{\prime }}\), by construction. Hence \(g=\bigcup _{\mathbf {b}\in \mathbf {B}}g_{\mathbf {b}}\) is a well-defined map. It is an injection: For h ∈ H and h′∈ H, if h ≠ h′, then g(h)≠g(h′) by the unique naming convention of the maps gb, b ∈B. It is also a surjection: it is well-defined and |H| = |HB| as by construction \(|H^{\prime }_{\mathbf {b}}|=|H{}_{\mathbf {b}}|\) for all b ∈B, and \(H=\bigcup _{\mathbf {b}\in \mathbf {B}}H{}_{\mathbf {b}}\) and \(H_{\mathbf {B}}=\bigcup _{\mathbf {b}\in \mathbf {B}}H^{\prime }_{\mathbf {b}}\). Hence g is a bijection.
That g is also the sought ETL isomorphism follows as \((\mathcal {H}_{\mathbf {b}},\underline {H}_{\mathbf {b}})\) is isomorphic to \((\mathcal {H}^{\prime }_{\mathbf {b}},\underline {H}^{\prime }_{\mathbf {b}})\), for all b ∈B, cf. Prop. 4. This completes the proof. □
Lemma 4
The saturated ETL model properties Synchronicity, Perfect Recall and Postcondition Describable persist under ETL model union.
I.e.: Let \(\{(\mathcal {H}_{j},\underline {H}_{j})\}_{j\in J}\) be a countable set of saturated ETL models. If all \((\mathcal {H}_{j},\underline {H}_{j})\) satisfy either of the mentioned properties, then the (unsaturated) union structure UJ satisfies that property.
Proof
Synchronicity, Perfect Recall and Postcondition Describable persist because they are defined on histories which occur uniquely in the ETL forest, which makes them local by nature. Hence these properties are evaluated locally within a branch to ensure that there will be no conflicts when taking the union of different ETL sub-models.□□
Property 5
Local No Miracles, Precondition Describable, Point Bisimulation Invariance and Connected Time-Steps do not persist under union.
Proof
Local No Miracles does not persist under union: Consider a family of two DEL dynamical systems (that each individually satisfy property Local No Miracles.) with multi-pointed action models f and g with equal initial Kripke model x = {h, h′, h1, h2} where hih′ and h∗h1 (by default, as initial models are connected), but disjoint Kripke models at the next level: f1(x) = {he, h′e′} and g1(x) = {h1e, h2e′} where h1eih2e′ while not heih′e′. In this example, Local No Miracles fails because not he∗h1e.
Precondition Describable does not persist under union: Consider a family of two DEL dynamical systems (that each individually satisfy property Precondition Describable) with multi-pointed action models f and g with equal initial Kripke model x = {h, h′} with h∗h′ (by default as initial models are connected), but disjoint Kripke models at the next level: f1(x) = {he} and g1(x) = {h′e}. Then it is possible that h′⊧δe while h⊮δe, which breaks property Precondition Describable. It is left as an open question whether a suitably weakened version of Precondition Describable exists.
That Point Bisimulation Invariance is not preserved under union follows as the property is stated based on a saturation, but the union structure is unpointed, and hence unsaturated. If the union structure would be pointed with the set of points chosen as the union of the sets of points from the united ETL models, then the resulting set of points need not be a saturation, as the united ETL models may overlap, but have distinct points. In that case, the union structure would be “oversaturated”.
Connected Time-Steps does not persist under union as histories within the same time-step are no longer necessarily epistemically connected in a union of disconnected ETL sub-models. □
Proposition 5
If an ETL model \(\mathcal {H}\) is generated by a family of pointed DEL dynamical systems (possibly neither image-finite nor concluding), then \(\mathcal {H}\) satisfies Synchronicity, Perfect Recall, Postcondition Describable and Very Local No Miracles and Local Bisimulation Invariance.
Proof
That \(\mathcal {H}\) satisfies Synchronicity, Perfect Recall and Postcondition Describable follows from Prop. 2 and Lemma 4.
That \(\mathcal {H}\) satisfies Very Local No Miracles follows directly by the additional requirement compared to Local No Miracles that he∗h1e.
That \(\mathcal {H}\) satisfies Local Bisimulation Invariance follows as 1) any ETL model that satisfies Point Bisimulation Invariance also satisfies Local Bisimulation Invariance, 2) Local Bisimulation Invariance is a property local to a connected component, and 3) connected components remain untouched under union.□
Rights and permissions
About this article
Cite this article
van Lee, H.S., Rendsvig, R.K. & van Wijk, S. Intensional Protocols for Dynamic Epistemic Logic. J Philos Logic 48, 1077–1118 (2019). https://doi.org/10.1007/s10992-019-09508-w
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-019-09508-w