Compositional checking of satisfaction (Q685107): Difference between revisions
From MaRDI portal
Set profile property. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Automatic verification of finite-state concurrent systems using temporal logic specifications / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3792217 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3033311 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Tableau-based model checking in the propositional mu-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A linear algorithm to solve fixed-point equations on transition systems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4038716 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A lattice-theoretical fixpoint theorem and its applications / rank | |||
Normal rank |
Latest revision as of 10:28, 22 May 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
0 references