conclusion.tex

% chapter : Conclusion and future work

\chapter{Conclusion and future work}\label{chapConclusion}

The main achievement of this thesis is the construction and (rigorous) verification of an operational based inference system for reasoning about bisimulation equivalence and (more important) inequivalence. The fact that this system not only produces a bisimulation containing a given pair, $(p,q)$, in case $p\sim q$, but also, in case $p\not\sim q$, is capable of giving a modal property (an argument of inequivalence) which only one of the processes enjoys, makes the system very suitable as an automatic tool aiding verification and debugging of systems. The usefulness was demonstrated through some examples. Also, an extension of the system making it possible to find weak bisimulations was discussed and the usefulness of this much more interesting system was demonstrated through several examples. In particular, the \verb#closedshop#-example, indicated that some sort of structuring of the bisimulations produced by the system was needed. The structure imposed gave for each pair in the bisimulation information about how moves of one process was matched by moved by the other. This resulted in the notion of extended bisimulation which was shown to be faithful to the standard notion of bisimulation. Moreover, a system finding extended bisimulations was implemented and the additional information supplied by the system immediately proved to be superior to that produced by other systems when \verb#closedshop# was reconsidered. The extra information given actually makes it easy to get a good insight into {\em how\/} the pairs of the bisimulation fits together, and thereby making it a lot more sensible using the system for theorem proving and a lot easier to take advantage of the produced results.

All in all we must conclude that our system actually fulfill the original goal of constructing a system arguing bisimulation equivalence or inequivalence. Furthermore, the system(s) seems to be a very useful tool assisting the verification of systems.

there are at least two related and interesting problems which are not covered by this thesis:
\begin{enumerate}
\item Find the time complexity of the algorithm used.
\item Show (if possible) that the properties generated are minimal (in some sense).
\end{enumerate}
Due to the algorithm following very closely the recursive definition of bisimulation and that backtracking may be necessary (when non-deterministic processes are considered) the time complexity is essentially exponential. However, it would be nice to verify this. Also, it would be interesting if the (expected) minimality of properties could be verified, as this would argue that the properties produced by our system in fact are concise and that our properties are `smaller' that the ones produced by e.g.\@ the system of~\cite{VestmarOlesen}.

Related to this is the question of whether or not the properties supplied by our system are as informative as we would like to think they are. Surely, they are both correct and they concisely states the property distinguishing the two inequivalent processes, but what are the alternatives? Of course, when asking a question like this you cannot expect to receive a final answer. We will certainly not give `the' answer, but we would like to put forward an alternative way of presenting the results of the system to the user. Imagine a system which differs from our system in that it initially just will tell whether or not the processes under consideration are equivalent. Now, instead of giving the full argument for the answer, the system will try to {\em convince\/} the user of the correctness of the answer by playing a `game' with him. It is a game in the sense that the competitors tires to make `life' as hard as possible for each other. The rules are easy. There are two situations to consider; in the first situation the system has determined that the processes are equivalent, and in the other it has been determined that the processes are inequivalent. In the first case the user `moves' first whereas in the latter case the system has the first `move'. A move actually consists of selecting a derivation which the opponent has to match. Assume that the processes under consideration are $SYS1$ and $SYS2$ then two typical situations could be:
\begin{itemize}
\item[$SYS1\not\sim SYS2$ :] The system moves first. It chooses a process to move, $SYS1$ say. Of course, it selects the worst possible move, namely the move which it knows that $SYS2$ cannot match. Then the user may try to find a move of $SYS2$ matching the move by the system. In case $SYS2$ cannot perform the given action, obviously he must acknowledge the answer given. Otherwise, no matter which derivation of $SYS2$ he chooses, he will of course not succeed, and finally---after sufficiently many repetitions of the game---he will have to admit that the system was right in the first place saying that $SYS1\not\sim SYS2$.

\item[$SYS1\sim SYS2$ :] Now, the user chooses a process to move, $SYS2$ say. He will then try to find a move of $SYS2$ which $SYS1$ cannot match and thereby prove that the system was wrong about saying that $SYS1\sim SYS2$. However, ind the end---after sufficiently many moves of the game---he will have to give in and admit the system was right all along, as the system will be able to match any move he can perform on $SYS2$.

\end{itemize}
Now, the point is that a system using the above method of communicating with the user will force the user to explore the behaviour of the two processes to an extent he probably never would have done in another situation and thereby he will learn more about the processes themselves and possibly gain a better understanding of why processes behave in the way the do. Also, this method does not even require the user to know anything about the theory of bisimulation, modal properties etc. All he has to know is how to make a move of a (CCS-)process.

% end of chapter