Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation

We present a method for decomposing modal formulas for processes with the internal action τ. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra. We use this decomposition method to derive congruence formats for branching and rooted branching bisimulation equivalence.

• Publication year

  2005

• Venue

  Formal Methods for Components and Objects

• Publication date

  2005-11-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/11804192_10
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Compositionality of Hennessy-Milner logic by structural operational semantics

  2006cited by this paper
• Divide and Congruence Applied to η-Bisimulation

  2006cited by this paper
• Divide and Congruence Applied to eta-Bisimulation

  2006cited by this paper
• The origins of structural operational semantics

  2004cited by this paper
• A structural approach to operational semantics

  2004cited by this paper
• Precongruence formats for decorated trace semantics

  2002influential reference
• Rooted Branching Bisimulation as a Congruence

  2000influential reference
• The meaning of negative premises in transition system specifications II

  1996cited by this paper
• Ntyft/Ntyxt Rules Reduce to Ntree Rules

  1996cited by this paper
• Branching time and abstraction in bisimulation semantics

  1996influential reference
• Structural Operational Semantics for Weak Bisimulations

  1995cited by this paper
• Bisimulation can't be traced

  1995cited by this paper
• The Linear Time - Branching Time Spectrum II

  1993cited by this paper
• The Linear Time - Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves

  1993cited by this paper
• Structured Operational Semantics and Bisimulation as a Congruence

  1992influential reference
• The meaning of negative premises in transition system specifications

  1991cited by this paper
• Transition System Specifications with Negative Premises

  1991cited by this paper
• Transition System Specifications with Negative Premises

  1990cited by this paper
• Compositionality through an Operational Semantics of Contexts

  1990cited by this paper
• Three logics for branching bisimulation

  1990cited by this paper
• Algebraic laws for nondeterminism and concurrency

  1985cited by this paper
• Higher-Level Synchronising Devices in Meije-SCCS

  1985cited by this paper
• Process Algebra for Synchronous Communication

  1984cited by this paper
• Representation of Events in Nerve Nets and Finite Automata

  1951cited by this paper

• Characteristic invariants in Hennessy–Milner logic

  2020cites this paper
• Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence

  2019cites this paper
• 11 : 2 Divide and Congruence III : Stability &

  2017cites this paper
• Divide and Congruence III: Stability & Divergence

  2017cites this paper
• Robust SOS Specifications of Probabilistic Processes

  2015cites this paper
• Fixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators

  2014cites this paper
• Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity

  2012cites this paper
• Congruence Formats for Weak Readiness Equivalence and Weak Possible Future Equivalence

  2010cites this paper
• A precongruence format for should testing preorder

  2010cites this paper
• Notes on Generative Probabilistic Bisimulation

  2007cites this paper
• Notes on Generative Probabilistic Bisimulation

  2006cites this paper
• On cool congruence formats for weak bisimulations

  2005cites this paper