A symbolic semantics for Full LOTOS in terms of symbolic transition systems is defined, following the approach taken for message passing CCS in [HL95a], altered to take account of the particular features of LOTOS (multi-way synchronisation, value negotiation, slection predicates). Symbolic bisimulation over symbolic transition systems is defined, and symbolic bisimulation on ground behaviour expressions is shown to preserve the usual concrete (strong) bisimulation on the standard semantics. Finally, a modal logic based on symbolic transition systems is defined. All are illustrated with reference to examples.
展开▼
