Research Paper #905
|Title:||Observant: an Annotated Term-Rewriting System for Deciding Observation Congruence|
|Authors:||Monroy-Borja,R; Bundy,A; Green,I|
|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.
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.