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. |
Download: | POSTSCRIPT COPY |