Dazhu Li

Dynamical systems model physical processes, but also computing, informational inquiry, or interaction in games. Some attractive modal logics exist for analyzing high-level behavior of dynamical systems, such as Dynamic Topological Logic. Adding to these, we focus on the fine-structure of states, associating them with assignments of values to variables. We present a logic with a perspicuous syntax for reasoning about dependencies over time. We study the properties of this system by presenting an effective reduction to a basic modal logic of functional dependence. This can be seen as justifying a common intuition that temporal dependence is a special case of general dependence when we follow the course of time. We also consider the addition of standard temporal modalities to this logic, where the reductive intuition no longer holds in general. On this base, we then introduce topological structure, and investigate the logic of continuous dependence given a continuous transition function, which can also be seen as modelling not just dependence but monotonic dependence for patterns of growth. Finally, we briefly discuss some further logical structures in dynamical systems such as term equalities, independence and non-deterministic choice.

In the tradition of memory logic, two comparatively weak systems, poison modal logic (PML) and poison sabotage logic (PSL), were studied in existing literature to capture the so-called poison game, which originally served as a paradigm to reason about graph- theoretical notions and was recently shown to have important applications in the theory of abstract argumentation. In this work, we continue to explore the technical aspect of the two logics and complete the existing results by providing our solutions to the questions identified in the literature [19, 20, 13]. Precisely, we show that (i) neither of them can be embedded in fixed-variable fragment of first-order logic, on the basis of the existing findings for PML and PSL, (ii) PSL has an undecidable satisfiability problem, and (iii) motivated by the existing axiomatization results for the standard memory logic [5], we axiomatize the two logics in a broader setting with enrichments from hybrid logic. As we shall see, in line with the fact that PSL is strictly weaker than PML, the calculus for the hybrid PSL developed will also be a ‘fragment’ of that for the hybrid PML.

The logic of the hide and seek game $$\textbf{LHS}$$ was proposed to capture interactions between agents in pursuit-evasion environments. In this paper, we explore a hybrid extension of $$\textbf{LHS}$$ and show that such an extension is beneficial in several aspects. We will show that it improves the technical properties of the resulting logical system, and expands the potential applications of the system. Specifically, we will investigate the expressive power of the hybrid logic of the hide and seek game $${\mathcal {H}}(\textbf{LHS})$$ and its crucial fragment $${\mathcal {H}}(\textbf{LHS}^{-})$$, at both model and frame levels. We will present complete Hilbert-style proof systems for both the logics $${\mathcal {H}}(\textbf{LHS}^{-})$$ and $${\mathcal {H}}(\textbf{LHS})$$, which in fact provides a solution to a known open problem.

The game of Cops and Robbers is an important model for studying computa-tional queries in pursuit-evasion environments, among others. As recent logical explorations have shown, its structure exhibits appealing analogies with modal logic. In this paper, we enrich the game with a setting in which players may have imperfect information. We propose a new formal framework, Epistemic Logic of Cops and Robbers (ELCR), to make the core notions of the game precise, for instance, players’ positions, observational power and inference. Applying ELCR to analyze the game, we obtain an automated way to track interactions between players and characterize their information updates during the game. The update mechanism is defined by a novel dynamic operator, and we compare it with some relevant paradigms from the game and logic perspectives. We study various prop-erties of ELCR including axiomatization and decidability. To our knowledge, this is the first attempt to explore these games from a formal point of view where (partial) information available to players is taken into account.

In this paper, using a propositional modal language extended with the window modality, we capture the first-order properties of various mereological theories. In this setting,$\Box \varphi $readsall the parts(of the current object)are$\varphi $, interpreted on the models with awhole-partbinary relation under various constraints. We show that all the usual mereological theories can be captured by modal formulas in our language via frame correspondence. We also correct a mistake in the existing completeness proof for a basic system of mereology by providing a new construction of the canonical model.

Formal learning theory formalizes the process of inferring a general result from examples, as in the case of inferring grammars from sentences when learning a language. In this work, we develop a general framework—the supervised learning game—to investigate the interaction between Teacher and Learner. In particular, our proposal highlights several interesting features of the agents: on the one hand, Learner may make mistakes in the learning process, and she may also ignore the potential relation between different hypotheses; on the other hand, Teacher is able to correct Learner’s mistakes, eliminate potential mistakes and point out the facts ignored by Learner. To reason about strategies in this game, we develop a modal logic of supervised learning and study its properties. Broadly, this work takes a small step towards studying the interaction between graph games, logics and formal learning theory.

We discuss a simple logic to describe one of our favourite games from childhood, hide and seek, and show how a simple addition of an equality constant to describe the winning condition of the seeker makes our logic undecidable. There are certain decidable fragments of first-order logic which behave in a similar fashion with respect to such a language extension, and we add a new modal variant to that class. We discuss the relative expressive power of the proposed logic in comparison to the standard modal counterparts. We prove that the model checking problem for the resulting logic is \(\textsf{P}\) -complete. In addition, by exploring the connection with related product logics, we gain more insight towards having a better understanding of the subtleties of the proposed framework.