A symholic semantics for Pull LOTOS in terms of symbolic transition systems is defined; the semantics extends the (infinitely branching) standard semantics by giving meaning to data parameterised behaviours, and provides a finitely branching representation for behaviours. Symbolic bisimulation is defined. This extends our previous work [14], making the definitions more amenable to automated reasoning and processes with recursion.
展开▼
