Automata learning is a successful tool for many application domains such as robotics and automatic verification. Typically, automata learning techniques operate in a supervised learning setting (active or passive) where they learn a finite state machine in contexts where additional information, such as labeled system executions, is available. However, other settings, such as learning from unlabeled data - an important aspect in machine learning - remain unexplored. To overcome this limitation, we propose a framework for learning a deterministic finite automaton (DFA) from a given multi-set of unlabeled words. We show that this problem is computationally hard and develop three learning algorithms based on constraint optimization. Moreover, we introduce novel regularization schemes for our optimization problems that improve the overall interpretability of our DFAs. Using a prototype implementation, we demonstrate practical feasibility in the context of unsupervised anomaly detection.

Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this paper, we present SL^λ, an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of tests required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We have implemented SL^λ as a new algorithm in RALib. We evaluate its performance by comparing it against SL^*, the current state-of-the-art RA learning algorithm, in a series of experiments, and show superior performance and substantial asymptotic improvements in bigger systems.

We present a technique for learning explainable timed automata from passive observations of a black-box function, such as an artificial intelligence system. Our method accepts a single, long, timed word with mixed input and output actions and learns a Mealy machine with one timer. The primary advantage of our approach is that it constructs a symbolic observation tree from a concrete timed word. This symbolic tree is then transformed into a human comprehensible automaton. We provide a prototype implementation and evaluate it by learning the controllers of two systems: a brick-sorter conveyor belt trained with reinforcement learning and a real-world derived smart traffic light controller. We compare different model generators using our symbolic observation tree as their input and achieve the best results using k-tails. In our experiments, we learn smaller and simpler automata than existing passive timed learners while maintaining accuracy.

Register automata are an expressive model of computation using finite memory. Conformance checking of their properties can be reduced to N O N E M P T I N E S S tests, however, this problem is PSPACE -complete. Existing approaches usually employ symbolic state exploration. This results in state explosion for most complex register automata. We propose a semantics-preserving transformation of register automata into a representation in which reachability of states is equivalent to reachability of locations, i.e., is in NL . We evaluate the algorithm on random-generated and real-world automata and show that it avoids state explosion and performs better on most instances than a comparable existing approach. This yields a practical approach to conformance checking of register automata.

In this paper, we present SPouT, a concolic executor for the Java virtual machine. To the user, SPouT is a java executable that takes some additional parameters for setting the values of concolic inputs and produces symbolic traces over variables under observation during the execution. Technically, SPouT extends the JVM implementation provided by the Espresso guest language for the GraalVM. Therefore, SPouT is the first concolic executor build on an industrial JVM. In this paper, we describe the architectural design of SPouT, detail how the partial symbolic analysis of Java ’s strings is implemented in SPouT, and show its performance and versatility by comparing it to other analysis tools for Java programs.

Register automata are an expressive model of computation using finite memory. Conformance checking of their properties can be reduced to $$\textsc {NonEmptiness}$$ tests, however, this problem is $$\mathsf {PSPACE}$$ -complete. Existing approaches usually employ symbolic state exploration. This results in state explosion for most complex register automata. We propose a semantics-preserving transformation of register automata into a representation in which reachability of states is equivalent to reachability of locations, i.e., is in $$\mathsf {NL}$$ . We evaluate the algorithm on random-generated and real-world automata and show that it avoids state explosion and performs better on most instances than a comparable existing approach. This yields a practical approach to conformance checking of register automata.

It is widely accepted by now that the discipline of Software Engineering is distinct from both Computer Science and Electrical Engineering, and that it requires bespoke higher education programs. In this paper, we argue that previous attempts at designing such programs have often failed to fully account for three essential characteristics of the discipline. We propose a design philosophy for undergraduate Software Engineering programs addressing these particularities and outline a corresponding program. Incorporating this philosophy would make Generation Alpha the first generation to receive a genuine Software Engineering education.

Register automata model languages over infinite alphabets. A number of publications define different register automata formalisms. Equal expressiveness has been conjectured for many formalisms but a formal analysis is still open. In this paper on the occasion of the \(63^\mathrm{rd}\) birthday of Bengt Jonsson we examine if these formalisms are equally expressive. We define a taxonomy to describe the different formalisms. By combining small-step reductions, we demonstrate that all models have equal expressiveness. We link these to model-specific complexity results for the \(\textsc {NonEmptiness}\) problem and decide which taxonomy features determine the complexity of \(\textsc {NonEmptiness}\). The taxonomy enables formal classification of future models. The reductions permit transfer of formalism-specific results to other formalisms.

Software faults are still a problem especially in deployed systems. We propose a new approach to monitor a deployed embedded system with another embedded system, which acts autonomously and isolated. The monitoring system generates reports containing probable fault locations, which can later be obtained without requiring expensive debugging hardware or continuous access to the monitored embedded system. For this, we assessed failure-detection oracles, transaction detectors and suspiciousness metrics and evaluated them in a practical combustion engine scenario. Especially, we propose a driver interaction model to capture correct interaction with periphery and use it as oracle. Our results show that for the repetitive behavior of an engine control unit, simple approaches perform best.