Convergence, continuity, recurrence and Turing completeness in dynamic epistemic logic1

2020 ◽  
Vol 30 (6) ◽  
pp. 1213-1238
Author(s):  
Dominik Klein ◽  
Rasmus K Rendsvig
Keyword(s):  
Epistemic Logic ◽  
Dynamic Epistemic Logic ◽  
Model Transformations ◽  
Continuous Mappings ◽  
Turing Completeness ◽  
Action Model ◽  
Free Case ◽  
Finite Action ◽  
Action Models ◽  
Turing Complete

Abstract The paper analyses dynamic epistemic logic from a topological perspective. The main contribution consists of a framework in which dynamic epistemic logic satisfies the requirements for being a topological dynamical system thus interfacing discrete dynamic logics with continuous mappings of dynamical systems. The setting is based on a notion of logical convergence, demonstratively equivalent with convergence in Stone topology. Presented is a flexible, parametrized family of metrics inducing the Stone topology, used as an analytical aid. We show maps induced by action model transformations continuous with respect to the Stone topology and present results on the recurrent behaviour of said maps. Among the recurrence results, we show maps induced by finite action models may have uncountably many recurrent points, even when initiated on a finite input model. Several recurrence results draws on the class of action models being Turing complete, for which the paper provides proof in the postcondition-free case. As upper bounds, it is shown that either 1 atom, 3 agents and preconditions of modal depth 18 or 1 atom, 7 agents and preconditions of modal depth 3 suffice for Turing completeness.

scholarly journals ARROW UPDATE LOGIC

2011 ◽  
Vol 4 (4) ◽  
pp. 536-559 ◽  
Author(s):  
BARTELD KOOI ◽  
BRYAN RENNE
Keyword(s):  
Epistemic Logic ◽  
Belief Change ◽  
Common Knowledge ◽  
Dynamic Epistemic Logic ◽  
Epistemic Access ◽  
Multi Agent ◽  
Logic Approach ◽  
Action Models ◽  
Information Change ◽  
Update Logic

We presentArrow Update Logic, a theory of epistemic access elimination that can be used to reason about multi-agent belief change. While the belief-changing “arrow updates” of Arrow Update Logic can be transformed into equivalent belief-changing “action models” from the popular Dynamic Epistemic Logic approach, we prove that arrow updates are sometimes exponentially more succinct than action models. Further, since many examples of belief change are naturally thought of from Arrow Update Logic’s perspective of eliminating access to epistemic possibilities, Arrow Update Logic is a valuable addition to the repertoire of logics of information change. In addition to proving basic results about Arrow Update Logic, we introduce a new notion of common knowledge that generalizes both ordinary common knowledge and the “relativized” common knowledge familiar from the Dynamic Epistemic Logic literature.

Program models and semi-public environments

2016 ◽  
Vol 29 (7) ◽  
pp. 1071-1097
Author(s):  
Davide Grossi ◽  
Wiebe van der Hoek ◽  
Christos Moyzes ◽  
Michael Wooldridge
Keyword(s):  
Epistemic Logic ◽  
Dynamic Epistemic Logic ◽  
Semantic Model ◽  
The World ◽  
Semantic Models ◽  
Action Models

Abstract We develop a logic for reasoning about semi-public environments , i.e. environments in which a process is executing, and where agents in the environment have partial and potentially different views of the process. Previous work on this problem illustrated that it was problematic to obtain both an adequate semantic model and a language for reasoning about semi-public environments. We here use program models for representing the changes that occur during the execution of a program. These models serve both as syntactic objects and as semantic models, and are a modification of action models in Dynamic Epistemic Logic, in the sense that they allow for ontic change (i.e. change in the world or state). We show how program models can elegantly capture a notion of observation of the environment. The use of these models resolves several difficulties identified in earlier work, and admit a much simpler treatment than was possible in previous work on semi-public environments.

scholarly journals Dynamic Epistemic Logic with Assignments, Concurrency and Communication Actions

2020 ◽  
Author(s):  
Mario Folhadela Benevides ◽  
Isaque Macalam Saab Lima
Keyword(s):  
Epistemic Logic ◽  
Reduction Method ◽  
Dynamic Epistemic Logic ◽  
Epistemic Action ◽  
Action Logic ◽  
Action Models

This work proposes an extension of Dynamic Epistemic Logic with Communication Actions by adding the notion of postconditions from Dynamic Epistemic Logic with Assigments to deal with boolean assignments to action models. Other concurrent logics, like Concurrent Epistemic Action Logic introduced by Ditmarsch, Hoek and Kooi, do not deal with boolean assignments. We present an axiomatization and show that the proof of soundness, completeness and decidability can be done using a reduction method.

scholarly journals Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic

2020 ◽  
Vol 10 (18) ◽  
pp. 6577
Author(s):  
Xiaojuan Chen ◽  
Huiwen Deng
Keyword(s):  
Epistemic Logic ◽  
Formal Language ◽  
Formal Method ◽  
Cryptographic Protocols ◽  
Dynamic Epistemic Logic ◽  
Security Requirements ◽  
Challenging Research ◽  
Research Task ◽  
Action Model ◽  
Efficient Verification

The security of cryptographic protocols has always been an important issue. Although there are various verification schemes of protocols in the literature, efficiently and accurately verifying cryptographic protocols is still a challenging research task. In this work, we develop a formal method based on dynamic epistemic logic to analyze and describe cryptographic protocols. In particular, we adopt the action model to depict the execution process of the protocol. To verify the security, the intruder’s actions are analyzed. We model exactly the protocol applying our formal language and give the verification models according to the security requirements of this cryptographic protocol. With analysis and proof on a selected example, we show the usefulness of our method. The result indicates that the selected protocol meets the security requirements.

scholarly journals Reachability Games in Dynamic Epistemic Logic

2019 ◽  
Author(s):  
Bastien Maubert ◽  
Sophie Pinchinat ◽  
François Schwarzentruber
Keyword(s):  
Epistemic Logic ◽  
Imperfect Information ◽  
Dynamic Epistemic Logic ◽  
Perfect Information ◽  
Planning Problem ◽  
Multiplayer Games ◽  
Public Announcements ◽  
Action Models

We define reachability games based on Dynamic Epistemic Logic (DEL), where the players? actions are finely described as DEL action models. We first consider the setting where a controller with perfect information interacts with an environment and aims at reaching some desired state of knowledge regarding the observers of the system. We study the problem of existence of a strategy for the controller, which generalises the classic epistemic planning problem, and we solve it for several types of actions such as public announcements and public actions. We then consider a yet richer setting where observers themselves are players, whose strategies must be based on their observations. We establish several decidability and undecidability results for the problem of existence of a distributed strategy, depending on the type of actions the players can use, and relate them to results from the literature on multiplayer games with imperfect information.

scholarly journals Concurrent Games in Dynamic Epistemic Logic

2020 ◽  
Author(s):  
Bastien Maubert ◽  
Sophie Pinchinat ◽  
Francois Schwarzentruber ◽  
Silvia Stranieri
Keyword(s):  
Epistemic Logic ◽  
Dynamic Epistemic Logic ◽  
Infinite Game ◽  
Action Models ◽  
Individual Actions

Action models of Dynamic Epistemic Logic (DEL) represent precisely how actions are perceived by agents. DEL has recently been used to define infinite multi-player games, and it was shown that they can be solved in some cases. However, the dynamics being defined by the classic DEL update product for individual actions, only turn-based games have been considered so far. In this work we define a concurrent DEL product, propose a mechanism to resolve conflicts between actions, and define concurrent DEL games. As in the turn-based case, the obtained concurrent infinite game arenas can be finitely represented when all actions are public, or all are propositional. Thus we identify cases where the strategic epistemic logic ATL*K can be model checked on such games.

Topo-Logic as a Dynamic-Epistemic Logic

2017 ◽  
pp. 330-346 ◽  
Author(s):  
Alexandru Baltag ◽  
Aybüke Özgün ◽  
Ana Lucia Vargas Sandoval
Keyword(s):  
Epistemic Logic ◽  
Dynamic Epistemic Logic

scholarly journals Parallel communicating grammar systems with context-free components are Turing complete for any communication model

2016 ◽  
Vol 8 (2) ◽  
pp. 113-170
Author(s):  
Mary Sarah Ruth Wilkin ◽  
Stefan D. Bruda
Keyword(s):  
Concurrent Systems ◽  
Communication Model ◽  
Broadcast Communication ◽  
Turing Completeness ◽  
One Step ◽  
Grammar Systems ◽  
Turing Complete ◽  
Context Free ◽  
Original Construction ◽  
Parallel Communicating Grammar Systems

Abstract Parallel Communicating Grammar Systems (PCGS) were introduced as a language-theoretic treatment of concurrent systems. A PCGS extends the concept of a grammar to a structure that consists of several grammars working in parallel, communicating with each other, and so contributing to the generation of strings. PCGS are usually more powerful than a single grammar of the same type; PCGS with context-free components (CF-PCGS) in particular were shown to be Turing complete. However, this result only holds when a specific type of communication (which we call broadcast communication, as opposed to one-step communication) is used. We expand the original construction that showed Turing completeness so that broadcast communication is eliminated at the expense of introducing a significant number of additional, helper component grammars. We thus show that CF-PCGS with one-step communication are also Turing complete. We introduce in the process several techniques that may be usable in other constructions and may be capable of removing broadcast communication in general.

scholarly journals The Dynamic Epistemic Logic for Actual Knowledge

2020 ◽  
Vol 49 (1) ◽  
Author(s):  
Arkadiusz Wójcik
Keyword(s):  
Epistemic Logic ◽  
Dynamic Epistemic Logic ◽  
Logical Omniscience ◽  
Actual Knowledge ◽  
Knowledge Change ◽  
The Past ◽  
Knowledge Models ◽  
Complete Axiomatization ◽  
New Information

The dynamic epistemic logic for actual knowledge models the phenomenon of actual knowledge change when new information is received. In contrast to the systems of dynamic epistemic logic which have been discussed in the past literature, our system is not burdened with the problem of logical omniscience, that is, an idealized assumption that the agent explicitly knows all classical tautologies and all logical consequences of his or her knowledge. We provide a sound and complete axiomatization for this logic.

Sign in / Sign up

Export Citation Format

Share Document