Compositional failure-based semantic models for Basic LOTOS

Autor: Martti Tienari, Antti Valmari
Rok vydání: 1995
Předmět:
Zdroj: Formal Aspects of Computing. 7:440-468
ISSN: 1433-299X
0934-5043
DOI: 10.1007/bf01211218
Popis: A systematic analysis of trace- and failure-based compositional semantic models for Basic LOTOS is presented. The analysis is motivated by the fact that the weakest known equivalences preserving sufficient information for several typical verification tasks are failure-based, and the weakness of an equivalence can be advantageous for verification. Both the equivalences and the preorders corresponding to the semantic models are covered. The analysis yields in a natural way two compositional semantic models, which are particularly suited for the verification of a general class of liveness properties, a task which cannot be performed with most established models.
Databáze: OpenAIRE