Temporal aspects of the modal logic of subset spaces
type: Item
instance of: scholarly article
title: Temporal aspects of the modal logic of subset spaces
zbMATH Open document ID: 0951.03014
DOI: 10.1016/S0304-3975(98)00310-7
author: Bernhard Heinemann
published in: Theoretical Computer Science
publication date: 2000-01-12T00:00:00Z
review text: A logic of knowledge and time is presented in the paper. It seems that a combination of knowledge and time in the frame of modal logic provides a powerful tool for applications in computer science and artificial intelligence. The author starts off with the so-called topological modal logic of Moss and Parikh. The logic describes the situations in which the knowledge of an agent increases if computational effort is spent. The increasing of knowledge amounts to a successive shrinking of the set of states the agent considers possible in the course of time. In this way a topological component comes into play. Formally, the logic is a bimodal system with two operators, \(K\) representing knowledge and \(\square\) representing effort. Heinemann's logic makes more explicit the temporal content of the effort operator by adding a nextstep operator to the Moss-Parikh formalism. A language \(LK\) is defined. It is based on a set \(PV\) of propositional variables. Formulas are defined as usual, using propositional connectives and modal operators. The basic modal operators are \(K\), \(\circ\) (nextstep), and \(\square\). The semantical structures are triples \((X, d, \sigma)\) (called subset tree models). \(X\) is a non-empty set. From the viewpoint of topological reasoning \(d\) is a crucial component: is is a sequence \(\langle E_{1}, \dots, E_{n}, \dots \rangle\) of equivalence relations on X such that for each \(j\) every class of \(E_{j}\) splits into some classes of \(E_{j+1}\) (the knowledge leads to a more detailed ability to distinguish). The pair \({\mathcal F} = (X, d)\) is called a subset tree frame. Finally, \(\sigma\) is a valuation (a mapping from \(PV \times X\) to \(\{ 0, 1 \}\)). A common satisfiability relation is defined and a set of axioms is proposed. It is proved that the axiomatization is sound and complete. Moreover, the set of \(LK\)-formulas holding in every subset tree model is decidable. The paper contains also some complexity results. The satisfiab…
Mathematics Subject Classification ID: 03B42
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68T30
Mathematics Subject Classification ID: 68T27
zbMATH DE Number: 1387348
zbMATH Keywords: logic of knowledge and time
zbMATH Keywords: modal logic
zbMATH Keywords: temporal logic
zbMATH Keywords: topological reasoning
zbMATH Keywords: nextstep operator
zbMATH Keywords: subset tree models
zbMATH Keywords: satisfiability
zbMATH Keywords: axiomatization
reviewed by: Jan Šefránek
MaRDI profile type: Publication
cites work: Q4293537
cites work: Q3867808
cites work: The complexity of propositional linear temporal logics
cites work: Topological reasoning and the logic of knowledge
cites work: Q4845472
cites work: Q4537445
cites work: Q3773852
cites work: Q4215596
description: scientific article; zbMATH DE number 1387348