Weakly Aggregative Modal Logic: Characterization and Interpolation

LORIProceeding Paper
Jixin Liu, Yanjing Wang, Yifeng Ding
Proceedings of LORI 2019
Publication year: 2019

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.

Multi-agent knowing how via multi-step plans: a dynamic epistemic planning based approach

Beyond know-thatLORIProceeding Paper
Yanjun Li, Yanjing Wang
Proceedings of LORI 2019
Publication year: 2019

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.

Knowledge-now and Knowledge-all

LORIProceeding Paper
Xinyu Wang, Yanjing Wang
Proceedings of LORI 2019
Publication year: 2019

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.

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.

When Names Are Not Commonly Known: Epistemic Logic with Assignments

AiMLBeyond know-thatBook ChapterProceeding Paper
Wang, Yanjing and Seligman, Jeremy
Advances in Modal Logic Vol.12, College Publications: 611—628, 2018
Publication year: 2018

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.

Bundled fragments of first-order modal logic: (un)decidability

Beyond know-thatProceeding Paper
Padmanabha, Anantha and Ramanujam, R. and Wang, Yanjing
In Proceedings of Foundations of Software Technology and Theoretical Computer Science (FSTTCS) 2018, 2018
Publication year: 2018

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 \forall \Box is undecidable over constant domain interpretations, even with only monadic predicates, whereas \exists \Box bundle is decidable. On the other hand, over increasing domain interpretations, we get decidability with both \forall \Box and \exists \Box bundles with unrestricted predicates. In these cases, we also obtain tableau based procedures that run in PSPACE. We further show that the \exists \Box bundle cannot distinguish between constant domain and increasing domain interpretations.

Strategically knowing how

Beyond know-thatIJCAIProceeding PaperSelected
Fervari, Raul and Herzig, Andreas and Li, Yanjun and Wang, Yanjing
In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI) 2017, 2017
Publication year: 2017

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 \phi means that there exists a (uniform) strategy such that the agent knows that it can make sure \phi. 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.

Knowing values and public inspection

Beyond know-thatICLAProceeding Paper
Van Eijck, Jan and Gattinger, Malvin and Wang, Yanjing
In Proceedings of International Conference on Logic and its Applications (ICLA) 2017, 2017
Publication year: 2017

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.

Achieving while maintaining: A logic of knowing how with intermediate constraints

Beyond know-thatICLAProceeding Paper
Li, Yanjun and Wang, Yanjing
In Proceedings of International Conference on Logic and its Applications (ICLA) 2017, 2017
Publication year: 2017

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 [10]. We give a sound and complete axiomatization of this logic.

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.

Knowing value logic as a normal modal logic

AiMLBeyond know-thatBook ChapterProceeding Paper
Gu, Tao and Wang, Yanjing
Advances in Modal Logic, College Publications, 11: 362—381, 2016
Publication year: 2016

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 R_i^c 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.

Representing Imperfect Information of Procedures with Hyper Models

ICLAProceeding Paper
Wang, Yanjing
In Proceedings of International Conference on Logic and its Applications (ICLA) 2015, 2015
Publication year: 2015

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.

A logic of knowing how

Beyond know-thatLORIProceeding Paper
Wang, Yanjing
In Proceedings of LORI ’15, 2015
Publication year: 2015

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.

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.

Conditionally knowing what

AiMLBeyond know-thatBook ChapterProceeding Paper
Wang, Yanjing and Fan, Jie
Advances in Modal Logic Vol.10, College Publications: 569—587, 2014
Publication year: 2014

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 [10], Plaza proposed an intuitive know-what operator which was generalized in [16] 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 [16] 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.

Almost necessary

AiMLBeyond know-thatBook ChapterProceeding Paper
Fan, Jie and Wang, Yanjing and van Ditmarsch, Hans
Advances in Modal Logic Vol.10, College Publications, 10: 178—196, 2014
Publication year: 2014

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.

Knowing that, knowing what, and public communication: Public announcement logic with Kv operators

Beyond know-thatIJCAIProceeding Paper
Wang, Yanjing and Fan, Jie
In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI) 2013, 2013
Publication year: 2013

An alternative axiomatization of DEL and its applications

IJCAIProceeding Paper
Wang, Yanjing and Aucher, Guillaume
In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI) 2013, 2013
Publication year: 2013

Not All Those Who Wander Are Lost: Dynamic Epistemic Reasoning in Navigation

AiMLBook ChapterProceeding Paper
Wang, Yanjing and Li, Yanjun
Advances in Modal Logic, College Publications, 9: 559—580, 2012
Publication year: 2012

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.

Reasoning about protocol change and knowledge

ICLAProceeding Paper
Wang, Yanjing
In Proceedings of International Conference on Logic and its Applications (ICLA) 2011, 2011
Publication year: 2011

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.

On axiomatizations of PAL

LORIProceeding Paper
Wang, Yanjing
In Proceedings of LORI 2011, 2011
Publication year: 2011

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.

Logic of information flow on communication channels (full paper)

Proceeding Paper
Wang, Yanjing and Sietsma, Floor and Van Eijck, Jan
In Proceedings of DALT 2010, 2011
Publication year: 2011

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

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.

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.

Refinement of Kripke Models for dynamics

Proceeding Paper
Dechesne, Francien and Orzan, Simona and Wang, Yanjing
In Proceedings of ICTAC 2008, 2008
Publication year: 2008

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.

Propositional dynamic logic as a logic of belief revision

Proceeding Paper
Van Eijck, Jan and Wang, Yanjing
In Proceedings of WOLLIC 2008, 2008
Publication year: 2008

PDL over accelerated labeled transition systems

Proceeding Paper
Chen, Taolue and Van De Pol, Jaco and Wang, Yanjing
In Proceedings of IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE) 2008, 2008
Publication year: 2008

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.

Risk Balance in Exchange Protocols

Proceeding Paper
Torabi Dashti, Mohammad and Wang, Yanjing
In Proceedings of ASIAN 2007, 2007
Publication year: 2007

Dynamic epistemic verification of security protocols : framework and case study

LORIProceeding Paper
Dechesne, Francien and Wang, Yanjing
In Proceedings of LORI 2007, 2007
Publication year: 2007