Compositionality of Hennessy-Milner logic by structural operational semantics

DOI10.1016/J.TCS.2005.11.035MaRDI QIDQ2368979zbMATH OpenOpenAlexFDO

Authors Paulien de Wind, Wan Fokkink, Rob van Glabbeek

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

Compositional proof systemCongruenceModal logicntyft/ntyxt formatStructural operational semantics

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)

Recommendations

• Compositionality of Hennessy-Milner logic through structural operational semantics.
• Compositionality of Probabilistic Hennessy-Milner Logic through Structural Operational Semantics
• Precongruence formats with lookahead through modal decomposition
• Decompositional reasoning about the history of parallel processes
• Divide and congruence: from decomposition of modal formulas to preservation of branching and -bisimilarity

Cites work

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

Cited in

(25)

• SOS specifications for uniformly continuous operators
• Divide and congruence. II: From decomposition of modal formulas to preservation of delay and weak bisimilarity
• Verification of asynchronous systems with an unspecified component
• Probabilistic divide \& congruence: branching bisimilarity
• Congruence from the operator's point of view. Syntactic requirements on modal characterizations
• Characteristic invariants in Hennessy-Milner logic
• Logical vs. behavioural specifications
• Dynamic structural operational semantics
• Logical characterisations, rule formats and compositionality for input-output conformance simulation
• Proving the validity of equations in GSOS languages using rule-matching bisimilarity
• Decompositional reasoning about the history of parallel processes
• Compositionality of Probabilistic Hennessy-Milner Logic through Structural Operational Semantics
• Logical characterisations and compositionality of input-output conformance simulation
• Compositional bisimulation metric reasoning with Probabilistic Process Calculi
• Compositional reasoning for multi-modal logics
• A pre-congruence format for XY-simulation
• Divide and congruence: from decomposition of modal formulas to preservation of branching and -bisimilarity
• SOS-based modal decomposition on nondeterministic probabilistic processes
• Rule formats for nominal process calculi
• Precongruence formats with lookahead through modal decomposition
• Rule formats for nominal process calculi
• Compositionality of Hennessy-Milner logic through structural operational semantics.
• Logical characterization of bisimulation metrics
• SOS formats and meta-theory: 20 years after
• On the expressibility of priority

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

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