Verification of equivalences between finite transition systems Theory and applications

The concepts of labelled transition system, and of observation-equivalence and testing-equivalence between systems are introduced. These topics are discussed in a number of papers, sparse in the Iiterature; they are conveniently assembled here in a unique, self-contained presentation. Ali proofs have been worked out in detail, and the reader is assumed unfamiliar with fixpoint theory. Three algorithms for verifying equivalence between finite transition systems are introduced and discussed (two for observation-equivalence and one for testing-equivalence). A proof of correctness for one of them, Sanderson's algorithm, is given (it was not found in the Iiterature). The algorithms have been implemented in Prolog, and their application to a small example is illustrated.

Vengono introdotti i concetti di sistema di transizioni, e di equivalenze osservazionale e di 'testing' fra sistemi. Questi argomenti sono discussi in svariati articoli, sparsi nella letteratura; essi sono convenientemente raccolti qui in una presentazione unica ed introduttiva. Tutte le dimostrazioni sono state elaborate in dettaglio, e non si assume famigliarita' con la teoria del punto fisso. Vengono introdotti e discussi tre algoritmi per verificare la equivalenza fra sistemi di transizione finiti (due per la equivalenza osservazionale, uno per la equivalenza di 'testing'). Viene fornita una prova di correttezza di uno di essi, l'algoritmo di Sanderson (non essendo stata trovata in letteratura). Gli algoritmi sono stati implementati in Prolog, e viene illustrata la loro applicazione ad un piccolo esempio.