On the modal definability of simulability by finite transitive models
type: Item
instance of: scholarly article
title: On the modal definability of simulability by finite transitive models
zbMATH Open document ID: 1246.03042
published in: Studia Logica
publication date: 2012-03-09T00:00:00Z
review text: Given a finite, transitive and reflexive Kripke model \(\langle W, \preccurlyeq, [ \mkern-3mu [ \cdot ] \mkern-3mu ] \rangle\) and \(w \in W\), it is shown that the property ``being simulated by \(w\)'' (i.e. lying on the image of a literal-preserving relation satisfying the ``forth'' condition of bisimulation) is modally undefinable within the class of \({\mathsf S4}\) Kripke models (contrary to \({\mathsf K4}\), which is also proved). A minor extension of the language by adding a sequent operator \(\natural\) (``tangle'') which can be interpreted over Kripke models as well as over topological spaces is proposed. In the extended language \({\mathsf L}^+ = {\mathsf L}^{\square \natural}\), being simulated by a point on a finite transitive Kripke model becomes definable, both over the class of arbitrary Kripke models and over the class of topological \({\mathsf S4}\) models. As a consequence it is obtained that any class of finite, transitive models over finitely many propositional variables closed under simulability is also definable in \({\mathsf L}^+\), as well as Boolean combinations of these classes. From this it follows that the \(\mu\)-calculus interpreted over any such class of models is decidable.
reviewed by: Damas Gruska
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 6013484
zbMATH Keywords: modal logic
zbMATH Keywords: bisimulation
zbMATH Keywords: decidability, mu-calculus
zbMATH Keywords: Kripke model
zbMATH Keywords: simulation
author: David Fernández-Duque
MaRDI profile type: Publication
full work available at URL: s11225-011-9339-x
OpenAlex ID: W2003311901
cites work: Q3367295
cites work: Modal languages and bounded fragments of predicate logic
cites work: Modal correspondence for models
cites work: Modal logic
cites work: Ultrafilters: Some old and some new results
cites work: Modal characterisation theorems over special classes of frames
cites work: Non-deterministic semantics for dynamic topological logic
cites work: Non-primitive recursive decidability of products of modal logics with expanding domains
cites work: Results on the propositional \(\mu\)-calculus
cites work: A finite model theorem for the propositional \(\mu\)-calculus
cites work: Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
cites work: Q3219755
DOI: 10.1007/S11225-011-9339-X
description: scientific article; zbMATH DE number 6013484