Stochastic transition systems

Abstract

Traditional methods for the analysis of system performance and reliability generally assume a precise knowledge of the system and its workload. Here, we present methods that are suited for the analysis of systems that contain partly unknown or unspecified components, such as systems in their early design stages.

We introduce stochastic transition systems, a high-level formalism for the modeling of timed probabilistic systems. Stochastic transition systems extend current modeling capabilities by enabling the representation of transitions having unknown delay distributions, alongside transitions with zero or exponentially-distributed delay. We show how these various types of transitions can be uniformly represented in terms of nondeterminism, probability, fairness and time, yielding efficient algorithms for system analysis. Finally, we present methods for the specification and verification of long-run average properties of STSs. These properties include many relevant performance and reliability indices, such as system throughput, average response time, and mean time between failures.

This work was partially supported by the NSF grant CCR-95-27927, by DARPA under the NASA grant NAG2-892, by the ARO grant DAAH04-95-1-0317, by ARO under the MURI grant DAAH04-96-1-0341, by Army contract DABT63-96-C-0096 (DARPA), by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, and by the NSF grant CCR-9504469.