MODEL CHECKING FOR A PROBABILISTIC BRANCHING TIME LOGIC WITH FAIRNESS

We consider concurrent probabilistic systems, based on probabilistic a utomata of Segala & Lynch [55], which allow non-deterministic choice b etween probability distributions. These systems can be decomposed into a collection of ''computation trees'' which arise by resolving the no n-deterministic, but not probabilistic, choices. The presence of non-d eterminism means that certain liveness properties cannot be establishe d unless fairness is assumed. We introduce a probabilistic branching t ime logic PBTL, based on the logic TPCTL of Hansson [30] and the logic PCTL of [55], resp. pCTL of [14]. The formulas of the logic express p roperties such as ''every request is eventually granted with probabili ty at least p''. We give three interpretations for PBTL on concurrent probabilistic processes: the first is standard, while in the remaining two interpretations the branching time quantifiers are taken to range over a certain kind of fair computation trees. We then present a mode l checking algorithm for verifying whether a concurrent probabilistic process satisfies a PBTL formula assuming fairness constraints. We als o propose adaptations of existing model checking algorithms for pCTL* [4, 14] to obtain procedures for PBTL* under fairness constraints. The techniques developed in this paper have applications in automatic ver ification of randomized distributed systems.