Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes (Q2257984)

The logic PML is a probabilistic version of modal logic, called Hennessy-Milner logic. Its diamond operator is decorated with a probability bound, i.e., formula \(\langle a\rangle_p\phi\) is satisfied by state \(s\) if an \(a\)-labelled transition is possible from \(s\) after which a set of states satisfying \(\phi\) is reached with probability at least \(p\). From the authors' abstract: Two alternative interpretations of PML over nondeterministic and probabilistic processes are considered and two new bisimulation-based equivalences that are in full agreement with those interpretations are provided. The new equivalences include as coarsest congruences the two bisimilarities for nondeterministic and probabilistic processes proposed by Segala and Lynch. The new interpretations of PML and the corresponding new bisimilarities are the first ones to offer a uniform framework for reasoning on processes that are purely nondeterministic or reactive probabilistic (no state has two or more outgoing transitions labelled by the same action) or that mix nondeterminism and probability in an alternating/nonalternanting way.