4 results
Dennis Guck ; Hassan Hatefi ; Holger Hermanns ; Joost-Pieter Katoen ; Mark Timmer.
Markov automata (MAs) extend labelled transition systems with random delays and probabilistic branching. Action-labelled transitions are instantaneous and yield a distribution over states, whereas timed transitions impose a random delay governed by an exponential distribution. MAs are thus a […]
Published on September 10, 2014
Andrea Turrini ; Holger Hermanns.
Probabilistic automata constitute a versatile and elegant model for concurrent probabilistic systems. They are equipped with a compositional theory supporting abstraction, enabled by weak probabilistic bisimulation serving as the reference notion for summarising the effect of abstraction. This paper […]
Published on December 18, 2014
Lijun Zhang ; David N. Jansen ; Flemming Nielson ; Holger Hermanns.
For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be turned into an approximation algorithm with worse than exponential […]
Published on July 31, 2012
Sebastian Biewer ; Rayna Dimitrova ; Michael Fries ; Maciej Gazda ; Thomas Heinze ; Holger Hermanns ; Mohammad Reza Mousavi.
We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a […]
Published on January 19, 2022