Compositionality of Hennessy-Milner logic by structural operational semantics

DOI10.1016/j.tcs.2005.11.035zbMath1088.68094OpenAlexW2116862465MaRDI QIDQ2368979

Paulien de Wind, Robert J. van Glabbeek, W. J. Fokkink

Publication date: 28 April 2006

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.11.035

zbMATH Keywords

Modal logicCongruenceStructural operational semanticsCompositional proof systemntyft/ntyxt format

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (20)

Proving the validity of equations in GSOS languages using rule-matching bisimilarity ⋮ Compositional Reasoning for Multi-modal Logics ⋮ A Pre-congruence Format for XY-simulation ⋮ Unnamed Item ⋮ SOS formats and meta-theory: 20 years after ⋮ SOS specifications for uniformly continuous operators ⋮ Divide and congruence. II: From decomposition of modal formulas to preservation of delay and weak bisimilarity ⋮ Congruence from the operator's point of view. Syntactic requirements on modal characterizations ⋮ Characteristic invariants in Hennessy-Milner logic ⋮ Logical characterisations, rule formats and compositionality for input-output conformance simulation ⋮ Divide and congruence: from decomposition of modal formulas to preservation of branching and \(\eta \)-bisimilarity ⋮ Logical Characterisations and Compositionality of Input-Output Conformance Simulation ⋮ Compositional bisimulation metric reasoning with Probabilistic Process Calculi ⋮ Verification of asynchronous systems with an unspecified component ⋮ Probabilistic divide \& congruence: branching bisimilarity ⋮ On the expressibility of priority ⋮ Unnamed Item ⋮ Logical vs. behavioural specifications ⋮ Coverability Synthesis in Parametric Petri Nets ⋮ Dynamic structural operational semantics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modal logics for communicating systems
• Compositional checking of satisfaction
• Transition system specifications with negative premises
• Results on the propositional \(\mu\)-calculus
• Calculi for synchrony and asynchrony
• A proof-theoretic characterization of observational equivalence
• Higher-level synchronising devices in Meije-SCCS
• The temporal semantics of concurrent programs
• A calculus of communicating systems
• Process logic: Expressiveness, decidability, completeness
• CONCUR '90. Theories of concurrency: unification and extension. Amsterdam, The Netherlands, August 1990. Proceedings
• Structured operational semantics and bisimulation as a congruence
• The meaning of negative premises in transition system specifications. II
• Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
• A structural approach to operational semantics
• \(Ntyft/ntyxt\) rules reduce to \(n\)tree rules
• The power of the future perfect in program logics
• A Theory of Communicating Sequential Processes
• Algebraic laws for nondeterminism and concurrency
• Compositionality Through an Operational Semantics of Contexts
• Bisimulation can't be traced
• The meaning of negative premises in transition system specifications
• Precongruence formats for decorated trace semantics
• Fundamentals of Computation Theory

This page was built for publication: Compositionality of Hennessy-Milner logic by structural operational semantics