A temporal semantics far 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 the expressiveness of the logic with respect to the operational semantics modulo luce equivalence. The capability of the given semantics to be used to verify interesting properties of programs is also investigated, and a study for more expressive semantics is discussed.
An expressive temporal logic for basic LOTOS
Fantechi A;Gnesi S;
1989
Abstract
A temporal semantics far 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 the expressiveness of the logic with respect to the operational semantics modulo luce equivalence. The capability of the given semantics to be used to verify interesting properties of programs is also investigated, and a study for more expressive semantics is discussed.| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_418287-doc_147683.pdf
solo utenti autorizzati
Descrizione: An expressive temporal logic for basic LOTOS
Tipologia:
Versione Editoriale (PDF)
Dimensione
5.01 MB
Formato
Adobe PDF
|
5.01 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
