A refinement calculus for specifications in Hennessy-Milner logic with recursion

DOI10.1007/BF01887208zbMath0696.68037MaRDI QIDQ911261

Sören Holmström

Publication date: 1989

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

refinementconcurrencyspecification languageCCSHennessy-Milner Logicspecification and verification of processes

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25) Theory of software (68N99)

Related Items

Conjunction on processes: Full abstraction via ready-tree semantics ⋮ A functional programming approach to the specification and verification of concurrent systems ⋮ Local model checking in the modal mu-calculus ⋮ Parametric and Quantitative Extensions of Modal Transition Systems

Cites Work

• Calculi for synchrony and asynchrony
• A proof-theoretic characterization of observational equivalence
• A calculus of communicating systems
• A lattice-theoretical fixpoint theorem and its applications
• Algebraic laws for nondeterminism and concurrency
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item