Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Ferro M., Gnesi S., Tamorri G. A denotational semantics for lotos. Internal note IEI-B4-21, 1991.
A denotational semantics for LOTOS is proposed in order to provide a formal tool to verify properties of LOTOS specification and to verify equivalences of LOTOS processes in a simple way. The defined semantics is a linear temporal one, given using a compositional approach, that relates a temporallogic formula to each language construct. Such semantics is proved fully abstract with respect to the trace equivalence defined on the operational semantics of the language. Also, we investigate on the capability of other semantics to be fully abstract with respect to stronger equivalences, because of the weakness of the trace equivalence.

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