Searcharxiv⌕ Search

arXiv subjects

Erika Ábrahám

Publications and source records attributed to Erika Ábrahám.

At least 19 recordsLinked to original sources

Attribution-based Explanations for Markov Decision Processes

Attribution techniques explain the outcome of an AI model by assigning a numerical score to its inputs. So far, these techniques have mainly focused on attributing importance to static input features at a single point in time, and thus fail to generalize to sequential decision-making settings. This paper fills this gap by introducing techniques to generate attribution-based explanations for Markov Decision Processes (MDPs). We give a formal characterization of what attributions should represent in MDPs, focusing on explanations that assign importance scores to both individual states and execution paths. We show how importance scores can be computed by leveraging techniques for strategy synthesis, enabling the efficient computation of these scores despite the non-determinism inherent in an MDP. We evaluate our approach on five case-studies, demonstrating its utility in providing interpretable insights into the logic of sequential decision-making agents.

cs.AI↗

Minimum Reachability Probabilities in Rectangular Automata with Random Clocks

Control applications for cyber-physical systems must make reliably safe control decisions in the presence of continuous dynamics as well as stochastic uncertainty. Providing safety guarantees for such systems requires formal modeling and analysis techniques that capture these aspects. For modeling, in this paper we consider rectangular automata with random clocks under prophetic scheduling. For this model class, existing methods can compute only upper bounds on reachability probabilities, enabling optimistic, best-case safety reasoning. We complement this view by introducing a novel method to compute lower bounds, thereby enabling worst-case analysis that is essential for safety-critical applications. Although both upper and lower bounds rely on reachability analysis, they are not dual: computing lower bounds requires an explicit separation of stochastic and nondeterministic choices along executions. We implement our approach and demonstrate its practical feasibility on an electric vehicle charging scenario, showing that meaningful worst-case guarantees can be obtained.

cs.FL↗

Tractable Hyperproperties for MDPs

Probabilistic hyperproperties describe probabilistic relations between multiple sets of executions in a stochastic system. Prominent examples include information-theoretic characterizations of security and privacy policies. However, model checking for existing probabilistic hyperlogics, such as HyperPCTL and PHL, is undecidable in Markov decision processes (MDPs). In this paper, we study an underexplored problem: the verification of fragments of probabilistic hyperproperties that relate the probabilities of different events to each other, possibly across independent executions of an MDP. Representative verification questions include: Can two different target states be reached from the same initial state with the same probability? (different events), Can a given target state be reached from two different initial states with the same probability? (same event, independent executions), and natural combinations of these forms. Besides reachability, our relational probabilistic properties cover safety, Büchi, and coBüchi objectives. They can also be combined conjunctively, thereby generalizing standard multi-objective MDP properties. We provide efficient algorithms for relevant classes of relational properties, while proving computational hardness and completeness results for others. An implementation of our approach outperforms solvers for more general probabilistic hyperlogics by orders of magnitude on the subset of their benchmarks that lies within our fragment.

cs.LO↗

More is Less: Adding Polynomials for Faster Explanations in NLSAT

To check the satisfiability of (non-linear) real arithmetic formulas, modern satisfiability modulo theories (SMT) solving algorithms like NLSAT depend heavily on single cell construction, the task of generalizing a sample point to a connected subset (cell) of $\mathbb{R}^n$, that contains the sample and over which a given set of polynomials is sign-invariant. In this paper, we propose to speed up the computation and simplify the representation of the resulting cell by dynamically extending the considered set of polynomials with further linear polynomials. While this increases the total number of (smaller) cells generated throughout the algorithm, our experiments show that it can pay off when using suitable heuristics due to the interaction with Boolean reasoning.

cs.SC↗

Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks

This paper presents optimizations to improve the scalability of reachability analysis on a subclass of hybrid automata extended with stochasticity. The optimizations target different components of the analysis, such as quantifier elimination for state set projection, and automated parameter selection during the numerical integration. Most importantly, whereas the original method combines forward and backward reachability, we show that the usage of backward reachability is optional for computing maximal reachability probabilities.

cs.SC↗

A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination

The Cylindrical Algebraic Decomposition (CAD) method is currently the only complete algorithm used in practice for solving real-algebraic problems. To ameliorate its doubly-exponential complexity, different exploration-guided adaptations try to avoid some of the computations. The first such adaptation named NLSAT was followed by Non-uniform CAD (NuCAD) and the Cylindrical Algebraic Covering (CAlC). Both NLSAT and CAlC have been developed and implemented in SMT solvers for satisfiability checking, and CAlC was recently also adapted for quantifier elimination. However, NuCAD was designed for quantifier elimination only, and no complete implementation existed before this work. In this paper, we present a novel variant of NuCAD for both real quantifier elimination and SMT solving, provide an implementation, and evaluate the method by experimentally comparing it to CAlC.

cs.SC↗

Projective Delineability for Single Cell Construction

The cylindrical algebraic decomposition (CAD) is the only complete method used in practice for solving problems like quantifier elimination or SMT solving related to real algebra, despite its doubly exponential complexity. Recent exploration-guided algorithms like NLSAT, NuCAD, and CAlC rely on CAD technology but reduce the computational effort heuristically. Single cell construction is a paradigm that is used in each of these algorithms. The central property on which the CAD algorithm is based is called delineability. Recently, we introduced a weaker notion called projective delineability which can require fewer computations to guarantee, but needs to be applied carefully. This paper adapts the single cell construction for exploiting projective delineability and reports on experimental results.

cs.SC↗

Why do women pursue a PhD in Computer Science?

Computer science attracts few women, and their proportion decreases through advancing career stages. Few women progress to PhD studies in CS after completing master's studies. Empowering women at this stage in their careers is essential to unlock untapped potential for society, industry and academia. This paper identifies students' career assumptions and information related to PhD studies focused on gender-based differences. We propose a Women Career Lunch program to inform female master students about PhD studies that explains the process, clarifies misconceptions, and alleviates concerns. An extensive survey was conducted to identify factors that encourage and discourage students from undertaking PhD studies. We identified statistically significant differences between those who undertook PhD studies and those who didn't, as well as gender differences. A catalogue of questions to initiate discussions with potential PhD students which allowed them to explore these factors was developed and translated to 8 languages. Encouraging factors toward PhD study include interest and confidence in research arising from a research involvement during earlier studies; enthusiasm for and self-confidence in CS in addition to an interest in an academic career; encouragement from external sources; and a positive perception towards PhD studies which can involve achieving personal goals. Discouraging factors include uncertainty and lack of knowledge of the PhD process, a perception of lower job flexibility, and the requirement for long-term commitment. Gender differences highlighted that female students who pursue a PhD have less confidence in their technical skills than males but a higher preference for interdisciplinary areas. Female students are less inclined than males to perceive the industry as offering better job opportunities and more flexible career paths than academia.

cs.CY↗

A Hyperlogic for Strategies in Stochastic Games (Extended Version)

We propose a probabilistic hyperlogic called HyperSt$^2$ that can express hyperproperties of strategies in turn-based stochastic games. To the best of our knowledge, HyperSt$^2$ is the first hyperlogic for stochastic games. HyperSt$^2$ can relate probabilities of several independent executions of strategies in a stochastic game. For example, in HyperSt$^2$ it is natural to formalize optimality, i.e., to express that some strategy is better than all other strategies, or to express the existence of Nash equilibria. We investigate the expressivity of HyperSt$^2$ by comparing it to existing logics for stochastic games, as well as existing hyperlogics. Though the model-checking problem for HyperSt$^2$ is in general undecidable, we show that it becomes decidable for bounded memory and is in EXPTIME and PSPACE-hard over memoryless deterministic strategies, and we identify a fragment for which the model-checking problem is PSPACE-complete.

cs.LO↗

Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)

Markov decision processes model systems subject to nondeterministic and probabilistic uncertainty. A plethora of verification techniques addresses variations of reachability properties, such as: Is there a scheduler resolving the nondeterminism such that the probability to reach an error state is above a threshold? We consider an understudied extension that relates different reachability probabilities, such as: Is there a scheduler such that two sets of states are reached with different probabilities? These questions appear naturally in the design of randomized algorithms and in various security applications. We provide a tractable algorithm for many variations of this problem, while proving computational hardness of some others. An implementation of our algorithm beats solvers for more general probabilistic hyperlogics by orders of magnitude, on the subset of their benchmarks that are within our fragment.

cs.LO↗

Counterfactual Strategies for Markov Decision Processes

Counterfactuals are widely used in AI to explain how minimal changes to a model's input can lead to a different output. However, established methods for computing counterfactuals typically focus on one-step decision-making, and are not directly applicable to sequential decision-making tasks. This paper fills this gap by introducing counterfactual strategies for Markov Decision Processes (MDPs). During MDP execution, a strategy decides which of the enabled actions (with known probabilistic effects) to execute next. Given an initial strategy that reaches an undesired outcome with a probability above some limit, we identify minimal changes to the initial strategy to reduce that probability below the limit. We encode such counterfactual strategies as solutions to non-linear optimization problems, and further extend our encoding to synthesize diverse counterfactual strategies. We evaluate our approach on four real-world datasets and demonstrate its practical viability in sophisticated sequential decision-making tasks.

cs.AI↗

FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex

In this paper we present a quantifier elimination method for conjunctions of linear real arithmetic constraints. Our algorithm is based on the Fourier-Motzkin variable elimination procedure, but by case splitting we are able to reduce the worst-case complexity from doubly to singly exponential. The adaption of the procedure for SMT solving has strong correspondence to the simplex algorithm, therefore we name it FMplex. Besides the theoretical foundations, we provide an experimental evaluation in the context of SMT solving. This is an extended version of the authors' work previously published at the fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023).

cs.SC↗

Hybrid Rebeca Revisited

Hybrid Rebeca is a modeling framework for asynchronous event-based cyber-physical systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. Besides the syntactical extension, we formalize the semantics of the extended language in terms of Timed Transition Systems, and adapt a reachability analysis algorithm originally designed for hybrid automata to be applicable to Hybrid Rebeca models. We prove the soundness of our approach and illustrate its applicability on a case study. The case study demonstrates that our dedicated algorithm is clearly superior to the alternative approach of transforming Hybrid Rebeca models to hybrid automata as an intermediate model and then applying the original reachability analysis method to this intermediate transformed models.

cs.FL↗

On Projective Delineability

We consider cylindrical algebraic decomposition (CAD) and the key concept of delineability which underpins CAD theory. We introduce the novel concept of projective delineability which is easier to guarantee computationally. We prove results about this which can allow reduced CAD computations.

math.AG↗

ROSAR: An Adversarial Re-Training Framework for Robust Side-Scan Sonar Object Detection

This paper introduces ROSAR, a novel framework enhancing the robustness of deep learning object detection models tailored for side-scan sonar (SSS) images, generated by autonomous underwater vehicles using sonar sensors. By extending our prior work on knowledge distillation (KD), this framework integrates KD with adversarial retraining to address the dual challenges of model efficiency and robustness against SSS noises. We introduce three novel, publicly available SSS datasets, capturing different sonar setups and noise conditions. We propose and formalize two SSS safety properties and utilize them to generate adversarial datasets for retraining. Through a comparative analysis of projected gradient descent (PGD) and patch-based adversarial attacks, ROSAR demonstrates significant improvements in model robustness and detection accuracy under SSS-specific conditions, enhancing the model's robustness by up to 1.85%. ROSAR is available at https://github.com/remaro-network/ROSAR-framework.

cs.CV↗

Knowledge Distillation in YOLOX-ViT for Side-Scan Sonar Object Detection

In this paper we present YOLOX-ViT, a novel object detection model, and investigate the efficacy of knowledge distillation for model size reduction without sacrificing performance. Focused on underwater robotics, our research addresses key questions about the viability of smaller models and the impact of the visual transformer layer in YOLOX. Furthermore, we introduce a new side-scan sonar image dataset, and use it to evaluate our object detector's performance. Results show that knowledge distillation effectively reduces false positives in wall detection. Additionally, the introduced visual transformer layer significantly improves object detection accuracy in the underwater environment. The source code of the knowledge distillation in the YOLOX-ViT is at https://github.com/remaro-network/KD-YOLOX-ViT.

cs.CV↗

Extending Neural Network Verification to a Larger Family of Piece-wise Linear Activation Functions

In this paper, we extend an available neural network verification technique to support a wider class of piece-wise linear activation functions. Furthermore, we extend the algorithms, which provide in their original form exact respectively over-approximative results for bounded input sets represented as start sets, to allow also unbounded input set. We implemented our algorithms and demonstrated their effectiveness in some case studies.

cs.LG↗

Parameter Synthesis for Markov Models: Covering the Parameter Space

Markov chain analysis is a key technique in formal verification. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such as failure rates or packet loss ratios, etc. are often not -- or only partially -- known. This motivates considering parametric models with transitions labeled with functions over parameters. Whereas traditional Markov chain analysis relies on a single, fixed set of probabilities, analysing parametric Markov models focuses on synthesising parameter values that establish a given safety or performance specification $φ$. Examples are: what component failure rates ensure the probability of a system breakdown to be below 0.00000001?, or which failure rates maximise the performance, for instance the throughput, of the system? This paper presents various analysis algorithms for parametric discrete-time Markov chains and Markov decision processes. We focus on three problems: (a) do all parameter values within a given region satisfy $φ$?, (b) which regions satisfy $φ$ and which ones do not?, and (c) an approximate version of (b) focusing on covering a large fraction of all possible parameter values. We give a detailed account of the various algorithms, present a software tool realising these techniques, and report on an extensive experimental evaluation on benchmarks that span a wide range of applications.

cs.LO↗