Knowing How to Plan

Beyond know-thatProceeding PaperTARK
Yanjun Li, Yanjing Wang
in Proceedings of TARK2021
Publication year: 2021

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.

De Re Updates

Proceeding PaperTARK
Michael Cohen, Wen Tang, Yanjing Wang
Proceedings of TARK2021
Publication year: 2021

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.

How to Agree without Understanding Each Other: Public Announcement Logic with Boolean Definitions

Proceeding PaperTARK
Gattinger, Malvin and Wang, Yanjing
In Proceedings on Conference on Theoretical Aspects of Rationality and Knowledge (TARK) 2019, 2019
Publication year: 2019

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.

A New Modal Framework for Epistemic Logic

Beyond know-thatProceeding PaperSelectedTARK
Wang, Yanjing
Proceedings of Conference on Theoretical Aspects of Rationality and Knowledge (TARK) 2017, 251: 515—534, 2017
Publication year: 2017

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 \exists x\phi, e.g., knowing how to achieve \phi roughly means that there exists a way such that you know that it is a way to ensure that \phi 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.

A Dynamic Epistemic Framework for Conformant Planning

Proceeding PaperTARK
Yu, Quan and Li, Yanjun and Wang, Yanjing
In Proceedings on Conference on Theoretical Aspects of Rationality and Knowledge (TARK) 2015, 2015
Publication year: 2015

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.

Hidden protocols

Proceeding PaperTARK
van Ditmarsch, Hans and Ghosh, Sujata and Verbrugge, Rineke and Wang, Yanjing
In Proceedings of Conference on Theoretical Aspects of Rationality and Knowledge (TARK) 2011, 2011
Publication year: 2011

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.

(largely extended journal version of the TARK2011 paper)

Verifying epistemic protocols under common knowledge

Proceeding PaperTARK
Wang, Yanjing and Kuppusamy, Lakshmanan and van Eijck, Jan
In Proceedings of Conference on Theoretical Aspects of Rationality and Knowledge (TARK) 2009, 2009
Publication year: 2009

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.