7 papers
Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata
Christel Baier, Sascha Klüppelholz, Timm Spork
Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes -regular languages by processing their ultimately periodic…
Backward Responsibility in Transition Systems Beyond Safety
Christel Baier, Rio Klatt, Sascha Klüppelholz +2
As the complexity of software systems rises, methods for explaining their behaviour are becoming ever-more important. When a system fails, it is critical to determine which of its…
Certificates and Witnesses for Multi-objective Ï-regular Queries in Markov Decision Processes
Christel Baier, Calvin Chau, Volodymyr Drobitko +2
Multi-objective probabilistic model checking is a powerful technique for verifying stochastic systems against multiple (potentially conflicting) properties. To enhance the trustwor…
Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
Timm Spork, Christel Baier, Joost-Pieter Katoen +2
We introduce -bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $(\varepsil…
Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes
Christel Baier, Calvin Chau, Sascha Klüppelholz
Certifying verification algorithms not only return whether a given property holds or not, but also provide an accompanying independently checkable certificate and a corresponding w…
Formal Quality Measures for Predictors in Markov Decision Processes
Christel Baier, Sascha Klüppelholz, Jakob Piribauer +1
In adaptive systems, predictors are used to anticipate changes in the systems state or behavior that may require system adaption, e.g., changing its configuration or adjusting reso…