KiMeKo (KI-Med-Kollaborationsplattform) is a publically funded collaborative research project that develops a sustainable AI-Med ecosystem for AI-based medical device development. The project runs from July 2024 to December 2027 and joins seven Northern German research institutions. KiMeKo addresses the complete development trajectory, from concept and data acquisition to validation, regulatory evidence generation, and approval-oriented documentation. The project contributes a practical toolchain and platform capabilities for non-experts and experts, including structured innovation support, uncertaintyaware sensor-data fusion, hybrid expert-system modeling, and workflow-guided data acquisition and anonymization. This paper summarizes project objectives, expected outputs, relevance to IEEE COMPSAC 2026 themes, and current progress. In particular, KiMeKo aligns with Applied AI and Smart & Connected Health by combining AI engineering, privacy-conscious data processing, and regulation-aware medical software development.

Runtime verification (RV) examines whether a system’s run satisfies its specification. This typically requires full knowledge of the run, but many applications face imprecise or missing inputs, e.g., from noisy sensors. We aim to develop a symbolic RV procedure that can handle noisy inputs and is able to exploit assumptions that encode background knowledge about the system in order to produce reliable monitoring verdicts. As the symbolic setting in general induces increasingly large monitoring states, we aim to identify fragments of specifications where monitoring requires constant memory. After providing a formalization of the problem at hand, we propose an RV procedure and give formal correctness statements and proofs. We empirically validate our approach in two realistic case studies. The developed RV procedure is the first to effectively handle both uncertainties and assumptions in the expressive setting of Lola, and we identify relevant and expressive fragments where our procedure requires constant memory. Our evaluation witnesses the practical applicability of the approach. RV with uncertainties and assumptions is feasible in the Lola setting, and needs only constant memory in some relevant fragments. Future work will explore further theories and adapt the approach to specific applications.

Deep learning has seen significant progress in applications such as autonomous driving and healthcare, with synthetic data playing an increasingly important role. However, models trained on synthetic data often suffer performance drops in real-world settings due to domain shifts. Domain Generalization (DG) aims to address this problem by developing models that can robustly generalize to unseen domains, with a key challenge being the selection of an appropriate checkpoint. For the checkpoint selection problem, we introduce a standardized approach that simultaneously enhances model robustness through the combination of Exponential Moving Average (EMA) and Data Augmentation. Our method reduces performance variability and improves generalization in 25 out of 26 experiments, highlighting EMA as a promising technique for more stable and reliable DG performance in real-world applications.

Abstract Runtime verification is a technique for monitoring a system’s behavior against a formal specification. Monitors must produce verdicts that are sound with respect to the specification. Anticipation is the ability to immediately produce verdicts when the monitor can confidently predict the inevitability of the verdict. Stream runtime verification is a specialized form of runtime verification tailored to the monitoring and verification of data streams. In this paper we study anticipatory monitoring for stream runtime verification. More specifically, we present an algorithm with anticipation for monitoring of Lola specifications, which we then extend to exploit assumptions and tolerate uncertainties. As perfect anticipation is in general not computable, we use techniques from abstract interpretation, especially widening, to approximate anticipatory monitoring verdicts. Finally, we report on three empirical cases studies using a prototype implementation of a symbolic instantiation of our approach.

We present a study to assess the feasibility and implications of replacing internal combustion engine vehicles with battery-powered electric vehicles (EVs) in a car-sharing fleet. For the analysis, we used operational data from a local car-sharing company, which encompasses various aspects such as trip distance, start and duration, vehicle type, and pickup and return locations. To evaluate the impact of transitioning the entire fleet to EVs, we used EV and charger models to simulate the battery-powered trips and also the necessary post-trip recharging. Both could affect the service quality of car sharing services, as the requested trip distance might not be covered by an electric vehicle due to range or charging time limitations. Specifically, in our simulation-based analysis, we identified chains of consecutive bookings as a critical factor for car-sharing electrification. Furthermore, to assess the potential impact of electrification on the energy grid, we used data about the local grid load and its composition to relate it to the predicted vehicle charging times.

In this paper, we study the concept of conflict in the setting of timed normative logical specification languages. To this end, we introduce the Flat Monadic Metric Time Normative Logic suitable for specifying the behavior of basic timed normative systems using sets of intervals. We provide a characterization of normative conflicts by the satisfiability of the formula and its sub-formulas. Moreover, an SMT-based satisfiability procedure for FMMTNL is provided.

Angluin's L$^*$ algorithm learns the minimal deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximatively correct (PAC) version substitutes an equivalence query by numerous random membership queries to get a high level confidence to the answer. Thus it can be applied to any kind of device and may be viewed as an algorithm for synthesizing an automaton abstracting the behavior of the device based on observations. Here we are interested on how Angluin's PAC learning algorithm behaves for devices which are obtained from a DFA by introducing some noise. More precisely we study whether Angluin's algorithm reduces the noise and produces a DFA closer to the original one than the noisy device. We propose several ways to introduce the noise: (1) the noisy device inverts the classification of words w.r.t. the DFA with a small probability, (2) the noisy device modifies with a small probability the letters of the word before asking its classification w.r.t. the DFA, (3) the noisy device combines the classification of a word w.r.t. the DFA and its classification w.r.t. a counter automaton, and (4) the noisy DFA is obtained by a random process from two DFA such that the language of the first one is included in the second one. Then when a word is accepted (resp. rejected) by the first (resp. second) one, it is also accepted (resp. rejected) and in the remaining cases, it is accepted with probability 0.5. Our main experimental contributions consist in showing that: (1) Angluin's algorithm behaves well whenever the noisy device is produced by a random process, (2) but poorly with a structured noise, and, that (3) is able to eliminate pathological behaviours specified in a regular way. Theoretically, we show that randomness almost surely yields systems with non-recursively enumerable languages.

Abstract This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning. This model may then be analyzed using model checking as a verification technique. The term property-directed reflects the idea that our procedure is guided and controlled by the given property rather than performing the two steps separately. We show that this not only allows us to discover small counterexamples fast, but also to generalize them by pumping toward faulty flows hinting at the underlying error in the RNN. We also show that our method can be efficiently used for adversarial robustness certification of RNNs.

Dataflow languages have, as well as functional languages, immutable semantics, which is often implemented by copying values. A common compiler optimization known from functional languages involves analyzing which data structures can be modified in-place instead of copying them. This paper presents a novel algorithm to this so called Aggregate Update Problem for multi-clocked dataflow languages, i.e. those that allow streams to have events at disjoint timestamps, like e.g. Lucid, Lustre and Signal. Unrestricted multi-clocked languages require a static triggering analysis on how events and hence data values are read, written and replicated. We use TeSSLa as a generic stream transformation language with a small set of operators to develop our ideas. We implemented the solution in a TeSSLa compiler targeting the Java VM via Scala code generation which combines persistent data structures and mutable data structures for those data values which allow in-place editing. Our empirical evaluation shows considerable speedup for use cases where queues, maps or sets are dominant data structures.

Abstract Runtime Verification is a lightweight verification approach that aims at checking that a run of a system under observation adheres to a formal specification. A classical approach is to synthesize a monitor from an LTL property. Usually, such a monitor receives the trace of the system under observation incrementally and checks the property with respect to the first position of any trace that extends the received prefix. This comes with the disadvantage that once the monitor detects a violation or satisfaction of the verdict it cannot recover and the erroneous position in the trace is not explicitly disclosed. An alternative monitoring problem, proposed for example for Past LTL evaluation, is to evaluate the LTL property repeatedly at each position in the received trace, which enables recovering and gives more information when the property is breached. In this paper we study this concept of recurrent monitoring in detail, particularly we investigate how the notion of anticipation (yielding future verdicts when they are inevitable) can be extended to recurrent monitoring. Furthermore, we show how two fundamental approaches in Runtime Verification can be applied to recurrent monitoring, namely Uncertainty—which deals with the handling of inaccurate or unavailable information in the input trace—and Assumptions, i.e. the inclusion of additional knowledge about system invariants in the monitoring process.

Abstract Runtime verification deals with checking correctness properties on the runs of a system under scrutiny. To achieve this, it addresses a variety of sub-problems related to monitoring of systems: These range from the appropriate design of a specification language over efficient monitor generation as hardware and software monitors to solutions for instrumenting the monitored system, preferably in a non-intrusive way. Further aspects play a role for the usability of a runtime verification toolchain, e.g. availability, sufficient documentation and the existence of a developer community. In this paper we present the TeSSLa ecosystem, a runtime verification framework built around the stream runtime verification language TeSSLa: It provides a rich toolchain of mostly freely available compilers for monitor generation on different hardware and software backends, as well as instrumentation mechanisms for various runtime verification requirements. Additionally, we highlight how the online resources and supporting tools of the community-driven project enable the productive usage of stream runtime verification.

In this paper, we introduce TDDL, a timed dyadic deontic logic. Our starting point is a version of a dyadic deontic logic with conditional obligations, permissions, and obligations, and with a “reparation” operator for representing contrary-to-duties and contrary-to-prohibitions. We also consider a sequence operator allowing us to define norms as sequences of individual norms and most importantly with timed intervals, allowing us to express deadlines of norms. We provide a trace semantics capturing both satisfaction and violation of norms and discuss fulfillment of TDDL specifications.

This paper introduces a synthesis procedure for the satisfiability problem of RMTL- ∫ formulas as SAT solving modulo theories. RMTL- ∫ is a real-time version of metric temporal logic (MTL) extended by a duration quantifier allowing to measure time durations. For any given formula, a SAT instance modulo the theory of arrays, uninterpreted functions with equality and non-linear real-arithmetic is synthesized and may then be further investigated using appropriate SMT solvers. We show the benefits of using RMTL- ∫ with the given SMT encoding on a diversified set of examples that include in particular its application in the area of schedulability analysis. Therefore, we introduce a simple language for formalizing schedulability problems and show how to formulate timing constraints as RMTL- ∫ formulas. Our practical evaluation based on our synthesis and Z3 as back-end SMT solver also shows the feasibility of the overall approach.

Abstract We study the problem of online runtime verification of real-time event streams. Our monitors can observe concurrent systems with a shared clock, but where each component reports observations as signals that arrive to the monitor at different speeds and with different and varying latencies. We start from specifications in a fragment of the TeSSLa specification language, where streams (including inputs and final verdicts) are not restricted to be Booleans but can be data from richer domains, including integers and reals with arithmetic operations and aggregations. Specifications can be used both for checking logical properties and for computing statistics and general numeric temporal metrics (and properties on these richer metrics). We present an online evaluation algorithm for the specification language and a concurrent implementation of the evaluation algorithm. The algorithm can tolerate and exploit the asynchronous arrival of events without synchronizing the inputs. Then, we introduce a theory of asynchronous transducers and show a formal proof of the correctness such that every possible run of the monitor implements the semantics. Finally, we report an empirical evaluation of a highly concurrent Erlang implementation of the monitoring algorithm.

Runtime Verification (RV) studies how to analyze execution traces of a system under observation. Stream Runtime Verification (SRV) applies stream transformations to obtain information from observed traces. Incomplete traces with information missing in gaps pose a common challenge when applying RV and SRV techniques to real-world systems as RV approaches typically require the complete trace without missing parts. This paper presents a solution to perform SRV on incomplete traces based on abstraction. We use TeSSLa as specification language for non-synchronized timed event streams and define abstract event streams representing the set of all possible traces that could have occurred during gaps in the input trace. We show how to translate a TeSSLa specification to its abstract counterpart that can propagate gaps through the transformation of the input streams and thus generate sound outputs even if the input streams contain gaps and events with imprecise values. The solution has been implemented as a set of macros for the original TeSSLa and an empirical evaluation shows the feasibility of the approach.

This issue of Mathematical Structures in Computer Science (MSCS) contains a selection of papers presented at the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), which took place in Cali, Colombia, on October 29–31, 2015.

Modern multi-core Systems-on-Chip (SoC) provide very high computational power. On the downside, they are hard to debug and it is often very difficult to understand what is going on in these chips because of the limited observability inside the SoC. Chip manufacturers try to compensate this difficulty by providing highly compressed trace data from the individual cores. In the past, the common way to deal with this data was storing it for later offline analysis, which severely limits the time span that can be observed. In this contribution, we present an FPGA-based solution that is able to process the trace data in real-time, enabling continuous observation of the state of a core. Moreover, we discuss applications enabled by this technology.

We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the model-checking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.

BACKGROUND: Next generation sequencing (NGS) technologies enable studies and analyses of the diversity of both T and B cell receptors (TCR and BCR) in human and animal systems to elucidate immune functions in health and disease. Over the last few years, several algorithms and tools have been developed to support respective analyses of raw sequencing data of the immune repertoire. These tools focus on distinct aspects of the data processing and require a strong bioinformatics background. To facilitate the analysis of T and B cell repertoires by less experienced users, software is needed that combines the most common tools for repertoire analysis. RESULTS: We introduce a graphical user interface (GUI) providing a complete analysis pipeline for processing raw NGS data for human and animal TCR and BCR clonotype determination and advanced differential repertoire studies. It provides two applications. ClonoCalc prepares the raw data for downstream analyses. It combines a demultiplexer for barcode splitting and employs MiXCR for paired-end read merging and the extraction of human and animal TCR/BCR sequences. ClonoPlot wraps the R package tcR and further contributes self-developed plots for the descriptive comparative investigation of immune repertoires. CONCLUSION: This workflow reduces the amount of programming required to perform the respective analyses and supports both communication and training between scientists and technicians, and across scientific disciplines. The Open Source development in Java and R is modular and invites advanced users to extend its functionality. Software and documentation are freely available at https://bitbucket.org/ClonoSuite/clonocalc-plot .

The model-checking problem for Software Products Lines (SPLs) is harder than for single systems: variability constitutes a new source of complexity that exacerbates the state-explosion problem. Abstraction techniques have successfully alleviated state explosion in single-system models. However, they need to be adapted to SPLs, to take into account the set of variants that produce a counterexample. In this paper, we apply CEGAR (Counterexample-Guided Abstraction Refinement) and we design new forms of abstraction specifically for SPLs. We carry out experiments to evaluate the efficiency of our new abstractions. The results show that our abstractions, combined with an appropriate refinement strategy, hold the potential to achieve large reductions in verification time, although they sometimes perform worse. We discuss in which cases a given abstraction should be used.

Multicore System-on-Chip (SoC) implementations of embedded systems are becoming very popular. In these systems it is possible to spread out computations over many cores. On one hand this leads to better energy efficiency if clock frequencies and core voltages are reduced. On the other hand this delivers very high performance to the software developer and thus enables complex software systems to be implemented. Unfortunately, debugging and validation of these systems becomes extremely difficult. Various technological approaches try to solve this dilemma. In this contribution we will show a new approach to observe multi-core SoCs and make their internal operations visible to external analysis tools. Also, we show that runtime verification can be employed to analyze and validate these internal operations while the system operates in its normal environment. The combination of these two approaches delivers unprecedented options to the developer to understand and verify system behavior even in complex multicore SoCs.

We propose fLTL, an extension to linear-time temporal logic (LTL) that allows for expressing relative frequencies by a generalization of temporal operators. This facilitates the specification of requirements such as the deadlines in a realtime system must be met in at least 95% of all cases. For our novel logic, we establish an undecidability result regarding the satisfiability problem but identify a decidable fragment which strictly increases the expressiveness of LTL by allowing, e.g., to express non-context-free properties.

Traditionally routing has focused on finding shortest paths in networks with positive, static edge costs representing the distance between two nodes. Energy-optimal routing for electric vehicles creates novel algorithmic challenges, as simply understanding edge costs as energy values and applying standard algorithms does not work. First, edge costs can be negative due to recuperation, excluding Dijkstra-like algorithms. Second, edge costs may depend on parameters such as vehicle weight only known at query time, ruling out existing preprocessing techniques. Third, considering battery capacity limitations implies that the cost of a path is no longer just the sum of its edge costs. This paper shows how these challenges can be met within the framework of A* search. We show how the specific domain gives rise to a consistent heuristic function yielding an O(n2) routing algorithm. Moreover, we show how battery constraints can be treated by dynamically adapting edge costs and hence can be handled in the same way as parameters given at query time, without increasing run-time complexity. Experimental results with real road networks and vehicle data demonstrate the advantages of our solution.

This workshop will bring together researchers interested in raising the efficiency and the effectiveness of Software Product Line Engineering by applying innovative analysis approaches and formal methods.

Workflow mining is the task of automatically producing a workflow model from a set of event logs recording sequences of workflow events; each sequence corresponds to a use case or workflow instance. Formal approaches to workflow mining assume that th

This article studies runtime verification of properties expressed either in lineartime temporal logic (LTL) or timed lineartime temporal logic (TLTL). It classifies runtime verification in identifying its distinguishing features to model checking and testing, respectively. It introduces a three-valued semantics (with truth values true, false, inconclusive ) as an adequate interpretation as to whether a partial observation of a running system meets an LTL or TLTL property. For LTL, a conceptually simple monitor generation procedure is given, which is optimal in two respects: First, the size of the generated deterministic monitor is minimal , and, second, the monitor identifies a continuously monitored trace as either satisfying or falsifying a property as early as possible . The feasibility of the developed methodology is demontrated using a collection of real-world temporal logic specifications. Moreover, the presented approach is related to the properties monitorable in general and is compared to existing concepts in the literature. It is shown that the set of monitorable properties does not only encompass the safety and cosafety properties but is strictly larger. For TLTL, the same road map is followed by first defining a three-valued semantics. The corresponding construction of a timed monitor is more involved, yet, as shown, possible.

This extended abstract presents the main ideas behind regular linear-time temporal logic (RLTL), a logic that generalizes linear-time temporal logic (LTL) with the ability to use regular expressions arbitrarily as sub-expressions. Unlike LTL, RLTL can define all !-regular languages and unlike previous approaches, RLTL is defined with an algebraic signature, does not depend on fix-points in its syntax, and provides past operators via a single previous-step operator for basic state formulas. The satisfiability and model checking problems for RLTL are PSPACE-complete, which is optimal for extensions of LTL.

When monitoring a system w.r.t. a property defined in a temporal logic such as LTL, a major concern is to settle with an adequate interpretation of observable system events; that is, models of temporal logic formulae are usually infinite words of events,

This paper is concerned with bridging the gap between requirements and distributed systems. Requirements are defined as basic message sequence charts (MSCs) specifying positive and negative scenarios. Communicating finite-state machines (CFMs), i.e., finite automata that communicate via FIFO buffers, act as system realizations. The key contribution is a generalization of Angluin's learning algorithm for synthesizing CFMs from MSCs. This approach is exact-the resulting CFM precisely accepts the set of positive scenarios and rejects all negative ones-and yields fully asynchronous implementations. The paper investigates for which classes of MSC languages CFMs can be learned, presents an optimization technique for learning partial orders, and provides substantial empirical evidence indicating the practical feasibility of the approach.

This paper builds on product line CCS (PL-CCS), an algebraic approach to modeling the behavior of software product lines. The semantics of PL-CCS specifications is given in terms of labeled transition systems for individual products as well as for the entire product line and can be derived automatically. In this paper, we extend PL-CCS with a concept for specifying dependencies, show how to integrate it into a development methodology for product lines and validate its practical applicability by modeling a typical reactive system from the automotive domain. Most importantly, due to the algebraic nature of our model, we can derive calculation laws that allow to compute common parts of a product line. The application of the corresponding calculation rules is illustrated in detail with an example. By this, we obtain a formal foundation for restructuring product lines.

Abstract We extend the approach of model checking parameterized networks of processes by means of network invariants to the setting of real-time systems . We introduce timed transition structures (which are similar in spirit to timed automata) and define a notion of abstraction that is safe with respect to linear temporal properties. We strengthen the notion of abstraction to allow a finite system, then called network invariant , to be an abstraction of networks of real-time systems. In general the problem of checking abstraction of real-time systems is undecidable. Hence, we provide sufficient criteria, which can be checked automatically, to conclude that one system is an abstraction of a concrete one. Our method is based on timed superposition and discretization of timed systems. We exemplify our approach by proving mutual exclusion of a simple protocol inspired by Fischer’s protocol, using the model checker TLV.

In this paper we summarize parallel algorithms for enumerative model checking of properties formulated in linear time temporal logic (LTL) as well as a fragment of the \mu- calculus which naturally subsumes the branching time logic CTL (computation tree logic). We also indicate how to provide parallel model checking applications as services for integrated modelling, analysis, and verification using the FMICS-jETI platform.

The FMICS-jETI platform is a collaborative, service- based demonstrator of tools and techniques for the analysis of industrial critical systems. It is the FMICS Working Group contribution to the Verified Software Initiative. In this paper, we extend the scope of the FMICS-jETI platform to address the integration of heterogeneous and legacy tools and technologies. We show how to integrate 1) CORBA, a language independent standard for the inter-operability of heterogeneous functionalities distributed over a network, 2) active model learning technologies, via the LearnLib, as a model extrapolation technique that uses testing to explore a black box system and CORBA as a communication mechanism, and 3) third party applications built on top of the LearnLib, in this case Smyle, a tool that synthesizes design models by learning from examples, that uses the LearnLib as learner core.

Linear time temporal logic (LTL) has become a well established tool for specifying the dynamic behaviour of reactive systems with an interleaving semantics, and the automata-theoretic approach has proven to be a very useful mechanism for performing automatic verification in this setting. Especially alternating automata turned out to be a powerful tool in constructing efficient yet simple to understand decision procedures and directly yield further on-the-fly model checking procedures. In this paper we exhibit a decision procedure for LTL over Mazurkiewicz traces which generalises the classical automata-theoretic approach to a linear time temporal logic interpreted no longer over sequences but certain partial orders. Specifically, we construct a (linear) alternating Buchi automaton accepting the set of linearisations of traces satisfying the formula at hand. The salient point of our technique is to apply a notion of independence-rewriting to formulas of the logic. Furthermore, we show that the class of linear and trace-consistent alternating Buchi automata corresponds exactly to LTL formulas over Mazurkiewicz traces, lifting a similar result from Loding and Thomas formulated in the framework of LTL over words.

We present a model for message passing systems unifying concepts of message sequence charts (MSCs) and Lamport diagrams. Message passing systems may be defined-similarly to MSCs-without having a concrete communication medium in mind. Our main contribution is that we equip such systems with a tool set of specification and verification procedures. We provide a global linear time temporal logic which may be employed for specifying message passing systems. In an independent step, a communication channel may be specified. Given both specifications, we construct a Buchi automaton accepting those linearisations of MSCs which satisfy the given formula and correspond to a fixed but arbitrary channel.