We consider action-labelled systems with non-deterministic and probabilistic choice. Using the concept of norm functions, we introduce two types of bisimulations (called (strict) normed bisimulation equivalence) that allow for delays when simulating a transition and are strictly between strong and weak bisimulation equivalence a la. Using a suitable modification of th prominent splitter/partitioning technique, we present polynomial-time algorithms that constructs the quotient space of the (strict) normed bisimulation equivalence classes.
展开▼
