How to specify and verify the long-run average behaviour of probabilistic systems
- 27 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 454-465
- https://doi.org/10.1109/lics.1998.705679
Abstract
Long-run average properties of probabilistic systems refer to the average behaviour 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 behaviour 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.Keywords
This publication has 14 references indexed in Scilit:
- Markov decision processes and regular eventsPublished by Springer Nature ,2005
- Probabilistic simulations for probabilistic processesPublished by Springer Nature ,2005
- A framework for reasoning about time and reliabilityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- A Compositional Approach to Performance ModellingPublished by Cambridge University Press (CUP) ,1996
- Extended Markovian Process AlgebraPublished by Springer Nature ,1996
- Giving a net semantics to Markovian process algebraPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1995
- A Distributed Semantics for EMPA Based on Stochastic Contextual NetsThe Computer Journal, 1995
- A logic for reasoning about time and reliabilityFormal Aspects of Computing, 1994
- On the solution of GSPN reward modelsPerformance Evaluation, 1991
- Verifying temporal properties of finite-state probabilistic programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1988