Compositional checking of satisfaction

DOI10.1007/BF00709155MaRDI QIDQ685107zbMATH OpenFDO

Authors Henrik Reif Andersen, Glynn Winskel

Publication date 30 September 1993

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF00709155

zbMATH Keywords

compositionalitymodal \(\mu\)-calculusmodel checkingprocess calculi

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The paper presents a compositional method for deciding whether a process satisfies an assertion. Assertions are formulae in a modal \(\nu\)-calculus (the dual of the modal \(\mu\)-calculus), and processes are drawn from a very general process algebra inspired by CCS and CSP. Well-known operators from CCS, CSP, and other process algebras appear as derived operators. The method is compositional in the structure of processes and works purely on the syntax of processes. It consists of applying a sequence of reductions, each of which only take into account the top-level operator of the process. A reduction transforms a satisfaction problem for a composite process into equivalent satisfaction problems for the immediate subcomponents. Using process variables, systems with undefined subcomponents can be defined, and given an overall requirement to the system, necessary and sufficient conditions on these subcomponents can be found. Hence the process variables make it possible to specify and reason about what are often referred to as contexts, environments, and partial implementations. As reductions are algorithms that work on syntax, they can be considered as forming a bridge between traditional non-compositional model checking and compositional proof systems.

Recommendations

• scientific article; zbMATH DE number 4180789
• scientific article; zbMATH DE number 1522998
• scientific article; zbMATH DE number 4060694
• scientific article; zbMATH DE number 3905833
• Compositionality in state space verification methods

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• A linear algorithm to solve fixed-point equations on transition systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• CTL^* and ECTL^* as fragments of the modal -calculus
• scientific article; zbMATH DE number 4131643 (Why is no real title available?)
• scientific article; zbMATH DE number 4056971 (Why is no real title available?)
• scientific article; zbMATH DE number 177838 (Why is no real title available?)
• Tableau-based model checking in the propositional mu-calculus

Cited in

(8)

• A compositional -calculus proof system for statecharts processes
• Model checking and boolean graphs
• Complete proof systems for weighted modal logic
• Logical vs. behavioural specifications
• Compositional verification of asynchronous concurrent systems using CADP
• Compositionality of Hennessy-Milner logic by structural operational semantics
• Temporal logic and categories of Petri nets
• Abstract satisfaction

This page was built for publication: Compositional checking of satisfaction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685107)