The expressive power of implicit specifications
type: Item
instance of: scholarly article
title: The expressive power of implicit specifications
zbMATH Open document ID: 0779.68059
DOI: 10.1016/0304-3975(93)90155-M
published in: Theoretical Computer Science
publication date: 1993-10-25T00:00:00Z
review text: We investigate the expressive power of implicit specifications of concurrent systems. That is, we consider specifications \(S\) specifying a system \(P\) not directly, but rather in combination with a given environment. Formally, we shall represent the environment as a \(CCS\) context of the form \((A\mid[\;][\Phi])\setminus L\), where \(A\) is a process expression and \(\mid\), \(\setminus L\) and \([\Phi]\) are the parallel, restriction and renaming operators of \(CCS\), respectively. We investigate the expressive power of the following three types of implicit specifications: (i) \((A\mid P[\Phi])\setminus L\sim B\), where \(\sim\) is strong bisimulation equivalence and \(B\) is a process expression; (ii) \((A\mid P[\Phi])\setminus L\triangleleft S\), where \(S\) is a modal specification and \(\triangleleft\) is refinement between modal specifications (a generalization of bisimulation equivalence); and (iii) \((A\mid P[\Phi])\setminus L\models F\), where \(F\) is a formula of Hennessy-Milner logic extended with a (maximal) recursion construct. The paper offers the following two main results. When \(A\),\(B\) and \(S\) are recursion-free and \(F\) is a Hennessy-Milner logic formula, the expressive powers of all three types of implicit specifications are the same and equal that of Hennessy-Milner logic. When \(A\) and \(S\) are regular, the expressive powers of implicit specifications of type (ii) and (iii) are the same and identical to that of Hennessy-Milner logic extended with (maximal) recursion. Finally, we recall from \textit{K. G. Larsen} and \textit{L. Xinxin} [Lect. Notes Comput. Sci. 443, 526-539 (1990; Zbl 0765.68107)] that the expressive power of implicit specifications does not increase by modelling the environment as other contexts (of CCS or other process calculi).
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q10
zbMATH DE Number: 417349
zbMATH Keywords: implicit specifications
zbMATH Keywords: concurrent systems
zbMATH Keywords: Hennessy-Milner logic
author: Kim G. Larsen
describes a project that uses: LOTOS
MaRDI profile type: Publication
cites work: A linear algorithm to solve fixed-point equations on transition systems
cites work: The temporal logic of branching time
cites work: Q4027619
cites work: Tableau-based model checking in the propositional mu-calculus
cites work: Q4036558
cites work: Higher-level synchronising devices in Meije-SCCS
cites work: Propositional dynamic logic of regular programs
cites work: Algebraic laws for nondeterminism and concurrency
cites work: Q3777424
cites work: Q3700806
cites work: Q4732449
cites work: Q2736352
cites work: Q4744245
cites work: Q3792217
cites work: Compositionality Through an Operational Semantics of Contexts
cites work: On the Construction of Submodule Specifications and Communication Protocols
cites work: A calculus of communicating systems
cites work: Calculi for synchrony and asynchrony
cites work: A complete inference system for a class of regular behaviours
cites work: Q3992568
cites work: Q3907077
cites work: Submodule construction as equation solving in CCS
cites work: Q3694687
cites work: Local model checking in the modal mu-calculus
cites work: Q3033311
full work available at URL: 0304-3975(93)90155-m
OpenAlex ID: W1967594083
description: scientific article; zbMATH DE number 417349