A rewriting strategy to verify observational congruence

DOI10.1016/0020-0190(90)90023-QMaRDI QIDQ915472zbMATH OpenOpenAlexFDO

Authors P. 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

behavioural equivalencescompletionconcurrencydivergencenormal formspecification languageterm rewriting system

Mathematics Subject Classification ID

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

Recommendations

• Deciding observational congruence of finite-state CCS expressions by rewriting
• Rewriting approximations for properties verification over CCS specifications
• scientific article; zbMATH DE number 4085007
• scientific article; zbMATH DE number 3878352
• A modal characterization of observational congruence on finite terms of CCS

Cites work

• A calculus of communicating systems
• Algebraic laws for nondeterminism and concurrency
• Complete Sets of Reductions for Some Equational Theories
• Completion for rewriting modulo a congruence
• Completion of a Set of Rules Modulo a Set of Equations
• scientific article; zbMATH DE number 3986627 (Why is no real title available?)
• scientific article; zbMATH DE number 4074464 (Why is no real title available?)
• scientific article; zbMATH DE number 4085007 (Why is no real title available?)
• Termination orderings for associative-commutative rewriting systems

Cited in

(7)

• Complete sets of axioms for finite basic LOTOS behavioural equivalences
• Rewriting approximations for properties verification over CCS specifications
• A strategy to deal with divergent rewrite systems
• An automated proof technique for finite-state machine equivalence
• Mechanizing a proof by induction of process algebra specifications in higher order logic
• Infinite normal forms for non-linear term rewriting systems
• Deciding observational congruence of finite-state CCS expressions by rewriting

Describes a project that uses

Uses Software

• REVE

This page was built for publication: A rewriting strategy to verify observational congruence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q915472)