The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #905

Title:Observant: an Annotated Term-Rewriting System for Deciding Observation Congruence
Authors:Monroy-Borja,R; Bundy,A; Green,I
Date:Apr 1998
Presented:Submitted to ECAI98
Keywords:term-rewriting systems, annotated trss, ccs
Abstract:The use of term-rewriting systems (TRSs) is at the heart of automa-
ted theorem proving (ATP). There are a number of methods whereby we
can build terminating TRSs with full deduction power and termination.
One such theory is the theory of observation congruence in CCS[9].
One approach to overcome the problem is to use heuristic to control
search; it, however, introduces the problem of finding and capturing
such meta-level control. This paper advocates the use of annotated
TRSs (ATRSs) to tachle such problems. Annotations are used to capture
meta-level information that helps direct proof search; they give an
intuitive account of why and how rewriting is expected to work. We
introduce an ATRS called Observant and show how it can be used to
build a decision procedure for observation congruence in CCS; furth-
ermore, Observant can be used to prove CCS equations involving finite-
state systems and infinite-state systems. We prove Observant terminating,
sound, and complete - over the normalisation of finite processes, and so
argue that Observant surpasses rival term-rewriting strategies.

[Search These Pages] [DAI Home Page] [Comment]