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

DOI10.1016/j.ic.2009.05.005zbMath1205.68248MaRDI 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 algebra; Horn logic; observational congruence; \(\mu \)-expressions; finite axiomatisation

Mathematics Subject Classification ID

68T27: Logic in artificial intelligence

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Related Items

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