Turning SOS rules into equations

DOI10.1006/INCO.1994.1040zbMath0822.68059OpenAlexW2105135809MaRDI QIDQ1327393

Bard Bloom, Luca Aceto, Frits W. Vaandrager

Publication date: 19 June 1994

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

Full work available at URL: http://dare.uva.nl/personal/pure/en/publications/turning-sos-rules-into-equations(e53e57c4-f362-4f0f-bd42-47d25ca5bdd6).html

zbMATH Keywords

structural operational semantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (46)

Modal logic and the approximation induction principle ⋮ Proving the validity of equations in GSOS languages using rule-matching bisimilarity ⋮ GSOS and finite labelled transition systems ⋮ Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS ⋮ Axiomatizing GSOS with termination ⋮ Process languages with discrete relative time based on the ordered SOS format and rooted eager bisimulation ⋮ The Equational Theory of Weak Complete Simulation Semantics over BCCSP ⋮ A format for semantic equivalence comparison ⋮ A syntactic commutativity format for SOS ⋮ Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition? ⋮ A \(\pi\)-calculus with explicit substitutions ⋮ SOS formats and meta-theory: 20 years after ⋮ SOS specifications for uniformly continuous operators ⋮ An algebraic framework for developing and maintaining real-time systems ⋮ A Calculus of Countable Broadcasting Systems ⋮ CPO models for a class of GSOS languages ⋮ A π-calculus with explicit substitutions: The late semantics ⋮ A process algebra of communicating shared resources with dense time and priorities ⋮ A general conservative extension theorem in process algebras with inequalities ⋮ An axiomatic semantics for the synchronous language Gentzen. ⋮ Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction ⋮ DyNetKAT: an algebra of dynamic networks ⋮ Rule formats for determinism and idempotence ⋮ SOS rule formats for idempotent terms and idempotent unary operators ⋮ Compositional bisimulation metric reasoning with Probabilistic Process Calculi ⋮ Compositional semantics and behavioral equivalences for P systems ⋮ Compositional Abstraction in Real-Time Model Checking ⋮ Axiomatizing weak simulation semantics over BCCSP ⋮ Structural operational semantics for weak bisimulations ⋮ Towards general axiomatizations for bisimilarity and trace semantics ⋮ Embedding Untimed into Timed Process Algebra; the Case for Explicit Termination ⋮ Rule formats for distributivity ⋮ CCS with Hennessy's merge has no finite-equational axiomatization ⋮ Notions of bisimulation and congruence formats for SOS with data ⋮ On cool congruence formats for weak bisimulations ⋮ From rewrite rules to bisimulation congruences ⋮ Explicit substitutions for \(\pi\)-congruences ⋮ An axiomatic semantics for Esterel ⋮ Generating priority rewrite systems for OSOS process languages ⋮ Axiomatizing Weak Ready Simulation Semantics over BCCSP ⋮ Finite axiom systems for testing preorder and De Simone process languages ⋮ Compositional weak metrics for group key update ⋮ Dynamic structural operational semantics ⋮ Tile formats for located and mobile systems. ⋮ Ordered SOS process languages for branching and eager bisimulations ⋮ A Calculus for Team Automata

This page was built for publication: Turning SOS rules into equations