We introduce two observational logics for reasoning about Distributed Transition Systems (DTS). These logics characterize different classes of properties of DTS compurations. The first logic, LD, is a straightforward generalization of Hennessy-Milner Logic obtained by allowing modalities indexed by partial ordering observations; it is in full agreement with a computationally defined observational equivalence for true concurrency. The second logic, LP, has as a distinctive feature a past operator which appears to be crucial for adequately describing the interplay of concurrency and nondeterminism. A deeper understanding of Lp is gained by showing that it induces On DTS the same identification of another observational semantics.
Observational logics and true concurrency
De Nicola R;
1989
Abstract
We introduce two observational logics for reasoning about Distributed Transition Systems (DTS). These logics characterize different classes of properties of DTS compurations. The first logic, LD, is a straightforward generalization of Hennessy-Milner Logic obtained by allowing modalities indexed by partial ordering observations; it is in full agreement with a computationally defined observational equivalence for true concurrency. The second logic, LP, has as a distinctive feature a past operator which appears to be crucial for adequately describing the interplay of concurrency and nondeterminism. A deeper understanding of Lp is gained by showing that it induces On DTS the same identification of another observational semantics.File | Dimensione | Formato | |
---|---|---|---|
prod_418187-doc_147603.pdf
solo utenti autorizzati
Descrizione: Observational logics and true concurrency
Tipologia:
Versione Editoriale (PDF)
Dimensione
1.01 MB
Formato
Adobe PDF
|
1.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.