Technical Reports

A List by Author: Holger Hermanns

e-mail:

hermanns(a)cs.uni-saarland.de

Probabilistic Bisimulation: Naturally on Distributions

by Holger Hermanns, Jan Krèál, Jan Køetínský, April 2014, 36 pages.

FIMU-RS-2014-03. Available as Postscript, PDF.

Abstract:

In contrast to the usual understanding of probabilistic systems as stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this paper, we give a natural definition of strong bisimulation for probabilistic systems corresponding to this view that treats probability distributions as first-class citizens. Our definition applies in the same way to discrete systems as well as to systems with uncountable state and action spaces. Several examples demonstrate that our definition refines the understanding of behavioural equivalences of probabilistic systems. In particular, it solves a longstanding open problem concerning the representation of memoryless continuous time by memoryfull continuous time. Finally, we give algorithms for computing this bisimulation not only for finite but also for classes of uncountably infinite systems.

Verification of Open Interactive Markov Chains

by Tomá¹ Brázdil, Holger Hermanns, Jan Krèál, Jan Køetínský, Vojtìch Øehák, A full version of the paper presented at conference FSTTCS 2012. November 2012, 52 pages.

FIMU-RS-2012-04. Available as Postscript, PDF.

Abstract:

Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience - owed to compositionality properties - with effective verification algorithms and tools - owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive bounds on reachability probabilities that are assured to hold in any composition context.