How to Specify and Verify the Long-Run Average Behavior of Probabilistic Systems

Long-run average properties of probabilistic systems refer to average behavior of the system, measured over a period of time whose length diverges to infinity. These properties include many relevant performance and reliability indices, such as system throughput, average response time, and mean time between failures. In this paper, we argue that current formal specification methods cannot be used to specify long-run average properties of probabilistic systems. To enable the specification of these properties, we propose an approach based on the concept of experiments. Experiments are labeled graphs that can be used to describe behavior patterns of interest, such as the request for a resource followed by either a grant or a rejection. Experiments are meant to be performed infinitely often, and it is possible to specify their long-run average outcome or duration. We propose simple extensions of temporal logics based on experiments, and we present model-checking algorithms for the verification of properties of finite-state timed probabilistic systems in which both probabilistic and nondeterministic choice are present. The consideration of system models that include nondeterminism enables the performance and reliability analysis of partially specified systems, such as systems in their early design stages.