SPEAKER: Kim G. Larsen, BRICS, Aalborg University

DATE: 16 September 1999

PLACE and TIME: Room E3-209 at 15:00.

ABSTRACT:

This talk will be a rerun of my invited talk at PROBMIV. The 'validation'-part of the talk is related to the testing theory of De Nicola and Hennessy, but differs radically in that we consider tests as algorithmic descriptions, which must be guaranteed to terminate within some prescribed amount of time. However, due to the probabilistic setting, we are able to offer a metric for measuring the coverage of a testing effort (or the probability of making an erroneous conclusion).

We recall and generalize the early joint work with Arne Skou to the model of homogeneous, continuous-time Markov chains, as applied in several new probabilistic process algebras. That is, transitions are associated with a continuous time random process with an exponential distributed delay. Indeterminism is resolved by races between transitions executing at different rates. More precisely, we introduce a testing language, which allows performance properties of such systems to be settled with arbitrarily low error-probability through application of effectively constructable, finite tests. The testable performance properties are themselves expressed in a suitable rate-extended version of Hennessy-Milner Logic, which we show characterize a rate-based version of the probabilistic bisimulation of Larsen&Skou. The full distinguishing power of the suggested testing language is also shown to coincide with this version of probabilistic bisimulation.

In addition, I hope to have time to address the issue of compositional 'verification' of probabilistic systems, in particular in the context of continuous-time Markov systems.

For more information and references, you might also wish to look at the abstract of the PROBMIV99 talk.