On the Verification of Qualitative Properties of Probabilistic Processes under Fairness Constraints

Christel BaierChristel Baier, Marta Z. KwiatkowskaMarta Z. Kwiatkowska

DOI Link

Christel Baier, Marta Z. Kwiatkowska
On the Verification of Qualitative Properties of Probabilistic Processes under Fairness Constraints
Information Processing Letters, 66(2):71--79, 1998

Details
Bibtex

KurzfassungAbstract
We consider sequential and concurrent probabilistic processes and propose a general notion of fairness with respect to probabilistic choice, which allows to express various notions of fairness such as process fairness and event fairness. We show the soundness of proving the validity of qualitative properties of probabilistic processes under fairness constraints in the sense that whenever all fair executions of a probabilistic process fulfill a certain linear time property E then E holds for almost all executions (i.e., E holds with probability 1). It follows that in order to verify probabilistic processes with respect to linear time specifications, it suffices to establish that—for some instance of our general notion of fairness—all fair executions satisfy the specification. This generalizes the soundness results for extreme and α-fairness established by Pnueli in 1983 and 1993, respectively. Furthermore, we show that the α-fairness of Pnueli (1993) is the only fairness notion which is complete for validity of qualitative linear time properties.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{BK1998,
  author  = {Christel Baier and Marta Z. Kwiatkowska},
  title   = {On the Verification of Qualitative Properties of Probabilistic
             Processes under Fairness Constraints},
  journal = {Information Processing Letters},
  volume  = {66},
  number  = {2},
  year    = {1998},
  pages   = {71--79},
  doi     = {10.1016/S0020-0190(98)00038-6}
}