Logical characterization of probabilistic τ-bisimulation equivalences

Stochastic Petri nets (SPNs) is a well-known model for quantitative analysis. We consider the class called DTWSPNs that is a modification of discrete time SPNs (DTSPNs) by transition labeling and weights. Transitions of DTWSPNs are labeled by actions that represent elementary activities and can be visible or invisible for an external observer. For DTWSPNs, interleaving and step probabilistic т-bisimulation equivalences that abstract from invisible actions are introduced. A logical characterization of the equivalences is presented via formulas of the new probabilistic modal logics. This means that DTWSPNs are (interleaving or step) probabilistic τ-bisimulation equivalent if they satisfy the same formulas of the corresponding probabilistic modal logic. Thus, instead of comparing DTWSPNs operationally, one has to check the corresponding satisfaction relation only. The new interleaving and step logics are modifications of the probabilistic modal logic PML proposed by K.G. Larsen and A. Skou on probabilistic transition systems with visible actions.