A rewriting strategy to verify observational congruence

DOI10.1016/0020-0190(90)90023-QzbMath0702.68074OpenAlexW2021553745MaRDI QIDQ915472

Paola Inverardi, Monica Nesi

Publication date: 1990

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(90)90023-q

zbMATH Keywords

normal formcompletiondivergencebehavioural equivalencesconcurrencyspecification languageterm rewriting system

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Thue and Post systems, etc. (03D03)

Related Items

A strategy to deal with divergent rewrite systems ⋮ Infinite normal forms for non-linear term rewriting systems ⋮ Deciding observational congruence of finite-state CCS expressions by rewriting ⋮ Complete sets of axioms for finite basic LOTOS behavioural equivalences

Uses Software

• REVE

Cites Work

• Termination orderings for associative-commutative rewriting systems
• A calculus of communicating systems
• Completion for rewriting modulo a congruence
• Algebraic laws for nondeterminism and concurrency
• Completion of a Set of Rules Modulo a Set of Equations
• Complete Sets of Reductions for Some Equational Theories
• Unnamed Item
• Unnamed Item
• Unnamed Item