Compositional checking of satisfaction (Q685107): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 01:58, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Compositional checking of satisfaction |
scientific article |
Statements
Compositional checking of satisfaction (English)
0 references
30 September 1993
0 references
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.
0 references
process calculi
0 references
compositionality
0 references
modal \(\mu\)-calculus
0 references
model checking
0 references