Branching time and abstraction in bisimulation semantics

DOI10.1145/233551.233556zbMath0882.68085OpenAlexW1985161650MaRDI QIDQ4371679

W. P. Weijland, Robert J. van Glabbeek

Publication date: 21 January 1998

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/5564

zbMATH Keywords

comparative concurrency semantics

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (only showing first 100 items - show all)

Process languages with discrete relative time based on the ordered SOS format and rooted eager bisimulation ⋮ When is partial trace equivalence adequate? ⋮ Model independent approach to probabilistic models ⋮ Timed process calculi with deterministic or stochastic delays: commuting between durational and durationless actions ⋮ Branching time and orthogonal bisimulation equivalence ⋮ Bisimulation maps in presheaf categories ⋮ Operational semantics for Petri net components ⋮ Focus points and convergent process operators: A proof strategy for protocol verification ⋮ Formal modelling and verification of GALS systems using GRL and CADP ⋮ Branching bisimilarity is an equivalence indeed! ⋮ Priority and abstraction in process algebra ⋮ Compositional verification of concurrent systems by combining bisimulations ⋮ Cones and foci: A mechanical framework for protocol verification ⋮ Comparative branching-time semantics for Markov chains ⋮ Preferential choice and coordination conditions ⋮ Probabilistic bisimulation for realistic schedulers ⋮ A generic framework for checking semantic equivalences between pushdown automata and finite-state automata ⋮ A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences ⋮ Divide and congruence. II: From decomposition of modal formulas to preservation of delay and weak bisimilarity ⋮ Out for coffee: with Rob ⋮ All congruences below stability-preserving fair testing or CFFD ⋮ Coupled similarity: the first 32 years ⋮ On the probabilistic bisimulation spectrum with silent moves ⋮ A linear-time branching-time perspective on interface automata ⋮ Characteristic invariants in Hennessy-Milner logic ⋮ A complete axiomatization of weighted branching bisimulation ⋮ Reactive Turing machines ⋮ A general conservative extension theorem in process algebras with inequalities ⋮ Process algebra with propositional signals ⋮ Process algebra with language matching ⋮ Two finite specifications of a queue ⋮ Application of static analyses for state-space reduction to the microcontroller binary code ⋮ Modeling and efficient verification of wireless ad hoc networks ⋮ Distinguishing and relating higher-order and first-order processes by expressiveness ⋮ External equality and absolute equality coincide in finite CCS and \(\pi\) calculus without summation ⋮ Taming Dr. Frankenstein: contract-based design for cyber-physical systems ⋮ Unique parallel decomposition in branching and weak bisimulation semantics ⋮ Divide and congruence: from decomposition of modal formulas to preservation of branching and \(\eta \)-bisimilarity ⋮ Characterisations of testing preorders for a finite probabilistic \(\pi\)-calculus ⋮ Towards a process calculus for REST: current state of the art ⋮ Reusing artifact-centric business process models: a behavioral consistent specialization approach ⋮ Cartesian difference categories ⋮ Automated temporal equilibrium analysis: verification and synthesis of multi-player games ⋮ On hierarchically developing reactive systems ⋮ A polynomial \(\lambda\)-bisimilar normalization for reset Petri nets ⋮ Team equivalences for finite-state machines with silent moves ⋮ Generalizing the Paige-Tarjan algorithm by abstract interpretation ⋮ Axiomatizing weak simulation semantics over BCCSP ⋮ On the tradeoff between compositionality and exactness in weak bisimilarity for integrated-time Markovian process calculi ⋮ Rooted branching bisimulation as a congruence ⋮ Team bisimilarity, and its associated modal logic, for BPP nets ⋮ Extensional Petri net ⋮ Deciding orthogonal bisimulation ⋮ Infinite normal forms for non-linear term rewriting systems ⋮ Polynomial time decision algorithms for probabilistic automata ⋮ Structural operational semantics for weak bisimulations ⋮ Deciding observational congruence of finite-state CCS expressions by rewriting ⋮ Observational structures and their logic ⋮ Confluence reduction for Markov automata ⋮ Computing maximal weak and other bisimulations ⋮ A formal verification technique for behavioural model-to-model transformations ⋮ Universal extensions to simulate specifications ⋮ A general account of coinduction up-to ⋮ Refinement of actions in event structures and causal trees ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ On the expressiveness of interaction ⋮ Decidability of branching bisimulation on normed commutative context-free processes ⋮ Soundness of workflow nets: classification, decidability, and analysis ⋮ Simulation refinement for concurrency verification ⋮ Dynamic consistency in process algebra: from paradigm to ACP ⋮ On cool congruence formats for weak bisimulations ⋮ On the computational complexity of bisimulation, redux ⋮ Ensuring liveness properties of distributed systems: open problems ⋮ Branching bisimulation for probabilistic systems: characteristics and decidability ⋮ Divide and congruence. III: From decomposition of modal formulas to preservation of stability and divergence ⋮ Encapsulating deontic and branching time specifications ⋮ Verification of reactive systems via instantiation of parameterised Boolean equation systems ⋮ A brief history of process algebra ⋮ A general approach to comparing infinite-state systems with their finite-state specifications ⋮ Modular specification of process algebras ⋮ Open maps in concrete categories and branching bisimulation for prefix orders ⋮ A study on team bisimulation and H-team bisimulation for BPP nets ⋮ A thesis for interaction ⋮ Process calculus based upon evaluation to committed form ⋮ Probabilistic weak simulation is decidable in polynomial time ⋮ Game-theoretic simulation checking tool ⋮ Branching bisimulation congruence for probabilistic systems ⋮ Bisimilarity on basic parallel processes ⋮ Conduché property and tree-based categories ⋮ The compression structure of a process ⋮ Raiders of the lost equivalence: probabilistic branching bisimilarity ⋮ Absolute versus relative time in process algebras. ⋮ Vertical implementation ⋮ Ordered SOS process languages for branching and eager bisimulations ⋮ Axiomatising divergence ⋮ Compositional verification of asynchronous concurrent systems using CADP ⋮ The cones and foci proof technique for timed transition systems ⋮ Next-preserving branching bisimulation ⋮ Branching place bisimilarity: a decidable behavioral equivalence for finite Petri nets with silent moves ⋮ Translating Java for multiple model checkers: The Bandera back-end

This page was built for publication: Branching time and abstraction in bisimulation semantics