# Probabilistic model checking of regenerative concurrent systems

## M. Paolieri, A. Horváth, E. Vicario

**Abstract:** We consider the problem of verifying quantitative reachability
properties in stochastic models of concurrent activities with
generally distributed durations. Models are specified as stochastic
time Petri nets and checked against Boolean combinations of interval
until operators imposing bounds on the probability that the marking
process will satisfy a goal condition at some time in the interval
[α,β] after an execution that never violates a safety property. The
proposed solution is based on the analysis of regeneration points in
model executions: a regeneration is encountered after a discrete event
if the future evolution depends only on the current marking and not on
its previous history, thus satisfying the Markov property. We analyze
systems in which multiple generally distributed timers can be started
or stopped independently, but regeneration points are always
encountered with probability 1 after a bounded number of discrete
events. Leveraging the properties of regeneration points in
probability spaces of execution paths, we show that the problem can be
reduced to a set of Volterra integral equations, and we provide
algorithms to compute their parameters through the enumeration of
finite sequences of stochastic state classes encoding the joint
probability density function (PDF) of generally distributed timers
after each discrete event. The computation of symbolic PDFs is limited
to discrete events before the first regeneration, and the repetitive
structure of the stochastic process is exploited also before the lower
bound α, providing crucial benefits for large time bounds. A case
study is presented through the probabilistic formulation of Fischer’s
mutual exclusion protocol, a well-known real-time verification
benchmark.

Stochastic ProcessesModel CheckingTheory

copy bib | save bib | save pdf | go to publisher

🏠 Home