A temporal semantics for Basic LOTOS, i.e. LOTOS without value passing, is presented. The semantics is provided using a compositional approach by which it is possible to associate temporal logic formulae to each language construct. The relationships between this semantics and the operational semantics of the language have been studied in detail, showing its simple abstractness with respect to the operational semantics modulo string equivalence. The capability of the given semantics to be used to verify interesting properties of programs is also investigated.
A temporal semantics for basic LOTOS
Fantechi A;Gnesi S;
1989
Abstract
A temporal semantics for Basic LOTOS, i.e. LOTOS without value passing, is presented. The semantics is provided using a compositional approach by which it is possible to associate temporal logic formulae to each language construct. The relationships between this semantics and the operational semantics of the language have been studied in detail, showing its simple abstractness with respect to the operational semantics modulo string equivalence. The capability of the given semantics to be used to verify interesting properties of programs is also investigated.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_418096-doc_147530.pdf
accesso aperto
Descrizione: A temporal semantics for basic LOTOS
Dimensione
2.49 MB
Formato
Adobe PDF
|
2.49 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
