Falk Howar

Simon Lutz, Daniil Kaminskyi, Florian Wittbold et al.

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.

Malte Hellmeier, Hendrik Norkowski, Ernst-Christoph Schrewe et al.

Large language models (LLMs) have gained significant popularity in recent years. Differentiating between a text written by a human and one generated by an LLM has become almost impossible. Information-hiding techniques such as digital watermarking or steganography can help by embedding information inside text in a form that is unlikely to be noticed. However, existing techniques, such as linguistic-based or format-based methods, change the semantics or cannot be applied to pure, unformatted text. In this paper, we introduce a novel method for information hiding called Innamark, which can conceal any byte-encoded sequence within a sufficiently long cover text. This method is implemented as a multi-platform library using the Kotlin programming language, which is accompanied by a command-line tool and a web interface. By substituting conventional whitespace characters with visually similar Unicode whitespace characters, our proposed scheme preserves the semantics of the cover text without changing the number of characters. Furthermore, we propose a specified structure for secret messages that enables configurable compression, encryption, hashing, and error correction. An experimental benchmark comparison on a dataset of 1 000 000 Wikipedia articles compares ten algorithms. The results demonstrate the robustness of our proposed Innamark method in various applications and the imperceptibility of its watermarks to humans. We discuss the limits to the embedding capacity and robustness of the algorithm and how these could be addressed in future work.

Eric Fiege, Salima Houta, Pinar Bisgin et al.

Documentation of epileptic seizures plays an essential role in planning medical therapy. Solutions for automated epileptic seizure detection can help improve the current problem of incomplete and erroneous manual documentation of epileptic seizures. In recent years, a number of wearable sensors have been tested for this purpose. However, detecting seizures with subtle symptoms remains difficult and current solutions tend to have a high false alarm rate. Seizures can also affect the patient's arterial blood pressure, which has not yet been studied for detection with sensors. The pulse transit time (PTT) provides a noninvasive estimate of arterial blood pressure. It can be obtained by using to two sensors, which are measuring the time differences between arrivals of the pulse waves. Due to separated time chips a clock drift emerges, which is strongly influencing the PTT. In this work, we present an algorithm which responds to alterations in the PTT, considering the clock drift and enabling the noninvasive monitoring of blood pressure alterations using separated sensors. Furthermore we investigated whether seizures can be detected using the PTT. Our results indicate that using the algorithm, it is possible to detect seizures with a Random Forest. Using the PTT along with other signals in a multimodal approach, the detection of seizures with subtle symptoms could thereby be improved.

Adina Aniculaesei, Daniel Arnsberger, Falk Howar et al.

There is an increasing necessity to deploy autonomous systems in highly heterogeneous, dynamic environments, e.g. service robots in hospitals or autonomous cars on highways. Due to the uncertainty in these environments, the verification results obtained with respect to the system and environment models at design-time might not be transferable to the system behavior at run time. For autonomous systems operating in dynamic environments, safety of motion and collision avoidance are critical requirements. With regard to these requirements, Macek et al. [6] define the passive safety property, which requires that no collision can occur while the autonomous system is moving. To verify this property, we adopt a two phase process which combines static verification methods, used at design time, with dynamic ones, used at run time. In the design phase, we exploit UPPAAL to formalize the autonomous system and its environment as timed automata and the safety property as TCTL formula and to verify the correctness of these models with respect to this property. For the runtime phase, we build a monitor to check whether the assumptions made at design time are also correct at run time. If the current system observations of the environment do not correspond to the initial system assumptions, the monitor sends feedback to the system and the system enters a passive safe state.

Guillaume Brat, David Bushnell, Misty Davies et al.

This paper describes our work on demonstrating verification technologies on a flight-critical system of realistic functionality, size, and complexity. Our work targeted a commercial aircraft control system named Transport Class Model (TCM), and involved several stages: formalizing and disambiguating requirements in collaboration with do- main experts; processing models for their use by formal verification tools; applying compositional techniques at the architectural and component level to scale verification. Performed in the context of a major NASA milestone, this study of formal verification in practice is one of the most challenging that our group has performed, and it took several person months to complete it. This paper describes the methodology that we followed and the lessons that we learned.