A complete axiomatisation for observational congruence of finite-state behaviours

DOI10.1016/0890-5401(89)90070-9zbMath0688.68050OpenAlexW2022258624MaRDI QIDQ1263984

Publication date: 1989

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/15164645/A_Complete_Axiomatisation_for_Observational_Congruence_of_Finite_State_Behaviors.pdf

zbMATH Keywords

bisimulation guarded expressions transition diagrams (charts)

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Abstract data types; algebraic specification (68Q65) Software, source code, etc. for problems pertaining to systems and control theory (93-04)

Related Items

Morphisms and Minimisation of Weighted Automata ⋮ A complete axiomatisation for trace congruence of finite state behaviors ⋮ The Equational Theory of Weak Complete Simulation Semantics over BCCSP ⋮ Tau laws for pi calculus ⋮ Axiomatising infinitary probabilistic weak bisimilarity of finite-state behaviours ⋮ Priority and abstraction in process algebra ⋮ An equational axiomatization for multi-exit iteration ⋮ A complete axiomatization of finite-state ACSR processes ⋮ Nonaxiomatisability of equivalences over finite state processes ⋮ Axiomatizations for probabilistic finite-state behaviors ⋮ A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences ⋮ Unnamed Item ⋮ A complete axiomatization of weighted branching bisimulation ⋮ A process algebra of communicating shared resources with dense time and priorities ⋮ The equational logic of fixed points ⋮ Axiomatizing flat iteration ⋮ Axiomatizing Lüttgen \& Vogler's ready simulation for finite processes in \(\mathrm{CLL}_{R}\) ⋮ Rooted divergence-preserving branching bisimilarity is a congruence: a simpler proof ⋮ Theory of interaction ⋮ An algebra of behavioural types ⋮ Reactive bisimulation semantics for a process algebra with timeouts ⋮ Probabilistic weak bisimulation and axiomatization for probabilistic models ⋮ Unnamed Item ⋮ Iteration Semirings ⋮ Team equivalences for finite-state machines with silent moves ⋮ Axiomatizing weak simulation semantics over BCCSP ⋮ A ground-complete axiomatisation of finite-state processes in a generic process algebra ⋮ Up-to Techniques for Branching Bisimilarity ⋮ Inference systems for observation equivalences in the \(\pi\)-calculus ⋮ A complete axiomatization of timed bisimulation for a class of timed regular behaviours ⋮ Infinite normal forms for non-linear term rewriting systems ⋮ Structural operational semantics for weak bisimulations ⋮ Deciding observational congruence of finite-state CCS expressions by rewriting ⋮ Process calculi as a tool for studying coordination, contracts and session types ⋮ CCS with priority guards ⋮ Unnamed Item ⋮ Causal Semantics for BPP Nets with Silent Moves ⋮ Deciding bisimilarity is P-complete ⋮ Tree Process Calculus ⋮ Multi-Linear Iterative K-Σ-Semialgebras ⋮ Non-deterministic structures of computation ⋮ On recursive operations over logic LTS ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ On quasi-open bisimulation ⋮ Is observational congruence on \(\mu \)-expressions axiomatisable in equational Horn logic? ⋮ On timed alternating simulation for concurrent timed games ⋮ On Finite Bases for Weak Semantics: Failures Versus Impossible Futures ⋮ Unnamed Item ⋮ Explicit substitutions for \(\pi\)-congruences ⋮ Equations, Contractions, and Unique Solutions ⋮ Unnamed Item ⋮ Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations. ⋮ Axiomatizing Weak Ready Simulation Semantics over BCCSP ⋮ Finite axiom systems for testing preorder and De Simone process languages ⋮ The Value-Passing Calculus ⋮ Understanding the mismatch combinator in chi calculus ⋮ Axiomatising divergence ⋮ Expressing Priorities and External Probabilities in Process Algebra via Mixed Open/Closed Systems ⋮ A Generic Process Algebra ⋮ Extensions of Standard Weak Bisimulation Machinery: Finite-state General Processes, Refinable Actions, Maximal-progress and Time ⋮ The theory of interactive generalized semi-Markov processes ⋮ Hiding resources that can fail: An axiomatic perspective ⋮ Control of discrete-event systems with partial observations using coalgebra and coinduction

Cites Work