611 citations · 855 across the 28 of their papers we have counts for
16 papers · 1 filter
Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic (Extended Version)
Lena Becker, Holger Hermanns
Markov jump linear systems (MJLSs) model dynamical phenomena subject to random switching among multiple linear modes, driven by an underlying Markov chain. Classical notions such a…
Conformance Relations and Hyperproperties for Doping Detection in Time and Space
Sebastian Biewer, Rayna Dimitrova, Michael Fries +4
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-…
Doping Tests for Cyber-Physical Systems
Sebastian Biewer, Pedro D'Argenio, Holger Hermanns
The software running in embedded or cyber-physical systems (CPS) is typically of proprietary nature, so users do not know precisely what the systems they own are (in)capable of doi…
Facets of Software Doping
Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner +1
This paper provides an informal discussion of the formal aspects of software doping.
Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems
Holger Hermanns, Peter Höfner
This volume contains the proceedings of MARS 2017, the second workshop on Models for Formal Analysis of Real Systems, held on April 29, 2017 in Uppala, Sweden, as an affiliated wor…
Is your software on dope? Formal analysis of surreptitiously "enhanced" programs
Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer +2
Usually, it is the software manufacturer who employs verification or testing to ensure that the software embedded in a device meets its main objectives. However, these days we are…
Compositional Reasoning for Interval Markov Decision Processes
Vahid Hashemi, Holger Hermanns, Andrea Turrini
Model checking probabilistic CTL properties of Markov decision processes with convex uncertainties has been recently investigated by Puggelli et al. Such model checking algorithms…
Explicit Model Checking of Very Large MDP using Partitioning and Secondary Storage
Arnd Hartmanns, Holger Hermanns
The applicability of model checking is hindered by the state space explosion problem in combination with limited amounts of main memory. To extend its reach, the large available ca…
Analysis of Timed and Long-Run Objectives for Markov Automata
Dennis Guck, Hassan Hatefi, Holger Hermanns +2
Markov automata (MAs) extend labelled transition systems with random delays and probabilistic branching. Action-labelled transitions are instantaneous and yield a distribution over…
MeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata
Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi +3
Markov automata combine continuous time, probabilistic transitions, and nondeterminism in a single model. They represent an important and powerful way to model a wide range of comp…
Probabilistic Bisimulation: Naturally on Distributions
Holger Hermanns, Jan Krčál, Jan Křetínský
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 pa…
Modelling, Reduction and Analysis of Markov Automata (extended version)
Dennis Guck, Hassan Hatefi, Holger Hermanns +2
Markov automata (MA) constitute an expressive continuous-time compositional modelling formalism. They appear as semantic backbones for engineering frameworks including dynamic faul…
Compositional Verification and Optimization of Interactive Markov Chains
Holger Hermanns, Jan Krčál, Jan Křetínský
Interactive Markov chains (IMC) are compositional behavioural models extending labelled transition systems and continuous-time Markov chains. We provide a framework and algorithms…
Transient Reward Approximation for Continuous-Time Markov Chains
Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer +1
We are interested in the analysis of very large continuous-time Markov chains (CTMCs) with many distinct rates. Such models arise naturally in the context of reliability analysis,…
Efficient CSL Model Checking Using Stratification
Lijun Zhang, David N. Jansen, Flemming Nielson +1
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,…
Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations
Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand +1
Strong and weak simulation relations have been proposed for Markov chains, while strong simulation and strong probabilistic simulation relations have been proposed for probabilisti…