Finite axiom systems for testing preorder and De Simone process languages

DOI10.1016/S0304-3975(99)00214-5zbMath0944.68125WikidataQ114012739 ScholiaQ114012739MaRDI QIDQ1575273

Irek Ulidowski

Publication date: 21 August 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

equational logictesting semanticscomplete axiomatisationsDe Simone process languagesstructured operational semantics (SOS)

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Axiomatizing GSOS with termination ⋮ Process languages with discrete relative time based on the ordered SOS format and rooted eager bisimulation ⋮ A syntactic commutativity format for SOS ⋮ SOS formats and meta-theory: 20 years after ⋮ Ensuring liveness properties of distributed systems: open problems ⋮ A precongruence format for should testing preorder ⋮ Automating Soundness Proofs ⋮ Generating priority rewrite systems for OSOS process languages ⋮ Finite axiom systems for testing preorder and De Simone process languages ⋮ Ordered SOS process languages for branching and eager bisimulations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Observation equivalence as a testing equivalence
• Structural operational semantics for weak bisimulations
• Transition system specifications with negative premises
• Bisimulation and divergence
• Priorities in process algebras
• A complete inference system for a class of regular behaviours
• Algebra of communicating processes with abstraction
• Higher-level synchronising devices in Meije-SCCS
• Extensional equivalences for transition systems
• Structured operational semantics and bisimulation as a congruence
• A complete axiomatisation for observational congruence of finite-state behaviours
• Turning SOS rules into equations
• Testing equivalences for processes
• Finite axiom systems for testing preorder and De Simone process languages
• Ordered SOS process languages for branching and eager bisimulations
• CPO models for compact GSOS languages
• Process algebra for synchronous communication
• Process Algebra
• Bisimulation can't be traced