611 citations · 855 across the 28 of their papers we have counts for
33 papers
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…
Software Doping Analysis for Human Oversight
Sebastian Biewer, Kevin Baum, Sarah Sterz +5
This article introduces a framework that is meant to assist in mitigating societal risks that software can pose. Concretely, this encompasses facets of software doping as well as u…
On the Foundations of Cycles in Bayesian Networks
Christel Baier, Clemens Dubslaff, Holger Hermanns +1
Bayesian networks (BNs) are a probabilistic graphical model widely used for representing expert knowledge and reasoning under uncertainty. Traditionally, they are based on directed…
On the Automation, Optimization, and In-Orbit Validation of Intelligent Satellite Constellation Operations
Gregory Stock, Juan A. Fraire, Holger Hermanns +3
Recent breakthroughs in technology have led to a thriving "new space" culture in low-Earth orbit (LEO) in which performance and cost considerations dominate over resilience and rel…
Distributed On-Demand Routing for LEO Mega-Constellations: A Starlink Case Study
Gregory Stock, Juan A. Fraire, Holger Hermanns
The design and launch of large-scale satellite networks create an imminent demand for efficient and delay-minimising routing methods. With the rising number of satellites in such c…
RTLola on Board: Testing Real Driving Emissions on your Phone
Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns +3
This paper is about shipping runtime verification to the masses. It presents the crucial technology enabling everyday car owners to monitor the behaviour of their cars in-the-wild.…
What Do We Want From Explainable Artificial Intelligence (XAI)? -- A Stakeholder Perspective on XAI and a Conceptual Model Guiding Interdisciplinary XAI Research
Markus Langer, Daniel Oster, Timo Speith +5
Previous research in Explainable Artificial Intelligence (XAI) suggests that a main aim of explainability approaches is to satisfy specific interests, goals, expectations, needs, 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…
Towards a Framework Combining Machine Ethics and Machine Explainability
Kevin Baum, Holger Hermanns, Timo Speith
We find ourselves surrounded by a rapidly increasing number of autonomous and semi-autonomous systems. Two grand challenges arise from this development: Machine Ethics and Machine…
Continuous-Time Markov Decisions based on Partial Exploration
Pranav Ashok, Yuliya Butkova, Holger Hermanns +1
We provide a framework for speeding up algorithms for time-bounded reachability analysis of continuous-time Markov decision processes. The principle is to find a small, but almost…
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.
Multi-Objective Approaches to Markov Decision Processes with Uncertain Transition Parameters
Dimitri Scheftelowitsch, Peter Buchholz, Vahid Hashemi +1
Markov decision processes (MDPs) are a popular model for performance analysis and optimization of stochastic systems. The parameters of stochastic behavior of MDPs are estimates fr…
Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes
Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns +2
Interval Markov decision processes (IMDPs) generalise classical MDPs by having interval-valued transition probabilities. They provide a powerful modelling tool for probabilistic sy…
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…
Distributed Synthesis in Continuous Time
Holger Hermanns, Jan Krčál, Steen Vester
We introduce a formalism modelling communication of distributed agents strictly in continuous-time. Within this framework, we study the problem of synthesising local strategies for…
On the Control of Self-Balancing Unicycles
Felix Freiberger, Holger Hermanns
This paper discusses the problem of designing a self-balancing unicycle where pedals are used for both power generation and speed control. After developing the principal physical a…
Optimal Continuous Time Markov Decisions
Yuliya Butkova, Hassan Hatefi, Holger Hermanns +1
In the context of Markov decision processes running in continuous time, one of the most intriguing challenges is the efficient approximation of finite horizon reachability objectiv…
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…
Recharging Probably Keeps Batteries Alive
Holger Hermanns, Jan Krčál, Gilles Nies
The kinetic battery model is a popular model of the dynamic behavior of a conventional battery, useful to predict or optimize the time until battery depletion. The model however la…
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…
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…