Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Gnesi S., Ristori G. Compositional logic semantics and lotos. In: 10th International IFIP WG 6.1 Symposium on Protocol Specification, Testing and Verification. (Ottawa, Ontario, Canada, 12 - 15 June 1990). Proceedings, pp. 365 - 378. Luigi Logrippo, Robert L. Probert and Hansan Ural (eds.). North-Holland, 1990.
A branching temporal semantics for a subset of LOTOS is proposed in order to provide a formal tool to verify properties of LOTOS specifications. The semantics is defined using a compositional approach, to provide modularity in the verification process, by which it is possible to associate a CTL * formula to each language construct. The relations between the equivalence defined on LOTOS and the equivalence induced by the temporal semantics have been studied, proving that the compositionality requiremement does not permit to preserve the discriminating power of bisimulation. We succeed however in reaching a weaker equivalence, simulation, which appears to be the strongest one with respect to which it is possible to give a fully abstract compositional semantics using standard temporal logics.
Subject LOTOS

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