Search

• < Previous
• 1
• Next >

---

Cost Preserving Bisimulations for Probabilistic Automata

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&nbsp;[&hellip;]

---

Efficient CSL Model Checking Using Stratification

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&nbsp;[&hellip;]

---

Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations

Lijun Zhang ; Holger Hermanns ; Friedrich Eisenbrand ; David N. Jansen.

Strong and weak simulation relations have been proposed for Markov chains, while strong simulation and strong probabilistic simulation relations have been proposed for probabilistic automata. However, decision algorithms for strong and weak simulation over Markov chains, and for strong simulation&nbsp;[&hellip;]

---

Analysis of Timed and Long-Run Objectives for Markov Automata

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&nbsp;[&hellip;]

---

Conformance Relations and Hyperproperties for Doping Detection in Time and Space

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&nbsp;[&hellip;]

---