Graphical versus logical specifications

DOI10.1016/0304-3975(92)90276-LzbMath0776.68084MaRDI QIDQ685358

Gérard Boudol, Kim Guldstrand Larsen

Publication date: 25 October 1993

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

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)

Related Items

Characteristic formulae for fixed-point semantics: a general framework, A Pre-congruence Format for XY-simulation, Extending modal transition systems with structured labels, ACTL for modal interface automata, Conjunction on processes: Full abstraction via ready-tree semantics, Reducing behavioural to structural properties of programs with procedures, When Are Prime Formulae Characteristic?, When are prime formulae characteristic?, Specification of communicating processes: temporal logic versus refusals-based refinement, Compositional verification of sequential programs with procedures, CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties, Compositionality for quantitative specifications, A linear-time-branching-time spectrum for behavioral specification theories, Logical vs. behavioural specifications, Encoding safety in \(\mathrm{CLL}_R\), Reasoning about nondeterministic and concurrent actions: A process algebra approach, Refinement checking on parametric modal transition systems

Cites Work

• Modal logics for communicating systems
• A logic for the description of non-deterministic programs and their properties
• Algebraic laws for nondeterminism and concurrency
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item