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.
A denotational semantics for lotos
Fantechi A;Gnesi S;
1991
Abstract
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.| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_447636-doc_161317.pdf
accesso aperto
Descrizione: A denotational semantics for lotos
Dimensione
3.11 MB
Formato
Adobe PDF
|
3.11 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
