Is observational congruence on \(\mu \)-expressions axiomatisable in equational Horn logic?

DOI10.1016/j.ic.2009.05.005zbMath1205.68248OpenAlexW2076739792MaRDI QIDQ979076

Michael Mendler, Gerald Lüttgen

Publication date: 25 June 2010

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

Full work available at URL: https://doi.org/10.1016/j.ic.2009.05.005

zbMATH Keywords

process algebraHorn logicobservational congruence\(\mu \)-expressionsfinite axiomatisation

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Non-deterministic structures of computation ⋮ Denotational fixed-point semantics for constructive scheduling of synchronous concurrency

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A complete axiomatization of timed bisimulation for a class of timed regular behaviours
• A complete inference system for a class of regular behaviours
• A complete axiomatisation for observational congruence of finite-state behaviours
• A completeness theorem for Kleene algebras and the algebra of regular events
• A complete equational axiomatization for prefix iteration
• Nonaxiomatisability of equivalences over finite state processes
• Completeness of Park induction
• CCS with Hennessy's merge has no finite-equational axiomatization
• Process algebra with timing
• Axiomatizing prefix iteration with silent steps
• Higher-order Horn clauses
• On the Axiomatizability of Priority
• Impossibility Results for the Equational Theory of Timed CCS
• An Equational Axiomatization of Bisimulation over Regular Expressions
• ITERATION ALGEBRAS
• Two Complete Axiom Systems for the Algebra of Regular Events
• On Finite Alphabets and Infinite Bases III: Simulation
• A fully abstract denotational model for observational precongruence

This page was built for publication: Is observational congruence on \(\mu \)-expressions axiomatisable in equational Horn logic?