Fantechi A., Gnesi S., Sacchelli R. Tableau methods to decide strong bisimilarity on LOTOS processes involving pure interleaving and enabling. In: Seventh International Conference on Formal Description Techniques. (Berne, Switzerland, 4 - 7 October 1994). Proceedings, pp. 198 - 200. Dieter Hogrefe, Stefan Leue (eds.). Silhouette, 1994. |

Abstract (English) |
Several methodologies and most automatic tool support for LOTOS can only be used if the specifications considered describe finite-state machines. For example, an equivalence verifier can only manipulate specifications in this class; an attempt to verify the equivalence of two non finite-state processes may not terminate with an answer. However, as it is known, LOTOS gives the possibility to describe also non finite-state systems. So it could be useful to provide methodologies and tools for verification on this class of systems. Indeed more powerful verification techniques have recently been exploited for non-finite state systems defined in other process algebras. Among these verification techniques we wish to recall the bisimulation decision algorithms on context free processes of Basic Process Algebra (BPA) due to Baeten, Bergstra and Klop and to Hüttel and Stirling and the algorithm to decide the bisimilarity between Basic Parallel Processes (BPP) given in [8]. In this paper we present a decision algorithm to prove the bisimulation between non finite-state systems on a subset of LOTOS, LOTOS CF+III, able to describe the sequential composition of normed interleaved recursive processes. The class of processes so defined covers all context free processes and some context dependent processes. This subset, called from now on LOTOS CF+III can be seen as tbe combination of two process languages. The first, LOTOS CF, includes action prefix, exit, enabling and recursion. The second, LOTOS III, includes action prefix, exit, pure interleaving and recursion. | |

Subject | LOTOS verification D.2.4 Software/Program Verification |

1) Download Document PDF |

Open access Restricted Private