BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Christel Baier

Christel Baier contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer Sciencemath.OCPerformanceeess.SYSoftware EngineeringSymbolic ComputationSystems and Control

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
9works
0followers
7topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

9 published item(s)

preprint2022arXiv

Causality in Configurable Software Systems

Detecting and understanding reasons for defects and inadvertent behavior in software is challenging due to their increasing complexity. In configurable software systems, the combinatorics that arises from the multitude of features a user might select from adds a further layer of complexity. We introduce the notion of feature causality, which is based on counterfactual reasoning and inspired by the seminal definition of actual causality by Halpern and Pearl. Feature causality operates at the level of system configurations and is capable of identifying features and their interactions that are the reason for emerging functional and non-functional properties. We present various methods to explicate these reasons, in particular well-established notions of responsibility and blame that we extend to the feature-oriented setting. Establishing a close connection of feature causality to prime implicants, we provide algorithms to effectively compute feature causes and causal explications. By means of an evaluation on a wide range of configurable software systems, including community benchmarks and real-world systems, we demonstrate the feasibility of our approach: We illustrate how our notion of causality facilitates to identify root causes, estimate the effects of features, and detect feature interactions.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

On probability-raising causality in Markov decision processes

The purpose of this paper is to introduce a notion of causality in Markov decision processes based on the probability-raising principle and to analyze its algorithmic properties. The latter includes algorithms for checking cause-effect relationships and the existence of probability-raising causes for given effect scenarios. Inspired by concepts of statistical analysis, we study quality measures (recall, coverage ratio and f-score) for causes and develop algorithms for their computation. Finally, the computational complexity for finding optimal causes with respect to these measures is analyzed.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

The variance-penalized stochastic shortest path problem

The stochastic shortest path problem (SSPP) asks to resolve the non-deterministic choices in a Markov decision process (MDP) such that the expected accumulated weight before reaching a target state is maximized. This paper addresses the optimization of the variance-penalized expectation (VPE) of the accumulated weight, which is a variant of the SSPP in which a multiple of the variance of accumulated weights is incurred as a penalty. It is shown that the optimal VPE in MDPs with non-negative weights as well as an optimal deterministic finite-memory scheduler can be computed in exponential space. The threshold problem whether the maximal VPE exceeds a given rational is shown to be EXPTIME-hard and to lie in NEXPTIME. Furthermore, a result of interest in its own right obtained on the way is that a variance-minimal scheduler among all expectation-optimal schedulers can be computed in polynomial time.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Farkas certificates and minimal witnesses for probabilistic reachability constraints

This paper introduces Farkas certificates for lower and upper bounds on minimal and maximal reachability probabilities in Markov decision processes (MDP), which we derive using an MDP-variant of Farkas' Lemma. The set of all such certificates is shown to form a polytope whose points correspond to witnessing subsystems of the model and the property. Using this correspondence we can translate the problem of finding minimal witnesses to the problem of finding vertices with a maximal number of zeros. While computing such vertices is computationally hard in general, we derive new heuristics from our formulations that exhibit competitive performance compared to state-of-the-art techniques. As an argument that asymptotically better algorithms cannot be hoped for, we show that the decision version of finding minimal witnesses is NP-complete even for acyclic Markov chains.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Iterative Variable Reordering: Taming Huge System Families

For the verification of systems using model-checking techniques, symbolic representations based on binary decision diagrams (BDDs) often help to tackle the well-known state-space explosion problem. Symbolic BDD-based representations have been also shown to be successful for the analysis of families of systems that arise, e.g., through configurable parameters or following the feature-oriented modeling approach. The state space of such system families face an additional exponential blowup in the number of parameters or features. It is well known that the order of variables in ordered BDDs is crucial for the size of the model representation. Especially for automatically generated models from real-world systems, family models might even be not constructible due to bad variable orders. In this paper we describe a technique, called iterative variable reordering, that can enable the construction of large-scale family models. We exemplify feasibility of our approach by means of an aircraft velocity control system with redundancy mechanisms modeled in the input language of the probabilistic model checker PRISM. We show that standard reordering and dynamic reordering techniques fail to construct the family model due to memory and time constraints, respectively, while the new iterative approach succeeds to generate a symbolic family model.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Minimal witnesses for probabilistic timed automata

Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic information on why a given property holds or as input to refinement algorithms. This paper introduces witnessing subsystems for reachability problems in probabilistic timed automata (PTA). Using a new operation on difference bounds matrices, it is shown how Farkas certificates of finite-state bisimulation quotients of a PTA can be translated into witnessing subsystems. We present algorithms for the computation of minimal witnessing subsystems under three notions of minimality, which capture the timed behavior from different perspectives, and discuss their complexity.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

On Skolem-hardness and saturation points in Markov decision processes

The Skolem problem and the related Positivity problem for linear recurrence sequences are outstanding number-theoretic problems whose decidability has been open for many decades. In this paper, the inherent mathematical difficulty of a series of optimization problems on Markov decision processes (MDPs) is shown by a reduction from the Positivity problem to the associated decision problems which establishes that the problems are also at least as hard as the Skolem problem as an immediate consequence. The optimization problems under consideration are two non-classical variants of the stochastic shortest path problem (SSPP) in terms of expected partial or conditional accumulated weights, the optimization of the conditional value-at-risk for accumulated weights, and two problems addressing the long-run satisfaction of path properties, namely the optimization of long-run probabilities of regular co-safety properties and the model-checking problem of the logic frequency-LTL. To prove the Positivity- and hence Skolem-hardness for the latter two problems, a new auxiliary path measure, called weighted long-run frequency, is introduced and the Positivity-hardness of the corresponding decision problem is shown as an intermediate step. For the partial and conditional SSPP on MDPs with non-negative weights and for the optimization of long-run probabilities of constrained reachability properties (a U b), solutions are known that rely on the identification of a bound on the accumulated weight or the number of consecutive visits to certain sates, called a saturation point, from which on optimal schedulers behave memorylessly. In this paper, it is shown that also the optimization of the conditional value-at-risk for the classical SSPP and of weighted long-run frequencies on MDPs with non-negative weights can be solved in pseudo-polynomial time exploiting the existence of a saturation point.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Reduction Methods on Probabilistic Control-flow Programs for Reliability Analysis

Modern safety-critical systems are heterogeneous, complex, and highly dynamic. They require reliability evaluation methods that go beyond the classical static methods such as fault trees, event trees, or reliability block diagrams. Promising dynamic reliability analysis methods employ probabilistic model checking on various probabilistic state-based models. However, such methods have to tackle the well-known state-space explosion problem. To compete with this problem, reduction methods such as symmetry reduction and partial-order reduction have been successfully applied to probabilistic models by means of discrete Markov chains or Markov decision processes. Such models are usually specified using probabilistic programs provided in guarded command language. In this paper, we propose two automated reduction methods for probabilistic programs that operate on a purely syntactic level: reset value optimization and register allocation optimization. The presented techniques rely on concepts well known from compiler construction such as live range analysis and register allocation through interference graph coloring. Applied on a redundancy system model for an aircraft velocity control loop modeled in SIMULINK, we show effectiveness of our implementation of the reduction methods. We demonstrate that model-size reductions in three orders of magnitude are possible and show that we can achieve significant speedups for a reliability analysis.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

SWITSS: Computing Small Witnessing Subsystems

Witnessing subsystems for probabilistic reachability thresholds in discrete Markovian models are an important concept both as diagnostic information on why a property holds, and as input to refinement algorithms. We present SWITSS, a tool for the computation of Small WITnessing SubSystems. SWITSS implements exact and heuristic approaches based on reducing the problem to (mixed integer) linear programming. Returned subsystems can automatically be rendered graphically and are accompanied with a certificate which proves that the subsystem is indeed a witness.

0 citations0 reviewsNo code linkedOpen access