Various planning-based know-how logics have been proposed and studied in the recent literature. In this paper, we use such a logic to do know-how-based planning via model checking. In particular, we can handle the higher-order epistemic planning involving know-how formulas as the goal, e.g., find a plan to make sure p such that the adversary does not know how to make p false afterward. We give a PTIME-algorithm for the model checking problem over finite epistemic transition systems and axiomatize the logic under the assumption of perfect recall.
In this paper, we propose a lightweight yet powerful dynamic epistemic logic that not only captures the distinction between de dicto and de re knowledge but also the distinction between de dicto and de re updates. The logic is based on the dynamified version of an epistemic language extended with the assignment operator borrowed from dynamic logic, following the work of Wang and Seligman (2018). We obtain complete axiomatizations for the counterparts of public announcement logic and event-model-based DEL based on new reduction axioms taking care of the interactions between dynamics and assignments.
Abstract. Weakly Aggregative Modal Logic (WAML) is a collection of disguised polyadic modal logics with n-ary modalities whose arguments are all the same. WAML has some interesting applications on epistemic logic and logic of games, so we study some basic model theoretical aspects of WAML in this paper. Specically, we give a van Benthem-Rosen characterization theorem of WAML based on an intuitive notion of bisimulation and show that each basic WAML system Kn lacks Craig Interpolation.
Abstract. There are currently two approaches to the logic of knowing how: the planning-based one and the coalition-based one. However, the rst is single-agent, and the second is based on single-step joint actions. In this paper, to overcome both limitations, we propose a multi-agent framework for the logic of knowing how, based on multi-step dynamic epistemic planning studied in the literature. We obtain a sound and com- plete axiomatization and show that the logic is decidable, although the corresponding multi-agent epistemic planning problem is undecidable.
Abstract: In this paper, we propose a logical framework extending the standard epistemic logic with a new knowledge operator $\G_i$ which captures the knowledge about (physically) necessary facts, e.g., scientific knowledge. Semantically, the truth of $\G_i\phi$ depends on not only the epistemically indistinguishable worlds from the current real world but also the relevant (physically) possible worlds which are clearly distinguishable. Essentially, $\G_i$ is a bundle of the standard epistemic modality and a necessity-like modality. We axiomatize the corresponding epistemic logic completely in single- and multi-agent cases with interesting interaction axioms between the two epistemic operators.
Abstract. In standard epistemic logic, knowing that p is the same as knowing that p is true, but it does not say anything about understanding p or knowing its meaning. In this paper, we present a conservative extension of Public Announcement Logic (PAL) in which agents have knowledge or belief about both the truth values and the meanings of propositions. We give a complete axiomatization of PAL with Boolean Definitions and discuss various examples. An agent may understand a proposition without knowing its truth value or the other way round. Moreover, multiple agents can agree on something without agreeing on its meaning and vice versa.
Abstract: In standard epistemic logic, agent names are usually assumed to be common knowledge implicitly. This is unreasonable for various applications. Inspired by term modal logic and assignment operators in dynamic logic, we introduce a lightweight modal predicate logic where names can be non-rigid. The language can handle various de dicto and de re distinctions in a natural way. The main technical result is a complete axiomatisation of this logic over S5 models.
Abstract: Quantified modal logic provides a natural logical language for reasoning about modal attitudes even while retaining the richness of quantification for referring to predicates over domains. But then most fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic) have been shown to be decidable. In this paper, we study fragments that bundle quantifiers and modalities together, inspired by earlier work on epistemic logics of know-how/why/what. As always with quantified modal logics, it makes a significant difference whether the domain stays the same across worlds, or not. In particular, we show that the bundle is undecidable over constant domain interpretations, even with only monadic predicates, whereas bundle is decidable. On the other hand, over increasing domain interpretations, we get decidability with both and bundles with unrestricted predicates. In these cases, we also obtain tableau based procedures that run in PSPACE. We further show that the bundle cannot distinguish between constant domain and increasing domain interpretations.
Abstract. In this paper, we propose a single-agent logic of goal-directed knowing how extending the standard epistemic logic of knowing that with a new knowing how operator. The semantics of the new operator is based on the idea that knowing how to achieve means that there exists a (uniform) strategy such that the agent knows that it can make sure . We give an intuitive axiomatization of our logic and prove the soundness, completeness, and decidability of the logic. The crucial axioms relating knowing that and knowing how illustrate our understanding of knowing how in this setting. This logic can be used in representing both knowledge-that and knowledge-how.
Abstract: We present a basic dynamic epistemic logic of “knowing the value”. Analogous to public announcement in standard DEL, we study “public inspection”, a new dynamic operator which updates the agents’ knowledge about the values of constants.We provide a sound and strongly complete axiomatization for the single and multi-agent case, making use of the well-known Armstrong axioms for dependencies in databases.
Abstract: In this paper, we propose a ternary knowing how operator to express that the agent knows how to achieve $\phi$ given $\psi$ while maintaining $\chi$ in-between. It generalizes the logic of goal-directed knowing how proposed by Wang in . We give a sound and complete axiomatization of this logic.
Abstract: Recent years witnessed a growing interest in non-standard epistemic logics of knowing whether, knowing how, knowing what, knowing why and so on. The new epistemic modalities introduced in those logics all share, in their semantics, the general schema of , e.g., knowing how to achieve roughly means that there exists a way such that you know that it is a way to ensure that Moreover, the resulting logics are decidable. Inspired by those particular logics, in this work, we propose a very general and powerful framework based on quantifier-free predicate language extended by a new modality x, which packs exactly x together. We show that the resulting language, though much more expressive, shares many good properties of the basic propositional modal logic over arbitrary models, such as finite-tree-model property and van Benthem-like characterization w.r.t. first-order modal logic. We axiomatize the logic over S5 frames with intuitive axioms to capture the interaction between x and know-that operator in an epistemic setting.
Abstract. Recent years witness a growing interest in nonstandard epistemic logics of “knowing whether”, “knowing what”, “knowing how”, and so on. These logics are usually not normal, i.e., the standard axioms and reasoning rules for modal logic may be invalid. In this paper, we show that the conditional “knowing value” logic proposed by Wang and Fan (2013) can be viewed as a disguised normal modal logic by treating the negation of the Kv operator as a special diamond. Under this perspective, it turns out that the original first-order Kripke semantics can be greatly simplified by introducing a ternary relation in standard Kripke models, which associates one world with two i-accessible worlds that do not agree on the value of constant c. Under intuitive constraints, the modal logic based on such Kripke models is exactly the one studied by Wang and Fan (2013,2014). Moreover, there is a very natural binary generalization of the “knowing value” diamond, which, surprisingly, does not increase the expressive power of the logic. The resulting logic with the binary diamond has a transparent normal modal system, which sharpens our understanding of the “knowing value” logic and simplifies some previously hard problems.
Abstract. When reasoning about knowledge of procedures under imperfect information, the explicit representation of epistemic possibilities blows up the S5-like models of standard epistemic logic. To overcome this drawback, in this paper, we propose a new logical framework based on compact models without epistemic accessibility relations for reasoning about knowledge of procedures. Inspired by the 3-valued abstraction method in model checking, we introduce hyper models which encode the imperfect procedural information. We give a highly non-trivial 2-valued semantics of epistemic dynamic logic on such models while validating all the usual S5 axioms. Our approach is suitable for applications where procedural information is ‘learned’ incrementally, as demonstrated by various examples.
Abstract: In this paper, we propose a single-agent modal logic framework for reasoning about goal-direct “knowing how” based on ideas from linguistics, philosophy, modal logic and automated planning. We first define a modal language to express “I know how to guarantee phi given $\psi$” with a semantics not based on standard epistemic models but labelled transition systems that represent the agent’s knowledge of his own abilities. A sound and complete proof system is given to capture the valid reasoning patterns about “knowing how” where the most important axiom suggests its compositional nature.
Abstract: In this paper, we introduce a lightweight dynamic epistemic logical framework for automated plan-ning under initial uncertainty. We reduce plan verification and conformant planning to model check-ing problems of our logic. We show that the model checking problem of the iteration-free fragment is PSPACE-complete. By using two non-standard (but equivalent) semantics, we give novel model checking algorithms to the full language and the iteration-free language.
Abstract. Classic epistemic logic focuses on propositional knowledge expressed by “knowing that” operators. However, there are various types of knowledge used in natural language, in terms of “knowing how”, “knowing whether”, “knowing what”, and so on. In , Plaza proposed an intuitive know-what operator which was generalized in  by introducing a condition. The latter know-what operator can express natural conditional knowledge such as $\backslash$I know what your password is, if it is 4-digits”, which is not simply a material implication. Essentially this know-what operator packages a first-order quantifier and an S5-modality together in a non-trivial way, thus making it hard to axiomatize. In  an axiomatization is given for the single-agent epistemic logic with both know-that and know-what operators, while leaving axiomatizing the multi-agent case open due to various technical difficulties. In this paper, we solve this open problem. The completeness proof is highly non-trivial, compared to the singleagent case, which requires different techniques inspired by first-order intensional logic.
Abstract. A formula is contingent if it is possibly true and possibly false. A formula is non- contingent if it is not contingent, i.e., if it is necessarily true or necessarily false. In an epistemic setting, a formula is contingent’ means that you are ignorant about its value, whereas a formula is non-contingent’ means that you know whether it is true. Although non-contingency is definable in terms of necessity as above, necessity is not always definable in terms of non-contingency, as studied in the literature. We propose an almost-definability’ schema AD for non-contingency logic, the logic with the noncontingency operator as the only modality, making precise when necessity is definable with non-contingency. Based on AD we propose a notion of bisimulation for non- contingency logic, and characterize non-contingency logic as the (non-contingency) bisimulation invariant fragment of modal logic and of first-order logic. A known pain for non-contingency logic is the absence of axioms characterizing frame properties. This makes it harder to find axiomatizations of non-contingency logic over given frame classes. In particular, no axiomatization over symmetric frames is known, despite the rich results about non-contingency logic obtained in the literature since the 1960s. We demonstrate that the almost-definability’ schema AD can guide our search for proper axioms for certain frame properties, and help us in defining the canonical models. Following this idea, as the main result, we give a complete axiomatization of non-contingency logic over symmetric frames.
Abstract. In everyday life, people get lost even when they have the map: they simply may not know where they are in the map. However, when moving forward they may have new observations which can help to locate themselves by reasoning. In this paper, we propose and develop a semantic-driven dynamic epistemic framework to handle epistemic reasoning in such navigation scenarios. Our framework can be viewed as a careful blend of dynamic epistemic logic and epistemic temporal logic, thus enjoying features from both frameworks. We made an in-depth study on many model theoretical aspects of the proposed framework and provide a complete axiomatization.
Abstract. In social interactions, protocols govern our behavior and assign meaning to actions. In this paper, we investigate the dynamics of protocols and their epistemic effects. We develop two logics, inspired by Propositional Dynamic Logic (PDL) and Public Announcement Logic (PAL), for reasoning about protocol change and knowledge updates. We show that these two logics can be translated back to the standard PDL and PAL respectively.
Abstract. In the literature, different axiomatizations of Public Announcement Logic (PAL) were proposed. Most of these axiomatizations share a ‘core set’ of the so-called reduction axioms. In particular, there is a composition axiom which stipulates how two consecutive announcements are composed into one. In this paper, by designing non-standard Kripke semantics for the language of PAL, we show that without the composition axiom the core set does not completely axiomatize PAL. In fact, most of the intuitive ‘axioms’ and rules we took for granted could not be derived from the core set. The non-standard semantics we proposed is of its own interest in modelling realistic agents. We show that with the help of different composition axioms we may axiomatize PAL w.r.t. such non-standard semantics.
Abstract. In this paper, we develop an epistemic logic for specifying and reasoning about information flow on the underlying communication channels. By combining ideas from Dynamic Epistemic Logic (DEL) and Interpreted Systems (IS), our semantics offers a natural and neat way of modeling multi-agent communication scenarios with different assumptions about the observational power of agents. We relate our logic to the standard DEL and IS approaches and demonstrate its use by studying a telephone call communication scenario.
Abstract appeared at AAMAS2010
When agents know a protocol, this leads them to have expectations about future observations. Agents can update their knowledge by matching their actual observations with the expected ones. They eliminate states where they do not match. In this paper, we study how agents perceive protocols that are not commonly known, and propose a logic to reason about knowledge in such scenarios.
Abstract. Epistemic protocols are communication protocols aiming at transfer of knowledge in a controlled way. Typically, the preconditions or goals for protocol actions depend on the knowledge of agents, often in nested form. Informal epistemic protocol descriptions for muddy children, coordinated attack, dining cryptographers, Russian cards, secret key exchange are well known. The contribution of this paper is a formal study of a natural requirement on epistemic protocols, that the contents of the protocol can be assumed to be common knowledge. By formalizing this requirement we can prove that there can be no unbiased deterministic protocol for the Russian cards problem. For purposes of our formal analysis we introduce an epistemic protocol language, and we show that its model checking problem is decidable.
Abstract. We propose a property-preserving refinement/abstraction theory for Kripke Modal Labelled Transition Systems incorporating not only state mapping but also label and proposition lumping, in order to have a compact but informative abstraction. We develop a 3-valued version of Public Announcement Logic (PAL) which has a dynamic operator that changes the model in the spirit of public broadcasting. We prove that the refinement relation on static models assures us to safely reason about any dynamic properties in terms of PAL-formulas on the abstraction of a model. The theory is in particular interesting and applicable for an epistemic setting as the example of the Muddy Children puzzle shows, especially in the view of the growing interest for epistemic modelling and (automatic) verification of communication protocols.
Abstract. We present a thorough study of Propositional Dynamic Logic over a variation of labeled transition systems, called accelerated labelled transition systems, which are transition systems labeled with regular expressions over action labels. We study the model checking and satisfiability decision problems. Through a notion of regular expression rewriting, we reduce these two problems to the corresponding ones of PDL in the traditional semantics (w.r.t. LTS). As for the complexity, both of problems are proved to be EXPSPACE-complete. Moreover, the program, complexity of model checking problem turns out to be Nlogspace-complete. Furthermore, we provide an axiomatization for PDL which involves Kleene Algebra as an Oracle. The soundness and completeness are shown.