page 1  (13 pages)
2to next section

Almost always" and definitely sometime" are not enough:

Probabilistic quantifiers and Probabilistic model-checking1

Purush Iyer and Murali Narasimha
Dept of Computer Science
North Carolina State University
Raleigh, NC 27695-8206
e-mail: fpurush,
Phone: +1 (919)-515-7291
Fax: +1 (919)-515-7896 NC State University

Tech Report


Specifications for probabilistic programs often use the notion of almost always and definitely sometime to capture the probabilistic information. But there are a number of instances (eg. network protocols) where probabilistic information needs to be explicitly specified. In this paper we present PCTL?, a probabilistic version of the branching time logic CTL?, where the quantifiers for universality (almost always) and existence (definitely sometime) are replaced by a single probabilistic quantifier. We argue that this logic is more general than previous logics. We show how to model-check probabilistic programs (given as markov chains) against specifications in PCTL?. We also prove our algorithm correct and provide an analysis of its computational complexity.

1Supported in part by grant under NSF CCR-9404619