Master Thesis: (Oliver Markgraf)
Synthesis for parameterized Systems
Abstract:
Parameterized synthesis offers a solution to the problem of constructing correct and verified controllers for parameterized systems. These systems occur naturally in practice (e.g., in the form of distributed protocols where the amount of processes is often unknown at design time and the protocol must work regardless of the number of processes participating). In this thesis, we present a novel learning-based approach to the synthesis of reactive controllers for parameterized systems from safety specifications. We use the framework of regular model checking (i.e., synchronous automata) to model the synthesis problem as an infinite-duration two-player game and show how one can utilize Angluin’s wellknown L* algorithm to learn correct-by-design controllers. This approach results in a synthesis procedure that is conceptually simpler than existing synthesis methods and that guarantees to construct a reactive safety controller if a strategy for the controller can be expressed by a regular set. In contrast to existing methods, we use active learning instead of passive learning, equipping the learner with additional tools to accelerate the learning process. We have implemented our algorithm in a tool called L* -PSynth and have demonstrated its performance on a range of benchmarks, including robotic motion planning and distributed protocols. Despite the relative simplicity of L* -PSynth, it outperforms the stateof-the-art tools for synthesizing parameterized systems on 7 out of 9 benchmarks.
Master Thesis: (Pascal Bergsträßer)
A sufficient condition for decidability of the knapsack problem in wreath products of groups
Abstract:
The knapsack problem over a group G asks whether a given equation g1x1, . . . , gnxn= g with elements g1, . . . , gn, g ∈ G has a solution setting the variables xi to non-negative integers. Unlike the classical discrete optimization problem where G = ℤ the knapsack problem turns out to be undecidable over some non-commutative groups. There is no complete characterization for decidability of the knapsack problem in the non-commutative setting yet. An interesting construction that does not preserve decidability of the knapsack problem in general is the wreath product. As a main result of this thesis we obtain a sufficient condition for decidability of the knapsack problem in wreath products. We show that the knapsack problem over a wreath product G≀H is decidable if solvability of exponent equations is decidable over G and either G is abelian and KP+(H) is decidable or G is non-abelian and KP±(H) is decidable. Here, KP+ and KP± are two newly defined decision problems. Thus, we gain an approach to tackle decidablility of the knapsack problem over wreath products that allows us to consider the groups G and H separately. As an application of our main result we show that the knapsack problem over G≀BS(1, q) with q ≥ 1 is decidable if solvability of exponent equations is decidable over G.
Master Thesis:
Interpreting Register Automata and other Sequential Models
Abstract:
In this thesis, the counterfactual query is used to determine formal interpretability for various sequential models. Given a binary classification of a sequence by a model, a counterfactual query asks: Does a similar word exist, that is classified differently? This research demonstrates, that answering such queries is NP-Hard (or even undecidable) for recurrent neural networks (RNN) and transformers, but can be done in polynomial time for interval automata and register automata (for a fixed number of registers), even when these models are assumed to operate on the infinite domain of rational numbers. These queries are considered with respect to different similarity measures, namely Hamming distance, edit distance and dynamic time warping (DTW). Furthermore, I have implemented a polynomial time algorithm, that answers counterfactual queries of register automata with respect to DTW, as a python package. Lastly, a generalization of counterfactual queries for interval and register automata to the coverability problem for register automata with an accumulator is given, as well as a proof that this too can be solved in polynomial time (for a fixed number of registers).
Bachelor Thesis, 2024: (by Erdem Yildirim)
Formalisation and Development of Type Checking for Restricted and Unrestricted Maps with Set-theoretic Types in Erlang
Abstract:
Erlang is a functional language for programming dis- tributed systems. Erlang itself is dynamically typed but many static type analysis tools exist. One of them is etylizer [SWB23] with a mathematically sound type system based on set-theoretic types and semantic sub- typing. This thesis presents an enrichment of its type system by including Erlang’s parametric map types. The syntax of these types are flexible to a degree of ambiguity whence the need arises for imposing restrictions on their syntax. As a result, we obtain restricted and unrestricted map types. Integrating parametric maps into the type system of etylizer boils down to finding set-theoretic interpretations for them. These interpretations can be used to solve subtyping problems which are set containment problems in case of semantic subtyping.
1st place ACM Student research competition @Programming 2024, Undergraduate Category
Master Thesis:
Variable Independence in Linear Real Arithmetic
Abstract:
Variable independence and decomposability are algorithmic techniques for simplifying logical formulas by tearing apart connections between free variables. These techniques were originally proposed to speed up query evaluation in constraint databases, in particular by representing the query as a Boolean combination of formulas with no interconnected variables. They also have many other applications in SMT, string analysis, databases, automata theory and other areas. However, the precise complexity of variable independence and decomposability has been left open especially for the quantifier-free theory of linear real arithmetic (LRA), which is central in database applications. We introduce a novel characterization of formulas admitting decompositions and use it to show that it is coNP-complete to decide variable decomposability over LRA. As a corollary, we obtain that deciding variable independence is in the second level of the polynomial hierarchy. These results substantially improve the best known double exponential time algorithms for variable decomposability and independence. In many practical applications, it is important not only to decide variable independence/decomposability algorithmically but also to be able to efficiently eliminate connections between variables whenever possible. We design and implement an algorithm for this problem, which is optimal in theory, exponentially faster compared to the current state-of-the-art algorithm and efficient on various microbenchmarks. In particular, our algorithm is the first one to overcome a fundamental barrier between nondiscrete and discrete first-order theories (for the latter, the problem is significantly easier, and many techniques yielding efficient algorithms are known). Formulas arising in practice often have few or even no free variables that are perfectly independent. In this case, our algorithm can compute a best-possible approximation of a decomposition, which can be used to optimize database queries by exploiting partial variable independence, which is present in almost every logical formula or database query constraint.
Master Thesis:
Program Synthesis for TLA+ Specifications of Actor-Based Distributed Systems
Abstract:
Distributed systems are notoriously difficult to design and implement correctly. Although formal methods provide rigorous approaches to verifying the adherence of a program to its specification, there still exists a gap between a formal model and implementation if the model and its implementation are only loosely coupled. Developers usually overcome this gap through manual effort, which may result in the introduction of unexpected bugs. This master’s thesis presents Erla+, a translator that automatically translates models written in a subset of the PlusCal language to TLA+ for formal reasoning and produces executable Erlang programs in one run. Erla+ additionally provides new PlusCal primitives for actor-style modeling, thus clearly separating the modeled system from its environment. To increase confidence in Erla+’s generated Erlang im- implementations, we propose a model-based test case generation technique that compares the implementation’s runtime states to those of its verified model. We show the expressivity and strengths of Erla+ by applying it to representative use cases such as a Raft-based key-value store. Our evaluation shows that the implementations generated by Erla+ offer competitive performance against manually written and optimized state-of-the-art libraries.
Master Thesis, 2024:
The Complexity of the Equivalence Problem for Deterministic Rational Relations
Abstract:
We study the equivalence problem for deterministic rational relations, which are relations over finite strings presented by deterministic multi-tape automata: Given two deterministic multi-tape automata, do they recognize the same relation? While the problem is known to be decidable, the precise complexity is an open problem. In this thesis we study two known approaches to solve this problem, which are of combinatorial and of algebraic nature. The combinatorial algorithm solves the equivalence problem for binary relations in time O(n4). We provide a refined version, improving the time complexity to O(n3 α(n)), where α(n) is the inverse Ackermann function, which grows extremely slowly. The algebraic approach provides a randomized polynomial-time algorithm for the equivalence problem over relations of arbitrary arity. We improve on this result by showing that the algorithm can be implemented in randomized parallel polylogarithmic time using a computer with a polynomial number of processors. Additionally, we study the string tuples that distinguishing two inequivalent multi-tape automata and obtain upper bounds on the shortest distinguishing tuples purely by combinatorial means.
Master Thesis, 2024:(by Munko Tsyrempilon, supervised by I. Saglam & A. Schmuck)
A Decremental Algorithm for Fair Büchi Games
The paper resulting from this work will appear at ATVA’24 and received a distinguished paper recognition there.
Abstract:
This paper provides the first decremental algorithm for fair Büchi games. It efficiently recalculates the winning region under the deletion of live edges in the underlying game graph. Our algorithm addresses the unique challenges posed by fair Büchi games such as exponential-memory strategies and the non-monotonicity of the winning region under edge deletion. This prevents a straight forward ex- tension of dynamic algorithms from (normal) Büchi games, in particular Jurdziński’s small progress measures, on which these algorithms rely. The main contribution of this paper is the definition of a specialized (one- digit) progress measure for fair Büchi games and its correctness proof. We further derive a decremental algorithm for fair Büchi games using a fixed-point calculation entailed by this progress measure. We show that the (non-optimized) prototype implementation of our decremental algorithm outperforms an (optimized) fair Büchi game solver on a large class of benchmarks. By this, our work not only expands the scope of dynamic algorithms but also underscores the benefit of tailored solutions for specific game structures such as fair Büchi games.
Master Thesis, 2023: (by Mehrdad Zareian supervised by A. Schmuck)
Lazy Synthesis of Symbolic Output-Feedback Controllers for State-Based Safety Specifications
Abstract:
The resulting paper appeared at HSCC’23 Paper
This thesis presents a lazy symbolic output-feedback controller synthesis algorithm for state-based safety specifications over large transition systems. The novel idea of our approach is to integrate an iterative algorithm for observer design with an online adaptable safety controller synthesis algorithm. This allows us to iteratively update the safety controller to observer refinements and to guide these refinements by the existing controller. This results in efficient lazy synthesis of a safety controller whose domain increases with the time spent in synthesis. We present simulation results for a synthetic robot motion planning example showing the benefits of our algorithm compared to the standard approach.
Guided research projects
- Yanakieva, E., Youssef, M., Rezae, A.H., Bieniusa, A. (2021). On the Impossibility of Confidentiality, Integrity and Accessibility in Highly-Available File Systems. In: Echihabi, K., Meyer, R. (eds) Networked Systems. NETYS 2021. Lecture Notes in Computer Science(), vol 12754. Springer, Cham.
https://doi.org/10.1007/978-3-030-91014-3_1 (Best student paper award)
- Bounding the Size of Monadic Decompositions of Automatic Relations, Guided research project, 2024.
PhD Thesis
- Tool Supported Specification and Verification of Highly Available Applications. (by Peter Zeller, 2021)