Graphical versus logical specifications

DOI10.1016/0304-3975(92)90276-LMaRDI QIDQ685358zbMATH OpenFDO

Authors Gérard Boudol, Kim G. Larsen

Publication date 25 October 1993

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(92)90276-L

zbMATH Keywords

Hennessy-Milner logicLarsen-Thomsen's modal transition systemsverification of concurrent systems

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 125881
• Labelled transition logic: An outline
• Logical vs. behavioural specifications
• Process specification and verification
• Publication:5753511

Cites work

• scientific article; zbMATH DE number 3919813 (Why is no real title available?)
• scientific article; zbMATH DE number 4059362 (Why is no real title available?)
• scientific article; zbMATH DE number 3744561 (Why is no real title available?)
• scientific article; zbMATH DE number 4118343 (Why is no real title available?)
• A logic for the description of non-deterministic programs and their properties
• Algebraic laws for nondeterminism and concurrency
• Modal logics for communicating systems

Cited in

(23)

• Reasoning about nondeterministic and concurrent actions: A process algebra approach
• When are prime formulae characteristic?
• Compositional verification of sequential programs with procedures
• Conjunction on processes: Full abstraction via ready-tree semantics
• Characteristic formulae for fixed-point semantics: a general framework
• ACTL for modal interface automata
• scientific article; zbMATH DE number 176735 (Why is no real title available?)
• Refinement checking on parametric modal transition systems
• Algebraic Methodology and Software Technology
• Extending modal transition systems with structured labels
• Encoding safety in \(\mathrm{CLL}_R\)
• Logical vs. behavioural specifications
• Specification of communicating processes: temporal logic versus refusals-based refinement
• A pre-congruence format for XY-simulation
• Process specification and verification
• Diagrammatic specifications
• The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum
• A linear-time-branching-time spectrum for behavioral specification theories
• Compositionality for quantitative specifications
• CVPP: a tool set for compositional verification of control-flow safety properties
• When are prime formulae characteristic?
• Reducing behavioural to structural properties of programs with procedures
• scientific article; zbMATH DE number 125881 (Why is no real title available?)

This page was built for publication: Graphical versus logical specifications

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