Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Ferrari G. L. Observational logics and true concurrency. In: Third Italian Conference on Theoretical Computer Science (Mantova, 2 - 4 November 1989). Atti, pp. 212 - 223. A. Bertoni et al. (eds.). World Scientific, 1989.
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.

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