# DIET: Developing Implementation and Extending Theory A Symbolic Approach to Reasoning about LOTOS

## Project Achievements

The focus for this project was to build up a symbolic framework for reasoning about LOTOS. This framework pictured below is based around a symbolic semantics for Full LOTOS (see the AMAST 1997 paper and the FORTE 2001 paper) using Symbolic Transition Systems (STS) as defined by Hennessy and Lin. It also includes an HML-like logic (FULL) (see the Computer Journal paper) and symbolic bisimulation (see the FORTE 2001 paper and the Glasgow and Stirling technical reports). Although we focus on the use of LOTOS as a specification language, any similar process algebra can be represented in a symbolic framework.

In this project our key advances are:

Proof of the relation between symbolic and standard bisimulation
LOTOS is a standardised language, therefore it is important that the meaning of the semantics is retained while gaining the benefit of a more convenient compact notation using symbolic transition systems. This result means that if two closed processes are bisimilar under the standard bisimulation relation, then they are bisimilar under symbolic bisimulation (this will be reported in a later paper). This relation is shown by the heavy arrow in the framework picture.
Proof of adequacy of FULL with respect to symbolic bisimulation
This result shows that if two processes are bisimilar then they satisfy the same logical properties (see the Computer Journal paper and the FME 2001 paper). Conversely, if the processes are not bisimilar then there is a logical property which captures the difference between them. This is an important result because it shows that our symbolic framework is self-consistent in this sense. The logic differentiates exactly the same sets of processes as the bisimulation relation. This result is represented by the dashed arrows in framework picture.
Three prototype model checking tools for the logic
The three tools are built on top of existing tools, and all exploit different paradigms. The first (see the Bryans and Shankland FORTE 2001 paper) is built on top of CADP, and is useful because although the semantics in this case is not really symbolic, our tool can be part of an established suite of tools for reasoning about LOTOS specifications. The second (see the Robinson/Shankland AVIS paper) is built on top of the theorem prover Ergo. This implements a truly symbolic semantics, and gives access to theorem proving tactics for reasoning about the data part of specifications. The third (see the Bryans/Verdejo/Shankland AVIS paper) is built in a term rewriting system Maude. This also implements a symbolic semantics, and gives access to term rewriting techniques for dealing with data.
Extended version of FULL
The FULL logic has some nice theoretical properties, described above; however, for practical specification purposes a more expressive logic is required. A particular flaw in FULL is the inability to describe properties with loops. FULL* (a forthcoming paper by Bryans/Morel/Shankland will detail this) is an extended version of FULL which can describe such properties. Prototype implementation has been carried out in CADP.
Case studies
To demonstrate the functionality of our symbolic framework it is important to carry out case studies. Some small case studies exist, but these are not yet fully written up and published.

Collaborations have arisen through the tool development work with Alberto Verdejo (UCM, Spain) and Peter Robinson (SVRC, Australia). These are ongoing: Mr Verdejo is implementing other parts of the symbolic framework in Maude as part of his thesis, and an extended version of the Ergo paper is in preparation. New collaborations also arose in the theoretical work: Savi Maharaj (Stirling) contributed as much as a co-investigator (see the Computer Journal paper, the FME 2001 paper, and the TPHOLS paper) and Lionel Morel (IMAG, France) continues to work with us on a paper describing FULL*.

Related work, extending tool support for the framework by developing and implementing an algorithm for symbolic bisimulation is being carried out by Brian Ross (Glasgow), who is a student of Prof. Calder.