Modal logic and the approximation induction principle
type: Item
instance of: scholarly article
title: Modal logic and the approximation induction principle
zbMATH Open document ID: 1260.68266
DOI: 10.1017/S0960129511000387
author: Maciej Gazda
author: Wan Fokkink
publication date: 2012-05-11T00:00:00Z
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 6033364
zbMATH Keywords: modal logic
zbMATH Keywords: Hennessy-Milner theorem
zbMATH Keywords: bisimulations
zbMATH Keywords: process equivalence
zbMATH Keywords: finite preorders
zbMATH Keywords: approximation induction principle
MaRDI profile type: Publication
cites work: Precongruence formats for decorated trace semantics
cites work: Process Algebra
cites work: Proof systems for satisfiability in Hennessy-Milner logic with recursion
cites work: On the consistency of Koomen's fair abstraction rule
cites work: Algebraic laws for nondeterminism and concurrency
cites work: Turning SOS rules into equations
cites work: Correcting a Space-Efficient Simulation Algorithm
published in: MSCS. Mathematical Structures in Computer Science
review text: Hennessy Milner Logic, HML, is given through formulas NEWLINE\[NEWLINE \phi ::= \top \mid \bigwedge_{i\in I}\phi_i \mid \langle a \rangle \phi \mid \neg \phi, NEWLINE\]NEWLINE where \(I\) is an arbitrary index set; this logic is modified by replacing negation through a box operator \([a]\) and by adding disjunctions indexed by an arbitrary index set \(I\), yielding a logic HML\({}^+\). These logics are interpreted in a canonic way through a labelled transition system. Define for a sublogic \(\mathcal{O}\) an equivalence relation \(\sim_\mathcal{O}\) on the states of an labelled transition system through the satisfaction od exactly the same formulas in \(\mathcal{O}\). Conditions are investigated under which \(\sim_\mathcal{O}\) and \(\sim_{\mathcal{O}_{\text{FIN}}}\) resp. \(\sim_\mathcal{O}\) and \(\sim_{\mathcal{O}_{\text{FDP}}}\) coincide for image finite transition systems, where \(\mathcal{O}_{\text{FIN}}\) and \(\mathcal{O}_{\text{FDP}}\) are all formulas in \(\mathcal{O}\) that do not contain infinite conjunctions resp. are of finite depth. Since \(\mathcal{O}\) can be interpreted as a modal characterization of trace semantics, this yields a compactness result for these semantics. The results are compared to earlier results due to \textit{R. Goldblatt} and \textit{M. Hollenberg} [CSLI Lecture Notes 53, 189--216 (1995)] for modally saturated processes.NEWLINENEWLINE The second part of the paper introduces and discusses the approximation induction principle: Given projection operators, this principle states that two processes are equal if and only if they are equal up to any finite depth. Soundness of this principle is investigated in terms of HML-formulas of finite depth, and a simulation preorder is defined. Some complexity results are derived through sophisticated combinatorial arguments. They help constructing algorithmically a labelled transition system for which the simulation preorder stabilizes.NEWLINENEWLINEThe paper utilizes and extends the results gi…
reviewed by: Ernst-Erich Doberkat
description: scientific article; zbMATH DE number 6033364