Abstract

We present a testing preorder for Markovian processes based on a quantification of the probability with which they pass tests within a given amount of time, in order to establish in this setting a notion of process efficiency which may be useful for the analysis of soft real time systems. Markovian testing preorders are developed for continuous time processes, discrete time processes, and mixed processes where the duration of an action can be either exponentially distributed or zero. The Markovian testing theory is shown to enjoy close connections with the classical testing theory of De Nicola-Hennessy in that whenever a process passes a test with probability 1 (greater than 0) within some amount of time, then the process must (may) pass the test in the classical theory. The Markovian testing theory is similarly shown to be a refinement of the probabilistic testing theory of Cleaveland-Smolka et al. The relationship between the induced Markovian testing equivalence and the Markovian bisimulation equivalence is also presented. In order to ease the task of establishing relationships between Markovian processes, a fully abstract alternative characterization of the Markovian testing preorder is developed which is based on extended traces. A proof technique is derived from such an alternative characterization which simplifies the task of establishing preorder relationships between Markovian processes. Finally, it is shown that it is not possible to define a Markovian preorder which turns out to be consistent with reward based performance measures. This justifies the fact that a generic notion of efficiency has been considered.