Proving the validity of equations in GSOS languages using rule-matching bisimilarity

DOI10.1017/S0960129511000417zbMath1248.68347MaRDI QIDQ2883120

Luca Aceto, Anna Ingólfsdóttir, Matteo Cimini

Publication date: 11 May 2012

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

process algebrastructural operational semanticsbisimulation

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• A syntactic commutativity format for SOS
• SOS formats and meta-theory: 20 years after
• A complete inference system for a class of regular behaviours
• Higher-level synchronising devices in Meije-SCCS
• Structured operational semantics and bisimulation as a congruence
• An algebra for process creation
• A conservative look at operational semantics with variable binding
• Turning SOS rules into equations
• Bisimilarity of open terms.
• Axiomatizing GSOS with termination
• Compositionality of Hennessy-Milner logic by structural operational semantics
• Automating Soundness Proofs
• Rule Formats for Determinism and Idempotence
• A Rule Format for Unit Elements
• A Rule Format for Associativity
• Laws of programming
• Algebraic laws for nondeterminism and concurrency
• Compositionality Through an Operational Semantics of Contexts
• Process Algebra
• Bisimulation can't be traced
• Precongruence formats for decorated trace semantics

This page was built for publication: Proving the validity of equations in GSOS languages using rule-matching bisimilarity