Stochastic transition systems

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.