Showing 1–50 of 90 results for author: Zimmermann, M

The Reachability Problem for Neural-Network Control Systems

Authors: Christian Schilling, Martin Zimmermann

Abstract: A control system consists of a plant component and a controller which periodically computes a control input for the plant. We consider systems where the controller is implemented by a feedforward neural network with ReLU activations. The reachability problem asks, given a set of initial states, whether a set of target states can be reached. We show that this problem is undecidable even for trivial… ▽ More A control system consists of a plant component and a controller which periodically computes a control input for the plant. We consider systems where the controller is implemented by a feedforward neural network with ReLU activations. The reachability problem asks, given a set of initial states, whether a set of target states can be reached. We show that this problem is undecidable even for trivial plants and fixed-depth neural networks with three inputs and outputs. We also show that the problem becomes semi-decidable when the plant as well as the input and target sets are given by automata over infinite words. △ Less

Submitted 6 July, 2024; originally announced July 2024.

Journal ref: AISoLA 2023

The Complexity of Data-Free Nfer

Authors: Sean Kauffman, Kim Guldstrand Larsen, Martin Zimmermann

Abstract: Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment of nfer. The evaluation problem asks whether a given interval is generated by applying rules to a known input, while the satisfiability problem asks if an input… ▽ More Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment of nfer. The evaluation problem asks whether a given interval is generated by applying rules to a known input, while the satisfiability problem asks if an input exists that will generate a given interval. By excluding data from the language, we obtain polynomial-time algorithms for the evaluation problem and for satisfiability when only considering inclusive rules. Furthermore, we show decidability for the satisfiability problem for cycle-free specifications and undecidability for satisfiability of full data-free nfer. △ Less

Submitted 3 July, 2024; originally announced July 2024.

Efficient mid-term forecasting of hourly electricity load using generalized additive models

Authors: Monika Zimmermann, Florian Ziel

Abstract: Accurate mid-term (weeks to one year) hourly electricity load forecasts are essential for strategic decision-making in power plant operation, ensuring supply security and grid stability, and energy trading. While numerous models effectively predict short-term (hours to a few days) hourly load, mid-term forecasting solutions remain scarce. In mid-term load forecasting, besides daily, weekly, and an… ▽ More Accurate mid-term (weeks to one year) hourly electricity load forecasts are essential for strategic decision-making in power plant operation, ensuring supply security and grid stability, and energy trading. While numerous models effectively predict short-term (hours to a few days) hourly load, mid-term forecasting solutions remain scarce. In mid-term load forecasting, besides daily, weekly, and annual seasonal and autoregressive effects, capturing weather and holiday effects, as well as socio-economic non-stationarities in the data, poses significant modeling challenges. To address these challenges, we propose a novel forecasting method using Generalized Additive Models (GAMs) built from interpretable P-splines and enhanced with autoregressive post-processing. This model uses smoothed temperatures, Error-Trend-Seasonal (ETS) modeled non-stationary states, a nuanced representation of holiday effects with weekday variations, and seasonal information as input. The proposed model is evaluated on load data from 24 European countries. This analysis demonstrates that the model not only has significantly enhanced forecasting accuracy compared to state-of-the-art methods but also offers valuable insights into the influence of individual components on predicted load, given its full interpretability. Achieving performance akin to day-ahead TSO forecasts in fast computation times of a few seconds for several years of hourly data underscores the model's potential for practical application in the power system industry. △ Less

Submitted 27 May, 2024; originally announced May 2024.

Monitoring Real-Time Systems under Parametric Delay

Authors: Martin Fränzle, Thomas M. Grosen, Kim G. Larsen, Martin Zimmermann

Abstract: Online monitoring of embedded real-time systems can be achieved by reduction of an adequate property language, like Metric Interval Temporal Logic, to timed automata and symbolic execution of the resulting automata on the trace observed from the system. This direct construction however only is faithful if observation of the trace is immediate in the sense that the monitor can assign exact time sta… ▽ More Online monitoring of embedded real-time systems can be achieved by reduction of an adequate property language, like Metric Interval Temporal Logic, to timed automata and symbolic execution of the resulting automata on the trace observed from the system. This direct construction however only is faithful if observation of the trace is immediate in the sense that the monitor can assign exact time stamps to the actions it observes, which is rarely true in practice due to the substantial and fluctuating parametric delays introduced by the circuitry connecting the observed system to its monitoring device. We present a purely zone-based online monitoring procedure and its implementation which handle such parametric delays exactly without recurrence to costly verification procedures for parametric timed automata. △ Less

Submitted 28 April, 2024; originally announced April 2024.

Tracy, Traces, and Transducers: Computable Counterexamples and Explanations for HyperLTL Model-Checking

Authors: Sarah Winter, Martin Zimmermann

Abstract: HyperLTL model-checking enables the automated verification of information-flow properties for security-critical systems. However, it only provides a binary answer. Here, we introduce two paradigms to compute counterexamples and explanations for HyperLTL model-checking, thereby considerably increasing its usefulness. Both paradigms are based on the maxim ``counterexamples/explanations are Skolem fu… ▽ More HyperLTL model-checking enables the automated verification of information-flow properties for security-critical systems. However, it only provides a binary answer. Here, we introduce two paradigms to compute counterexamples and explanations for HyperLTL model-checking, thereby considerably increasing its usefulness. Both paradigms are based on the maxim ``counterexamples/explanations are Skolem functions for the existentially quantified trace variables''. Our first paradigm is complete (everything can be explained), but restricted to ultimately periodic system traces. The second paradigm works with (Turing machine) computable Skolem functions and is therefore much more general, but also shown incomplete (not everything can computably be explained). Finally, we prove that it is decidable whether a given finite transition system and a formula have computable Skolem functions witnessing that the system satisfies the formula. Our algorithm also computes transducers implementing computable Skolem functions, if they exist. △ Less

Submitted 28 April, 2024; originally announced April 2024.

Solving the swing-up and balance task for the Acrobot and Pendubot with SAC

Authors: Chi Zhang, Akhil Sathuluri, Markus Zimmermann

Abstract: We present a solution of the swing-up and balance task for the pendubot and acrobot for the participation in the AI Olympics competition at IJCAI 2023. Our solution is based on the Soft Actor Crtic (SAC) reinforcement learning (RL) algorithm for training a policy for the swing-up and entering the region of attraction of a linear quadratic regulator(LQR) controller for stabilizing the double pendul… ▽ More We present a solution of the swing-up and balance task for the pendubot and acrobot for the participation in the AI Olympics competition at IJCAI 2023. Our solution is based on the Soft Actor Crtic (SAC) reinforcement learning (RL) algorithm for training a policy for the swing-up and entering the region of attraction of a linear quadratic regulator(LQR) controller for stabilizing the double pendulum at the top position. Our controller achieves competitive scores in performance and robustness for both, pendubot and acrobot, problem scenarios. △ Less

Submitted 18 December, 2023; originally announced December 2023.

Comments: IJCAI 2023, RealAIGym competition

The Complexity of Second-order HyperLTL

Authors: Hadar Frenkel, Martin Zimmermann

Abstract: We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are as hard as truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quan… ▽ More We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are as hard as truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. The first fragment is still as hard as truth in third-order arithmetic while satisfiability for the second one is $Σ_1^1$-complete, i.e., only as hard as (first-order) HyperLTL and therefore much less complex. Finally, finite-state satisfiability and model-checking are in $Σ_2^2$ and $Σ_1^1$-hard, and thus also less complex than model-checking full second-order HyperLTL. △ Less

Submitted 28 April, 2024; v1 submitted 27 November, 2023; originally announced November 2023.

Strategies Resilient to Delay: Games under Delayed Control vs. Delay Games

Authors: Martin Fränzle, Sarah Winter, Martin Zimmermann

Abstract: We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. Our main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We fu… ▽ More We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. Our main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We furthermore analyze existence of randomized strategies that win almost surely, where this correspondence between the two types of games breaks down. △ Less

Submitted 2 October, 2023; originally announced October 2023.

Comments: In Proceedings GandALF 2023, arXiv:2309.17318

Journal ref: EPTCS 390, 2023, pp. 220-235

Evaluation of Key Spatiotemporal Learners for Print Track Anomaly Classification Using Melt Pool Image Streams

Authors: Lynn Cherif, Mutahar Safdar, Guy Lamouche, Priti Wanjara, Padma Paul, Gentry Wood, Max Zimmermann, Florian Hannesen, Yaoyao Fiona Zhao

Abstract: Recent applications of machine learning in metal additive manufacturing (MAM) have demonstrated significant potential in addressing critical barriers to the widespread adoption of MAM technology. Recent research in this field emphasizes the importance of utilizing melt pool signatures for real-time defect prediction. While high-quality melt pool image data holds the promise of enabling precise pre… ▽ More Recent applications of machine learning in metal additive manufacturing (MAM) have demonstrated significant potential in addressing critical barriers to the widespread adoption of MAM technology. Recent research in this field emphasizes the importance of utilizing melt pool signatures for real-time defect prediction. While high-quality melt pool image data holds the promise of enabling precise predictions, there has been limited exploration into the utilization of cutting-edge spatiotemporal models that can harness the inherent transient and sequential characteristics of the additive manufacturing process. This research introduces and puts into practice some of the leading deep spatiotemporal learning models that can be adapted for the classification of melt pool image streams originating from various materials, systems, and applications. Specifically, it investigates two-stream networks comprising spatial and temporal streams, a recurrent spatial network, and a factorized 3D convolutional neural network. The capacity of these models to generalize when exposed to perturbations in melt pool image data is examined using data perturbation techniques grounded in real-world process scenarios. The implemented architectures demonstrate the ability to capture the spatiotemporal features of melt pool image sequences. However, among these models, only the Kinetics400 pre-trained SlowFast network, categorized as a two-stream network, exhibits robust generalization capabilities in the presence of data perturbations. △ Less

Submitted 28 August, 2023; originally announced August 2023.

Comments: This work has been accepted to IFAC for publication under a Creative Commons Licence CC-BY-NC-ND

Report number: 2577

Robust Alternating-Time Temporal Logic

Authors: Aniello Murano, Daniel Neider, Martin Zimmermann

Abstract: In multi-agent system design, a crucial aspect is to ensure robustness, meaning that for a coalition of agents A, small violations of adversarial assumptions only lead to small violations of A's goals. In this paper we introduce a logical framework for robust strategic reasoning about multi-agent systems. Specifically, inspired by recent works on robust temporal logics, we introduce and study rATL… ▽ More In multi-agent system design, a crucial aspect is to ensure robustness, meaning that for a coalition of agents A, small violations of adversarial assumptions only lead to small violations of A's goals. In this paper we introduce a logical framework for robust strategic reasoning about multi-agent systems. Specifically, inspired by recent works on robust temporal logics, we introduce and study rATL and rATL*, logics that extend the well-known Alternating-time Temporal Logic ATL and ATL* by means of an opportune multi-valued semantics for the strategy quantifiers and temporal operators. We study the model-checking and satisfiability problems for rATL and rATL* and show that dealing with robustness comes at no additional computational cost. Indeed, we show that these problems are PTime-complete and ExpTime-complete for rATL, respectively, while both are 2ExpTime-complete for rATL*. △ Less

Submitted 20 July, 2023; originally announced July 2023.

Robust Probabilistic Temporal Logics

Authors: Martin Zimmermann

Abstract: We robustify PCTL and PCTL*, the most important specification languages for probabilistic systems, and show that robustness does not increase the complexity of the model-checking problems. We robustify PCTL and PCTL*, the most important specification languages for probabilistic systems, and show that robustness does not increase the complexity of the model-checking problems. △ Less

Submitted 28 April, 2024; v1 submitted 9 June, 2023; originally announced June 2023.

On the Existence of Reactive Strategies Resilient to Delay

Authors: Martin Fränzle, Paul Kröger, Sarah Winter, Martin Zimmermann

Abstract: We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. In games under delayed control both players suffer from partial informedness due to symmetrically delayed communication, while in delay games, the protagonist has to grant lookahead to the alter player. Our first main result, the interreducibility of the existence of… ▽ More We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. In games under delayed control both players suffer from partial informedness due to symmetrically delayed communication, while in delay games, the protagonist has to grant lookahead to the alter player. Our first main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We furthermore analyse existence of randomized strategies that win almost surely, where this correspondence between the two types of games breaks down. In this setting, some games surely won by the alter player in delay games can now be won almost surely by the protagonist in the corresponding game under delayed control, showing that it indeed makes a difference whether the protagonist has to grant lookahead or both players suffer from partial informedness. These results get even more pronounced when we finally address the quantitative goal of winning with a probability in $[0,1]$. We show that for any rational threshold $θ\in [0,1]$ there is a game that can be won by the protagonist with exactly probability $θ$ under delayed control, while being surely won by alter in the delay game setting. All these findings refine our original result that games under delayed control are not determined. △ Less

Submitted 12 March, 2024; v1 submitted 31 May, 2023; originally announced May 2023.

Comments: Full version of arXiv:2310.01010, contains all proofs omitted in the conference version as well as a new section on winning games under delayed control with mixed strategies with respect to a fixed threshold

HyperLTL Satisfiability Is Highly Undecidable, HyperCTL* is Even Harder

Authors: Marie Fortin, Louwe B. Kuijer, Patrick Totzke, Martin Zimmermann

Abstract: Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics. In this paper we settle the exact… ▽ More Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics. In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is $Σ_1^1$-complete and HyperCTL* satisfiability is $Σ_1^2$-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove $Σ_1^2$-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We also prove this bound to be tight. Furthermore, we prove that both countable and finitely-branching satisfiability for HyperCTL* are as hard as truth in second-order arithmetic, i.e. still highly undecidable. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is $Π_1^1$-complete. △ Less

Submitted 30 March, 2023; v1 submitted 29 March, 2023; originally announced March 2023.

Comments: Extended version of a paper presented at MFCS 2021 and archived as arXiv:2105.04176

A systems design approach for the co-design of a humanoid robot arm

Authors: Akhil Sathuluri, Anand Vazhapilli Sureshbabu, Markus Zimmermann

Abstract: Classically, the development of humanoid robots has been sequential and iterative. Such bottom-up design procedures rely heavily on intuition and are often biased by the designer's experience. Exploiting the non-linear coupled design space of robots is non-trivial and requires a systematic procedure for exploration. We adopt the top-down design strategy, the V-model, used in automotive and aerospa… ▽ More Classically, the development of humanoid robots has been sequential and iterative. Such bottom-up design procedures rely heavily on intuition and are often biased by the designer's experience. Exploiting the non-linear coupled design space of robots is non-trivial and requires a systematic procedure for exploration. We adopt the top-down design strategy, the V-model, used in automotive and aerospace industries. Our co-design approach identifies non-intuitive designs from within the design space and obtains the maximum permissible range of the design variables as a solution space, to physically realise the obtained design. We show that by constructing the solution space, one can (1) decompose higher-level requirements onto sub-system-level requirements with tolerance, alleviating the "chicken-or-egg" problem during the design process, (2) decouple the robot's morphology from its controller, enabling greater design flexibility, (3) obtain independent sub-system level requirements, reducing the development time by parallelising the development process. △ Less

Submitted 29 December, 2022; originally announced December 2022.

Comments: Presented at the Workshop on Development and Design Pipelines - From first ideas to well-functioning robots, 2022 IEEE-RAS International Conference on Humanoid Robots (Humanoids 2022)

Two-Step Online Trajectory Planning of a Quadcopter in Indoor Environments with Obstacles

Authors: Martin Zimmermann, Minh Nhat Vu, Florian Beck, Anh Nguyen, Andreas Kugi

Abstract: This paper presents a two-step algorithm for online trajectory planning in indoor environments with unknown obstacles. In the first step, sampling-based path planning techniques such as the optimal Rapidly exploring Random Tree (RRT*) algorithm and the Line-of-Sight (LOS) algorithm are employed to generate a collision-free path consisting of multiple waypoints. Then, in the second step, constraine… ▽ More This paper presents a two-step algorithm for online trajectory planning in indoor environments with unknown obstacles. In the first step, sampling-based path planning techniques such as the optimal Rapidly exploring Random Tree (RRT*) algorithm and the Line-of-Sight (LOS) algorithm are employed to generate a collision-free path consisting of multiple waypoints. Then, in the second step, constrained quadratic programming is utilized to compute a smooth trajectory that passes through all computed waypoints. The main contribution of this work is the development of a flexible trajectory planning framework that can detect changes in the environment, such as new obstacles, and compute alternative trajectories in real time. The proposed algorithm actively considers all changes in the environment and performs the replanning process only on waypoints that are occupied by new obstacles. This helps to reduce the computation time and realize the proposed approach in real time. The feasibility of the proposed algorithm is evaluated using the Intel Aero Ready-to-Fly (RTF) quadcopter in simulation and in a real-world experiment. △ Less

Submitted 6 February, 2023; v1 submitted 11 November, 2022; originally announced November 2022.

Comments: 8 pages, 9 figures

Weak-signal extraction enabled by deep-neural-network denoising of diffraction data

Authors: Jens Oppliger, M. Michael Denner, Julia Küspert, Ruggero Frison, Qisi Wang, Alexander Morawietz, Oleh Ivashko, Ann-Christin Dippel, Martin von Zimmermann, Izabela Biało, Leonardo Martinelli, Benoît Fauqué, Jaewon Choi, Mirian Garcia-Fernandez, Ke-Jin Zhou, Niels B. Christensen, Tohru Kurosawa, Naoki Momono, Migaku Oda, Fabian D. Natterer, Mark H. Fischer, Titus Neupert, Johan Chang

Abstract: Removal or cancellation of noise has wide-spread applications for imaging and acoustics. In every-day-life applications, denoising may even include generative aspects, which are unfaithful to the ground truth. For scientific use, however, denoising must reproduce the ground truth accurately. Here, we show how data can be denoised via a deep convolutional neural network such that weak signals appea… ▽ More Removal or cancellation of noise has wide-spread applications for imaging and acoustics. In every-day-life applications, denoising may even include generative aspects, which are unfaithful to the ground truth. For scientific use, however, denoising must reproduce the ground truth accurately. Here, we show how data can be denoised via a deep convolutional neural network such that weak signals appear with quantitative accuracy. In particular, we study X-ray diffraction on crystalline materials. We demonstrate that weak signals stemming from charge ordering, insignificant in the noisy data, become visible and accurate in the denoised data. This success is enabled by supervised training of a deep neural network with pairs of measured low- and high-noise data. We demonstrate that using artificial noise does not yield such quantitatively accurate results. Our approach thus illustrates a practical strategy for noise filtering that can be applied to challenging acquisition problems. △ Less

Submitted 11 December, 2023; v1 submitted 19 September, 2022; originally announced September 2022.

Comments: 14 pages, 10 figures; extended study, additional supplementary information, results unchanged

Journal ref: Nature Machine Intelligence (2024)

History-deterministic Parikh Automata

Authors: Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, Martin Zimmermann

Abstract: Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run. Thereby, they preserve many of the desirable properties of finite automata. Deterministic Parikh automata are strictly weaker than nondeterministic ones, but enjoy better closure and algorithmic properties. This state of affairs motivates the study of intermediate… ▽ More Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run. Thereby, they preserve many of the desirable properties of finite automata. Deterministic Parikh automata are strictly weaker than nondeterministic ones, but enjoy better closure and algorithmic properties. This state of affairs motivates the study of intermediate forms of nondeterminism. Here, we investigate history-deterministic Parikh automata, i.e., automata whose nondeterminism can be resolved on the fly. This restricted form of nondeterminism is well-suited for applications which classically call for determinism, e.g., solving games and composition. We show that history-deterministic Parikh automata are strictly more expressive than deterministic ones, incomparable to unambiguous ones, and enjoy almost all of the closure properties of deterministic automata. △ Less

Submitted 31 August, 2023; v1 submitted 16 September, 2022; originally announced September 2022.

Comments: arXiv admin note: text overlap with arXiv:2207.07694

Parikh Automata over Infinite Words

Authors: Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, Martin Zimmermann

Abstract: Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. Here, we study the extension of the classical framework onto infinite inputs: We introduce reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and study exp… ▽ More Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. Here, we study the extension of the classical framework onto infinite inputs: We introduce reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and study expressiveness, closure properties, and the complexity of verification problems. We show that almost all classes of automata have pairwise incomparable expressiveness, both in the deterministic and the nondeterministic case; a result that sharply contrasts with the well-known hierarchy in the $ω$-regular setting. Furthermore, emptiness is shown decidable for Parikh automata with reachability or Büchi acceptance, but undecidable for safety and co-Büchi acceptance. Most importantly, we show decidability of model checking with specifications given by deterministic Parikh automata with safety or co-Büchi acceptance, but also undecidability for all other types of automata. Finally, solving games is undecidable for all types. △ Less

Submitted 20 December, 2022; v1 submitted 15 July, 2022; originally announced July 2022.

Monitoring Timed Properties (Revisited)

Authors: Thomas Møller Grosen, Sean Kauffman, Kim Guldstrand Larsen, Martin Zimmermann

Abstract: In this paper we revisit monitoring real-time systems with respect to properties expressed either in Metric Interval Temporal Logic or as Timed Büchi Automata. We offer efficient symbolic online monitoring algorithms in a number of settings, exploiting so-called zones well-known from efficient model checking of Timed Automata. The settings considered include new, much simplified treatment of time… ▽ More In this paper we revisit monitoring real-time systems with respect to properties expressed either in Metric Interval Temporal Logic or as Timed Büchi Automata. We offer efficient symbolic online monitoring algorithms in a number of settings, exploiting so-called zones well-known from efficient model checking of Timed Automata. The settings considered include new, much simplified treatment of time divergence, monitoring under timing uncertainty, and extension of monitoring to offer minimum time estimates before conclusive verdicts can be made. △ Less

Submitted 5 September, 2022; v1 submitted 29 June, 2022; originally announced June 2022.

On Integrating Prior Knowledge into Gaussian Processes for Prognostic Health Monitoring

Authors: Simon Pfingstl, Markus Zimmermann

Abstract: Gaussian process regression is a powerful method for predicting states based on given data. It has been successfully applied for probabilistic predictions of structural systems to quantify, for example, the crack growth in mechanical structures. Typically, predefined mean and covariance functions are employed to construct the Gaussian process model. Then, the model is updated using current data du… ▽ More Gaussian process regression is a powerful method for predicting states based on given data. It has been successfully applied for probabilistic predictions of structural systems to quantify, for example, the crack growth in mechanical structures. Typically, predefined mean and covariance functions are employed to construct the Gaussian process model. Then, the model is updated using current data during operation while prior information based on previous data is ignored. However, predefined mean and covariance functions without prior information reduce the potential of Gaussian processes. This paper proposes a method to improve the predictive capabilities of Gaussian processes. We integrate prior knowledge by deriving the mean and covariance functions from previous data. More specifically, we first approximate previous data by a weighted sum of basis functions and then derive the mean and covariance functions directly from the estimated weight coefficients. Basis functions may be either estimated or derived from problem-specific governing equations to incorporate physical information. The applicability and effectiveness of this approach are demonstrated for fatigue crack growth, laser degradation, and milling machine wear data. We show that well-chosen mean and covariance functions, like those based on previous data, significantly increase look-ahead time and accuracy. Using physical basis functions further improves accuracy. In addition, computation effort for training is significantly reduced. △ Less

Submitted 17 June, 2022; originally announced June 2022.

Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime

Authors: Satya Prakash Nayak, Daniel Neider, Martin Zimmermann

Abstract: While most of the current synthesis algorithms only focus on correctness-by-construction, ensuring robustness has remained a challenge. Hence, in this paper, we address the robust-by-construction synthesis problem by considering the specifications to be expressed by a robust version of Linear Temporal Logic (LTL), called robust LTL (rLTL). rLTL has a many-valued semantics to capture different degr… ▽ More While most of the current synthesis algorithms only focus on correctness-by-construction, ensuring robustness has remained a challenge. Hence, in this paper, we address the robust-by-construction synthesis problem by considering the specifications to be expressed by a robust version of Linear Temporal Logic (LTL), called robust LTL (rLTL). rLTL has a many-valued semantics to capture different degrees of satisfaction of a specification, i.e., satisfaction is a quantitative notion. We argue that the current algorithms for rLTL synthesis do not compute optimal strategies in a non-antagonistic setting. So, a natural question is whether there is a way of satisfying the specification "better" if the environment is indeed not antagonistic. We address this question by developing two new notions of strategies. The first notion is that of adaptive strategies, which, in response to the opponent's non-antagonistic moves, maximize the degree of satisfaction. The idea is to monitor non-optimal moves of the opponent at runtime using multiple parity automata and adaptively change the system strategy to ensure optimality. The second notion is that of strongly adaptive strategies, which is a further refinement of the first notion. These strategies also maximize the opportunities for the opponent to make non-optimal moves. We show that computing such strategies for rLTL specifications is not harder than the standard synthesis problem, e.g., computing strategies with LTL specifications, and takes doubly-exponential time. △ Less

Submitted 10 August, 2022; v1 submitted 22 April, 2022; originally announced April 2022.

Weak Muller Conditions Make Delay Games Hard

Authors: Sarah Winter, Martin Zimmermann

Abstract: We show that solving delay games with winning conditions given by deterministic and nondeterministic weak Muller automata is 2EXPTIME-complete respectively 3EXPTIME-complete. Furthermore, doubly and triply exponential lookahead is necessary and sufficient to win such games. These results are the first that show that the succinctness of the automata types used to specify the winning conditions has… ▽ More We show that solving delay games with winning conditions given by deterministic and nondeterministic weak Muller automata is 2EXPTIME-complete respectively 3EXPTIME-complete. Furthermore, doubly and triply exponential lookahead is necessary and sufficient to win such games. These results are the first that show that the succinctness of the automata types used to specify the winning conditions has an influence on the complexity of these problems. △ Less

Submitted 19 October, 2022; v1 submitted 7 March, 2022; originally announced March 2022.

The Complexity of Evaluating nfer

Authors: Sean Kauffman, Martin Zimmermann

Abstract: Nfer is a rule-based language for abstracting event streams into a hierarchy of intervals with data. Nfer has multiple implementations and has been applied in the analysis of spacecraft telemetry and autonomous vehicle logs. This work provides the first complexity analysis of nfer evaluation, i.e., the problem of deciding whether a given interval is generated by applying rules. We show that the… ▽ More Nfer is a rule-based language for abstracting event streams into a hierarchy of intervals with data. Nfer has multiple implementations and has been applied in the analysis of spacecraft telemetry and autonomous vehicle logs. This work provides the first complexity analysis of nfer evaluation, i.e., the problem of deciding whether a given interval is generated by applying rules. We show that the full nfer language is undecidable and that this depends on both recursion in the rules and an infinite data domain. By restricting either or both of those capabilities, we obtain tight decidability results. We also examine the impact on complexity of exclusive rules and minimality. For the most practical case, which is minimality with finite data, we provide a polynomial-time algorithm. △ Less

Submitted 21 November, 2022; v1 submitted 28 February, 2022; originally announced February 2022.

Robust Computation Tree Logic

Authors: Satya Prakash Nayak, Daniel Neider, Rajarshi Roy, Martin Zimmermann

Abstract: It is widely accepted that every system should be robust in that ``small'' violations of environment assumptions should lead to ``small'' violations of system guarantees, but it is less clear how to make this intuition mathematically precise. While significant efforts have been devoted to providing notions of robustness for Linear Temporal Logic (LTL), branching-time logics, such as Computation Tr… ▽ More It is widely accepted that every system should be robust in that ``small'' violations of environment assumptions should lead to ``small'' violations of system guarantees, but it is less clear how to make this intuition mathematically precise. While significant efforts have been devoted to providing notions of robustness for Linear Temporal Logic (LTL), branching-time logics, such as Computation Tree Logic (CTL) and CTL*, have received less attention in this regard. To address this shortcoming, we develop ``robust'' extensions of CTL and CTL*, which we name robust CTL (rCTL) and robust CTL* (rCTL*). Both extensions are syntactically similar to their parent logics but employ multi-valued semantics to distinguish between ``large'' and ``small'' violations of the specification. We show that the multi-valued semantics of rCTL make it more expressive than CTL, while rCTL* is as expressive as CTL*. Moreover, we show that the model checking problem, the satisfiability problem, and the synthesis problem for rCTL and rCTL* have the same asymptotic complexity as their non-robust counterparts, implying that robustness can be added to branching-time logics for free. △ Less

Submitted 24 October, 2023; v1 submitted 18 January, 2022; originally announced January 2022.

Comments: Published in the proceedings of NASA Formal Methods (NFM), 2022

ACM Class: F.4.1; I.2.4

Towards Explainable End-to-End Prostate Cancer Relapse Prediction from H&E Images Combining Self-Attention Multiple Instance Learning with a Recurrent Neural Network

Authors: Esther Dietrich, Patrick Fuhlert, Anne Ernst, Guido Sauter, Maximilian Lennartz, H. Siegfried Stiehl, Marina Zimmermann, Stefan Bonn

Abstract: Clinical decision support for histopathology image data mainly focuses on strongly supervised annotations, which offers intuitive interpretability, but is bound by expert performance. Here, we propose an explainable cancer relapse prediction network (eCaReNet) and show that end-to-end learning without strong annotations offers state-of-the-art performance while interpretability can be included thr… ▽ More Clinical decision support for histopathology image data mainly focuses on strongly supervised annotations, which offers intuitive interpretability, but is bound by expert performance. Here, we propose an explainable cancer relapse prediction network (eCaReNet) and show that end-to-end learning without strong annotations offers state-of-the-art performance while interpretability can be included through an attention mechanism. On the use case of prostate cancer survival prediction, using 14,479 images and only relapse times as annotations, we reach a cumulative dynamic AUC of 0.78 on a validation set, being on par with an expert pathologist (and an AUC of 0.77 on a separate test set). Our model is well-calibrated and outputs survival curves as well as a risk score and group per patient. Making use of the attention weights of a multiple instance learning layer, we show that malignant patches have a higher influence on the prediction than benign patches, thus offering an intuitive interpretation of the prediction. Our code is available at www.github.com/imsb-uke/ecarenet. △ Less

Submitted 26 November, 2021; originally announced November 2021.

Comments: Accepted as a regular conference paper at ML4H 2021

Image prediction of disease progression by style-based manifold extrapolation

Authors: Tianyu Han, Jakob Nikolas Kather, Federico Pedersoli, Markus Zimmermann, Sebastian Keil, Maximilian Schulze-Hagen, Marc Terwoelbeck, Peter Isfort, Christoph Haarburger, Fabian Kiessling, Volkmar Schulz, Christiane Kuhl, Sven Nebelung, Daniel Truhn

Abstract: Disease-modifying management aims to prevent deterioration and progression of the disease, not just relieve symptoms. Unfortunately, the development of necessary therapies is often hampered by the failure to recognize the presymptomatic disease and limited understanding of disease development. We present a generic solution for this problem by a methodology that allows the prediction of progression… ▽ More Disease-modifying management aims to prevent deterioration and progression of the disease, not just relieve symptoms. Unfortunately, the development of necessary therapies is often hampered by the failure to recognize the presymptomatic disease and limited understanding of disease development. We present a generic solution for this problem by a methodology that allows the prediction of progression risk and morphology in individuals using a latent extrapolation optimization approach. To this end, we combined a regularized generative adversarial network (GAN) and a latent nearest neighbor algorithm for joint optimization to generate plausible images of future time points. We evaluated our method on osteoarthritis (OA) data from a multi-center longitudinal study (the Osteoarthritis Initiative, OAI). With presymptomatic baseline data, our model is generative and significantly outperforms the end-to-end learning model in discriminating the progressive cohort. Two experiments were performed with seven experienced radiologists. When no synthetic follow-up radiographs were provided, our model performed better than all seven radiologists. In cases where the synthetic follow-ups generated by our model were available, the specificity and sensitivity of all readers in discriminating progressors increased from $72.3\%$ to $88.6\%$ and from $42.1\%$ to $51.6\%$, respectively. Our results open up a new possibility of using model-based morphology and risk prediction to make predictions about future disease occurrence, as demonstrated in the example of OA. △ Less

Submitted 8 April, 2022; v1 submitted 22 November, 2021; originally announced November 2021.

HiRID-ICU-Benchmark -- A Comprehensive Machine Learning Benchmark on High-resolution ICU Data

Authors: Hugo Yèche, Rita Kuznetsova, Marc Zimmermann, Matthias Hüser, Xinrui Lyu, Martin Faltys, Gunnar Rätsch

Abstract: The recent success of machine learning methods applied to time series collected from Intensive Care Units (ICU) exposes the lack of standardized machine learning benchmarks for developing and comparing such methods. While raw datasets, such as MIMIC-IV or eICU, can be freely accessed on Physionet, the choice of tasks and pre-processing is often chosen ad-hoc for each publication, limiting comparab… ▽ More The recent success of machine learning methods applied to time series collected from Intensive Care Units (ICU) exposes the lack of standardized machine learning benchmarks for developing and comparing such methods. While raw datasets, such as MIMIC-IV or eICU, can be freely accessed on Physionet, the choice of tasks and pre-processing is often chosen ad-hoc for each publication, limiting comparability across publications. In this work, we aim to improve this situation by providing a benchmark covering a large spectrum of ICU-related tasks. Using the HiRID dataset, we define multiple clinically relevant tasks in collaboration with clinicians. In addition, we provide a reproducible end-to-end pipeline to construct both data and labels. Finally, we provide an in-depth analysis of current state-of-the-art sequence modeling methods, highlighting some limitations of deep learning approaches for this type of data. With this benchmark, we hope to give the research community the possibility of a fair comparison of their work. △ Less

Submitted 17 January, 2022; v1 submitted 16 November, 2021; originally announced November 2021.

Comments: NeurIPS 2021 (Datasets and Benchmarks)

An Adaptive Honeypot Configuration, Deployment and Maintenance Strategy

Authors: Daniel Fraunholz, Marc Zimmermann, Hans D. Schotten

Abstract: Since honeypots first appeared as an advanced network security concept they suffer from poor deployment and maintenance strategies. State-of-the-Art deployment is a manual process in which the honeypot needs to be configured and maintained by a network administrator. In this paper we present a method for a dynamic honeypot configuration, deployment and maintenance strategy based on machine learnin… ▽ More Since honeypots first appeared as an advanced network security concept they suffer from poor deployment and maintenance strategies. State-of-the-Art deployment is a manual process in which the honeypot needs to be configured and maintained by a network administrator. In this paper we present a method for a dynamic honeypot configuration, deployment and maintenance strategy based on machine learning techniques. Our method features an identification mechanism for machines and devices in a network. These entities are analysed and clustered. Based on the clusters, honeypots are intelligently deployed in the network. The proposed method needs no configuration and maintenance and is therefore a major advantage for the honeypot technology in modern network security. △ Less

Submitted 6 November, 2021; originally announced November 2021.

Deep learning-based bias transfer for overcoming laboratory differences of microscopic images

Authors: Ann-Katrin Thebille, Esther Dietrich, Martin Klaus, Lukas Gernhold, Maximilian Lennartz, Christoph Kuppe, Rafael Kramann, Tobias B. Huber, Guido Sauter, Victor G. Puelles, Marina Zimmermann, Stefan Bonn

Abstract: The automated analysis of medical images is currently limited by technical and biological noise and bias. The same source tissue can be represented by vastly different images if the image acquisition or processing protocols vary. For an image analysis pipeline, it is crucial to compensate such biases to avoid misinterpretations. Here, we evaluate, compare, and improve existing generative model arc… ▽ More The automated analysis of medical images is currently limited by technical and biological noise and bias. The same source tissue can be represented by vastly different images if the image acquisition or processing protocols vary. For an image analysis pipeline, it is crucial to compensate such biases to avoid misinterpretations. Here, we evaluate, compare, and improve existing generative model architectures to overcome domain shifts for immunofluorescence (IF) and Hematoxylin and Eosin (H&E) stained microscopy images. To determine the performance of the generative models, the original and transformed images were segmented or classified by deep neural networks that were trained only on images of the target bias. In the scope of our analysis, U-Net cycleGANs trained with an additional identity and an MS-SSIM-based loss and Fixed-Point GANs trained with an additional structure loss led to the best results for the IF and H&E stained samples, respectively. Adapting the bias of the samples significantly improved the pixel-level segmentation for human kidney glomeruli and podocytes and improved the classification accuracy for human prostate biopsies by up to 14%. △ Less

Submitted 25 May, 2021; originally announced May 2021.

Comments: Accepted as a regular conference paper at MIUA 2021

HyperLTL Satisfiability is $Σ_1^1$-complete, HyperCTL* Satisfiability is $Σ_1^2$-complete

Authors: Marie Fortin, Louwe B. Kuijer, Patrick Totzke, Martin Zimmermann

Abstract: Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics. In this paper we settle the exact… ▽ More Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics. In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is $Σ_1^1$-complete and HyperCTL* satisfiability is $Σ_1^2$-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove $Σ_1^2$-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is $Π_1^1$-complete. △ Less

Submitted 10 May, 2021; originally announced May 2021.

MSC Class: 03D35 ACM Class: F.4.1; F.3.1

A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct

Authors: Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, Martin Zimmermann

Abstract: We study the expressiveness and succinctness of history-deterministic pushdown automata (HD-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved based on the run constructed so far, but independently of the remainder of the input word. These are also known as good-for-games pushdown automata. We prove that HD-PDA recognise more languages than deterministic PDA (D… ▽ More We study the expressiveness and succinctness of history-deterministic pushdown automata (HD-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved based on the run constructed so far, but independently of the remainder of the input word. These are also known as good-for-games pushdown automata. We prove that HD-PDA recognise more languages than deterministic PDA (DPDA) but not all context-free languages (CFL). This class is orthogonal to unambiguous CFL. We further show that HD-PDA can be exponentially more succinct than DPDA, while PDA can be double-exponentially more succinct than HD-PDA. We also study HDness in visibly pushdown automata (VPA), which enjoy better closure properties than PDA, and for which we show that deciding HDness is ExpTime-complete. HD-VPA can be exponentially more succinct than deterministic VPA, while VPA can be exponentially more succinct than HD-VPA. Both of these lower bounds are tight. We then compare HD-PDA with PDA for which composition with games is well-behaved, i.e. good-for-games automata. We show that these two notions coincide, but only if we consider potentially infinitely branching games. Finally, we study the complexity of resolving nondeterminism in HD-PDA. Every HDPDA has a positional resolver, a function that resolves nondeterminism and that is only dependant on the current configuration. Pushdown transducers are sufficient to implement the resolvers of HD-VPA, but not those of HD-PDA. HD-PDA with finite-state resolvers are determinisable. △ Less

Submitted 10 January, 2024; v1 submitted 6 May, 2021; originally announced May 2021.

Journal ref: Logical Methods in Computer Science (January 11, 2024) lmcs:10156

Open community platform for hearing aid algorithm research: open Master Hearing Aid (openMHA)

Authors: Hendrik Kayser, Tobias Herzke, Paul Maanen, Max Zimmermann, Giso Grimm, Volker Hohmann

Abstract: open Master Hearing Aid (openMHA) was developed and provided to the hearing aid research community as an open-source software platform with the aim to support sustainable and reproducible research towards improvement and new types of assistive hearing systems not limited by proprietary software. The software offers a flexible framework that allows the users to conduct hearing aid research using to… ▽ More open Master Hearing Aid (openMHA) was developed and provided to the hearing aid research community as an open-source software platform with the aim to support sustainable and reproducible research towards improvement and new types of assistive hearing systems not limited by proprietary software. The software offers a flexible framework that allows the users to conduct hearing aid research using tools and a number of signal processing plugins provided with the software as well as the implementation of own methods. The openMHA software is independent of a specific hardware and supports Linux, macOS and Windows operating systems as well as 32-bit and 64-bit ARM-based architectures such as used in small portable integrated systems. www.openmha.org △ Less

Submitted 24 January, 2022; v1 submitted 3 March, 2021; originally announced March 2021.

Comments: 10 pages, 5 figures

Journal ref: SoftwareX, Volume 17, 2022, 100953, ISSN 2352-7110

Advancing diagnostic performance and clinical usability of neural networks via adversarial training and dual batch normalization

Authors: Tianyu Han, Sven Nebelung, Federico Pedersoli, Markus Zimmermann, Maximilian Schulze-Hagen, Michael Ho, Christoph Haarburger, Fabian Kiessling, Christiane Kuhl, Volkmar Schulz, Daniel Truhn

Abstract: Unmasking the decision-making process of machine learning models is essential for implementing diagnostic support systems in clinical practice. Here, we demonstrate that adversarially trained models can significantly enhance the usability of pathology detection as compared to their standard counterparts. We let six experienced radiologists rate the interpretability of saliency maps in datasets of… ▽ More Unmasking the decision-making process of machine learning models is essential for implementing diagnostic support systems in clinical practice. Here, we demonstrate that adversarially trained models can significantly enhance the usability of pathology detection as compared to their standard counterparts. We let six experienced radiologists rate the interpretability of saliency maps in datasets of X-rays, computed tomography, and magnetic resonance imaging scans. Significant improvements were found for our adversarial models, which could be further improved by the application of dual batch normalization. Contrary to previous research on adversarially trained models, we found that the accuracy of such models was equal to standard models when sufficiently large datasets and dual batch norm training were used. To ensure transferability, we additionally validated our results on an external test set of 22,433 X-rays. These findings elucidate that different paths for adversarial and real images are needed during training to achieve state of the art results with superior clinical interpretability. △ Less

Submitted 25 November, 2020; originally announced November 2020.

Approximating the Minimal Lookahead Needed to Win Infinite Games

Authors: Martin Zimmermann

Abstract: We present an exponential-time algorithm approximating the minimal lookahead necessary to win an $ω$-regular delay game. We present an exponential-time algorithm approximating the minimal lookahead necessary to win an $ω$-regular delay game. △ Less

Submitted 1 March, 2022; v1 submitted 22 October, 2020; originally announced October 2020.

Optimal Strategies in Weighted Limit Games

Authors: Aniello Murano, Sasha Rubin, Martin Zimmermann

Abstract: We prove the existence and computability of optimal strategies in weighted limit games, zero-sum infinite-duration games with a Büchi-style winning condition requiring to produce infinitely many play prefixes that satisfy a given regular specification. Quality of plays is measured in the maximal weight of infixes between successive play prefixes that satisfy the specification. We prove the existence and computability of optimal strategies in weighted limit games, zero-sum infinite-duration games with a Büchi-style winning condition requiring to produce infinitely many play prefixes that satisfy a given regular specification. Quality of plays is measured in the maximal weight of infixes between successive play prefixes that satisfy the specification. △ Less

Submitted 22 September, 2020; originally announced September 2020.

Comments: In Proceedings GandALF 2020, arXiv:2009.09360. Full version at arXiv:2008.11562

Journal ref: EPTCS 326, 2020, pp. 114-130

Optimal Strategies in Weighted Limit Games (full version)

Authors: Aniello Murano, Sasha Rubin, Martin Zimmermann

Abstract: We prove the existence and computability of optimal strategies in weighted limit games, zero-sum infinite-duration games with a Büchi-style winning condition requiring to produce infinitely many play prefixes that satisfy a given regular specification. Quality of plays is measured in the maximal weight of infixes between successive play prefixes that satisfy the specification. We prove the existence and computability of optimal strategies in weighted limit games, zero-sum infinite-duration games with a Büchi-style winning condition requiring to produce infinitely many play prefixes that satisfy a given regular specification. Quality of plays is measured in the maximal weight of infixes between successive play prefixes that satisfy the specification. △ Less

Submitted 7 September, 2020; v1 submitted 26 August, 2020; originally announced August 2020.

Good-for-games $ω$-Pushdown Automata

Authors: Karoliina Lehtinen, Martin Zimmermann

Abstract: We introduce good-for-games $ω$-pushdown automata ($ω$-GFG-PDA). These are automata whose nondeterminism can be resolved based on the input processed so far. Good-for-gameness enables automata to be composed with games, trees, and other automata, applications which otherwise require deterministic automata. Our main results are that $ω$-GFG-PDA are more expressive than deterministic $ω$- pushdown a… ▽ More We introduce good-for-games $ω$-pushdown automata ($ω$-GFG-PDA). These are automata whose nondeterminism can be resolved based on the input processed so far. Good-for-gameness enables automata to be composed with games, trees, and other automata, applications which otherwise require deterministic automata. Our main results are that $ω$-GFG-PDA are more expressive than deterministic $ω$- pushdown automata and that solving infinite games with winning conditions specified by $ω$-GFG-PDA is EXPTIME-complete. Thus, we have identified a new class of $ω$-contextfree winning conditions for which solving games is decidable. It follows that the universality problem for $ω$-GFG-PDA is in EXPTIME as well. Moreover, we study closure properties of the class of languages recognized by $ω$-GFG- PDA and decidability of good-for-gameness of $ω$-pushdown automata and languages. Finally, we compare $ω$-GFG-PDA to $ω$-visibly PDA, study the resources necessary to resolve the nondeterminism in $ω$-GFG-PDA, and prove that the parity index hierarchy for $ω$-GFG-PDA is infinite. This is a corrected version of the paper arXiv:2001.04392v6 published originally on January 7, 2022. △ Less

Submitted 14 February, 2023; v1 submitted 13 January, 2020; originally announced January 2020.

MSC Class: 68Q45 ACM Class: F.4.3

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (February 15, 2023) lmcs:6995

Optimally Resilient Strategies in Pushdown Safety Games

Authors: Daniel Neider, Patrick Totzke, Martin Zimmermann

Abstract: Infinite-duration games with disturbances extend the classical framework of infinite-duration games, which captures the reactive synthesis problem, with a discrete measure of resilience against non-antagonistic external influence. This concerns events where the observed system behavior differs from the intended one prescribed by the controller. For games played on finite arenas it is known that co… ▽ More Infinite-duration games with disturbances extend the classical framework of infinite-duration games, which captures the reactive synthesis problem, with a discrete measure of resilience against non-antagonistic external influence. This concerns events where the observed system behavior differs from the intended one prescribed by the controller. For games played on finite arenas it is known that computing optimally resilient strategies only incurs a polynomial overhead over solving classical games. This paper studies safety games with disturbances played on infinite arenas induced by pushdown systems. We show how to compute optimally resilient strategies in triply-exponential time. For the subclass of safety games played on one-counter configuration graphs, we show that determining the degree of resilience of the initial configuration is PSPACE-complete and that optimally resilient strategies can be computed in doubly-exponential time. △ Less

Submitted 8 July, 2020; v1 submitted 10 December, 2019; originally announced December 2019.

Promptness and Bounded Fairness in Concurrent and Parameterized Systems

Authors: Swen Jacobs, Mouhammad Sakr, Martin Zimmermann

Abstract: We investigate the satisfaction of specifications in Prompt Linear Temporal Logic (Prompt-LTL) by concurrent systems. Prompt-LTL is an extension of LTL that allows to specify parametric bounds on the satisfaction of eventualities, thus adding a quantitative aspect to the specification language. We establish a connection between bounded fairness, bounded stutter equivalence, and the satisfaction of… ▽ More We investigate the satisfaction of specifications in Prompt Linear Temporal Logic (Prompt-LTL) by concurrent systems. Prompt-LTL is an extension of LTL that allows to specify parametric bounds on the satisfaction of eventualities, thus adding a quantitative aspect to the specification language. We establish a connection between bounded fairness, bounded stutter equivalence, and the satisfaction of Prompt-LTL\X formulas. Based on this connection, we prove the first cutoff results for different classes of systems with a parametric number of components and quantitative specifications, thereby identifying previously unknown decidable fragments of the parameterized model checking problem. △ Less

Submitted 15 November, 2019; v1 submitted 8 November, 2019; originally announced November 2019.

Comments: Accepted for publication in VMCAI 2020

Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free

Authors: Daniel Neider, Alexander Weinert, Martin Zimmermann

Abstract: Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have been identified in the literature, among them the limited expressiveness, the lack of quantitative features, and the inability to express robustness. There is work on overcoming these shortcomings, but each of these is ty… ▽ More Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have been identified in the literature, among them the limited expressiveness, the lack of quantitative features, and the inability to express robustness. There is work on overcoming these shortcomings, but each of these is typically addressed in isolation. This is insufficient for applications where all shortcomings manifest themselves simultaneously. Here, we tackle this issue by introducing logics that address more than one shortcoming. To this end, we combine the logics Linear Dynamic Logic, Prompt-LTL, and robust LTL, each addressing one aspect, to new logics. For all combinations of two aspects, the resulting logic has the same desirable algorithmic properties as plain LTL. In particular, the highly efficient algorithmic backends that have been developed for LTL are also applicable to these new logics. Finally, we discuss how to address all three aspects simultaneously. △ Less

Submitted 17 September, 2019; originally announced September 2019.

Comments: In Proceedings GandALF 2019, arXiv:1909.05979. arXiv admin note: substantial text overlap with arXiv:1808.09028

Journal ref: EPTCS 305, 2019, pp. 1-16

The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas

Authors: Corto Mascle, Martin Zimmermann

Abstract: HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental security policies like noninterference and observational determinism, but has also found applications beyond security, e.g., distributed protoco… ▽ More HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental security policies like noninterference and observational determinism, but has also found applications beyond security, e.g., distributed protocols and coding theory. However, HyperLTL satisfiability is undecidable as soon as there are existential quantifiers in the scope of a universal one. To overcome this severe limitation to applicability, we investigate here restricted variants of the satisfiability problem to pinpoint the decidability border. First, we restrict the space of admissible models and show decidability when restricting the search space to models of bounded size or to finitely representable ones. Second, we consider formulas with restricted nesting of temporal operators and show that nesting depth one yields decidability for a slightly larger class of quantifier prefixes. We provide tight complexity bounds in almost all cases. △ Less

Submitted 13 December, 2019; v1 submitted 11 July, 2019; originally announced July 2019.

Two Decades of SCADA Exploitation: A Brief History

Authors: Simon Duque Anton, Daniel Fraunholz, Christoph Lipps, Frederic Pohl, Marc Zimmermann, Hans D. Schotten

Abstract: Since the early 1960, industrial process control has been applied by electric systems. In the mid 1970's, the term SCADA emerged, describing the automated control and data acquisition. Since most industrial and automation networks were physically isolated, security was not an issue. This changed, when in the early 2000's industrial networks were opened to the public internet. The reasons were mani… ▽ More Since the early 1960, industrial process control has been applied by electric systems. In the mid 1970's, the term SCADA emerged, describing the automated control and data acquisition. Since most industrial and automation networks were physically isolated, security was not an issue. This changed, when in the early 2000's industrial networks were opened to the public internet. The reasons were manifold. Increased interconnectivity led to more productivity, simplicity and ease of use. It decreased the configuration overhead and downtimes for system adjustments. However, it also led to an abundance of new attack vectors. In recent time, there has been a remarkable amount of attacks on industrial companies and infrastructures. In this paper, known attacks on industrial systems are analysed. This is done by investigating the exploits that are available on public sources. The different types of attacks and their points of entry are reviewed in this paper. Trends in exploitation as well as targeted attack campaigns against industrial enterprises are introduced. △ Less

Submitted 21 May, 2019; originally announced May 2019.

A tutorial on recursive models for analyzing and predicting path choice behavior

Authors: Maëlle Zimmermann, Emma Frejinger

Abstract: The problem at the heart of this tutorial consists in modeling the path choice behavior of network users. This problem has been extensively studied in transportation science, where it is known as the route choice problem. In this literature, individuals' choice of paths are typically predicted using discrete choice models. This article is a tutorial on a specific category of discrete choice models… ▽ More The problem at the heart of this tutorial consists in modeling the path choice behavior of network users. This problem has been extensively studied in transportation science, where it is known as the route choice problem. In this literature, individuals' choice of paths are typically predicted using discrete choice models. This article is a tutorial on a specific category of discrete choice models called recursive, and it makes three main contributions: First, for the purpose of assisting future research on route choice, we provide a comprehensive background on the problem, linking it to different fields including inverse optimization and inverse reinforcement learning. Second, we formally introduce the problem and the recursive modeling idea along with an overview of existing models, their properties and applications. Third, we extensively analyze illustrative examples from different angles so that a novice reader can gain intuition on the problem and the advantages provided by recursive models in comparison to path-based ones. △ Less

Submitted 19 March, 2020; v1 submitted 2 May, 2019; originally announced May 2019.

Journal ref: EURO Journal on Transportation and Logistics 9(2):10004, 2020

Machine learning for early prediction of circulatory failure in the intensive care unit

Authors: Stephanie L. Hyland, Martin Faltys, Matthias Hüser, Xinrui Lyu, Thomas Gumbsch, Cristóbal Esteban, Christian Bock, Max Horn, Michael Moor, Bastian Rieck, Marc Zimmermann, Dean Bodenham, Karsten Borgwardt, Gunnar Rätsch, Tobias M. Merz

Abstract: Intensive care clinicians are presented with large quantities of patient information and measurements from a multitude of monitoring systems. The limited ability of humans to process such complex information hinders physicians to readily recognize and act on early signs of patient deterioration. We used machine learning to develop an early warning system for circulatory failure based on a high-res… ▽ More Intensive care clinicians are presented with large quantities of patient information and measurements from a multitude of monitoring systems. The limited ability of humans to process such complex information hinders physicians to readily recognize and act on early signs of patient deterioration. We used machine learning to develop an early warning system for circulatory failure based on a high-resolution ICU database with 240 patient years of data. This automatic system predicts 90.0% of circulatory failure events (prevalence 3.1%), with 81.8% identified more than two hours in advance, resulting in an area under the receiver operating characteristic curve of 94.0% and area under the precision-recall curve of 63.0%. The model was externally validated in a large independent patient cohort. △ Less

Submitted 19 April, 2019; v1 submitted 16 April, 2019; originally announced April 2019.

Comments: 5 main figures, 1 main table, 13 supplementary figures, 5 supplementary tables; 250ppi images

Small World with High Risks: A Study of Security Threats in the npm Ecosystem

Authors: Markus Zimmermann, Cristian-Alexandru Staicu, Cam Tenny, Michael Pradel

Abstract: The popularity of JavaScript has lead to a large ecosystem of third-party packages available via the npm software package registry. The open nature of npm has boosted its growth, providing over 800,000 free and reusable software packages. Unfortunately, this open nature also causes security risks, as evidenced by recent incidents of single packages that broke or attacked software running on millio… ▽ More The popularity of JavaScript has lead to a large ecosystem of third-party packages available via the npm software package registry. The open nature of npm has boosted its growth, providing over 800,000 free and reusable software packages. Unfortunately, this open nature also causes security risks, as evidenced by recent incidents of single packages that broke or attacked software running on millions of computers. This paper studies security risks for users of npm by systematically analyzing dependencies between packages, the maintainers responsible for these packages, and publicly reported security issues. Studying the potential for running vulnerable or malicious code due to third-party dependencies, we find that individual packages could impact large parts of the entire ecosystem. Moreover, a very small number of maintainer accounts could be used to inject malicious code into the majority of all packages, a problem that has been increasing over time. Studying the potential for accidentally using vulnerable code, we find that lack of maintenance causes many packages to depend on vulnerable code, even years after a vulnerability has become public. Our results provide evidence that npm suffers from single points of failure and that unmaintained packages threaten large code bases. We discuss several mitigation techniques, such as trusted maintainers and total first-party security, and analyze their potential effectiveness. △ Less

Submitted 7 June, 2019; v1 submitted 25 February, 2019; originally announced February 2019.

Comments: To appear in USENIX Security Symposium 2019

Enabling Communication Technologies for Automated Unmanned Vehicles in Industry 4.0

Authors: Amina Fellan, Christian Schellenberger, Marc Zimmermann, Hans D. Schotten

Abstract: Within the context of Industry 4.0, mobile robot systems such as automated guided vehicles (AGVs) and unmanned aerial vehicles (UAVs) are one of the major areas challenging current communication and localization technologies. Due to stringent requirements on latency and reliability, several of the existing solutions are not capable of meeting the performance required by industrial automation appli… ▽ More Within the context of Industry 4.0, mobile robot systems such as automated guided vehicles (AGVs) and unmanned aerial vehicles (UAVs) are one of the major areas challenging current communication and localization technologies. Due to stringent requirements on latency and reliability, several of the existing solutions are not capable of meeting the performance required by industrial automation applications. Additionally, the disparity in types and applications of unmanned vehicle (UV) calls for more flexible communication technologies in order to address their specific requirements. In this paper, we propose several use cases for UVs within the context of Industry 4.0 and consider their respective requirements. We also identify wireless technologies that support the deployment of UVs as envisioned in Industry 4.0 scenarios. △ Less

Submitted 29 November, 2018; v1 submitted 28 November, 2018; originally announced November 2018.

Comments: 7 pages, 1 figure, 1 table

Journal ref: International Conference on Information and Communication Technology Convergence (ICTC) (2018), 171-176

Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification

Authors: Andrea Orlandini, Martin Zimmermann

Abstract: This volume contains the proceedings of the Ninth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2018). The symposium took place in Saarbrücken, Germany, from the 26th to the 28th of September 2018. The GandALF symposium was established by a group of Italian computer scientists interested in mathematical logic, automata theory, game theory, and their application… ▽ More This volume contains the proceedings of the Ninth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2018). The symposium took place in Saarbrücken, Germany, from the 26th to the 28th of September 2018. The GandALF symposium was established by a group of Italian computer scientists interested in mathematical logic, automata theory, game theory, and their applications to the specification, design, and verification of complex systems. Its aim is to provide a forum where people from different areas, and possibly with different backgrounds, can fruitfully interact. GandALF has a truly international spirit, as witnessed by the composition of the program and steering committee and by the country distribution of the submitted papers. △ Less

Submitted 7 September, 2018; originally announced September 2018.

Journal ref: EPTCS 277, 2018

Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free (full version)

Authors: Daniel Neider, Alexander Weinert, Martin Zimmermann

Abstract: Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have been identified in the literature, among them the limited expressiveness, the lack of quantitative features, and the inability to express robustness. There is work on overcoming these shortcomings, but each of these is ty… ▽ More Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have been identified in the literature, among them the limited expressiveness, the lack of quantitative features, and the inability to express robustness. There is work on overcoming these shortcomings, but each of these is typically addressed in isolation. This is insufficient for applications where all shortcomings manifest themselves simultaneously. Here, we tackle this issue by introducing logics that address more than one shortcoming. To this end, we combine the logics Linear Dynamic Logic, Prompt-LTL, and robust LTL, each addressing one aspect, to new logics. For all combinations of two aspects, the resulting logic has the same desirable algorithmic properties as plain LTL. In particular, the highly efficient algorithmic backends that have been developed for LTL are also applicable to these new logics. Finally, we discuss how to address all three aspects simultaneously. △ Less

Submitted 29 April, 2021; v1 submitted 27 August, 2018; originally announced August 2018.

From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics

Authors: Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo Tabuada, Alexander Weinert, Martin Zimmermann

Abstract: Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.… ▽ More Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions. However, a wide range of formulas are not monitorable under this approach, meaning that they have a prefix for which satisfaction and violation will always remain undetermined no matter how it is extended. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category. Recently, a robust semantics for LTL was introduced to capture different degrees by which a property can be violated. In this paper we introduce a robust semantics for finite strings and show its potential in monitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we discuss which properties that come naturally in LTL monitoring - such as the realizability of all truth values - can be transferred to the robust setting. Lastly, we show that LTL formulas with robust semantics can be monitored by deterministic automata and report on a prototype implementation. △ Less

Submitted 12 September, 2022; v1 submitted 21 July, 2018; originally announced July 2018.

Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems

Authors: Matthew Hague, Roland Meyer, Sebastian Muskalla, Martin Zimmermann

Abstract: We give a direct polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games played over the same class of graphs. That a polynomial-time reduction would exist was known since both problems are complete for the same complexity class. Coming up with a direct reduction, however, has been an open problem. Our solution to the puzzle… ▽ More We give a direct polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games played over the same class of graphs. That a polynomial-time reduction would exist was known since both problems are complete for the same complexity class. Coming up with a direct reduction, however, has been an open problem. Our solution to the puzzle brings together a number of techniques for pushdown games and adds three new ones. This work contributes to a recent trend of liveness to safety reductions which allow the advanced state-of-the-art in safety checking to be used for more expressive specifications. △ Less

Submitted 5 July, 2018; v1 submitted 8 May, 2018; originally announced May 2018.