Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Gnesi S., Sacchelli R. Tableau methods to decide strong bisimilarity on LOTOS processes involving pure interleaving and enabling. Internal note IEI-B4-08, 1994.
In this paper we describe a technique, based on the construction of semantic tableaux, to decide the strong bisimulation equivalence on a subset of LOTOS describing the sequential composition of normed interleaved processes, LOTOSCF+III. The algorithm presented is based on a careful combination of two algorithms defined in literature respectively for the Basic Process Algebra and for the Basic Parallel Processes. Then the offered combination of these algorithms is shown to solve the decision of bisimulation equivalence between LOTOSCF+III normed processes.
Subject Bisimulation
Model checking
D.2.4 Software/Program Verification. Model checking

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional