Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS

DOI10.1016/j.jlap.2004.03.004zbMath1072.68070OpenAlexW2135333778MaRDI QIDQ1878715

Alex K. Simpson

Publication date: 8 September 2004

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2004.03.004

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (7)

Compositionality of Hennessy-Milner logic by structural operational semantics ⋮ SOS formats and meta-theory: 20 years after ⋮ Unnamed Item ⋮ Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap ⋮ When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus ⋮ A general account of coinduction up-to ⋮ Bialgebraic methods and modal logic in structural operational semantics

Uses Software

• SLMC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modal logics for communicating systems
• Results on the propositional \(\mu\)-calculus
• Local model checking in the modal mu-calculus
• Turning SOS rules into equations
• Proving properties of dynamic process networks
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• Decidability of model checking for infinite-state concurrent systems
• A modal characterization of observational congruence on finite terms of CCS
• Algebraic laws for nondeterminism and concurrency
• Bisimulation can't be traced
• On global induction mechanisms in aμ-calculus with explicit approximations
• -Calculus with Explicit Points and Approximations

This page was built for publication: Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS