Analysis and Verification of Regenerative Stochastic Systems

The work presents a solution for the transient analysis of systems in which multiple generally distributed timers can be started or stopped independently, but regenerations are encountered in a bounded number of discrete events. Then, the problem of verifying an "interval until operator" in a regenerative system is investigated. The proposed solution is based on a renewal argument specific to the interval until operator, which results in bivariate integral equations. Using stochastic state classes, an algorithm is provided for the computation of the parameters required in the solution.