http://dl.gi.de/handle/20.500.12116/37950 2026-07-21T13:36:19Z 2026-07-21T13:36:19Z Moradkhani, Farzaneh Fränzle, Martin http://dl.gi.de/handle/20.500.12116/37955 2022-01-18T11:31:09Z 2021-01-01T00:00:00Z

Functional verification of cyber-physical systems containing machine-learnt components Moradkhani, Farzaneh; Fränzle, Martin Functional architectures of cyber-physical systems increasingly comprise components that are generated by training and machine learning rather than by more traditional engineering approaches, as necessary in safety-critical application domains, poses various unsolved challenges. Commonly used computational structures underlying machine learning, like deep neural networks, still lack scalable automatic verification support. Due to size, non-linearity, and non-convexity, neural network verification is a challenge to state-of-art Mixed Integer linear programming (MILP) solvers and satisfiability modulo theories (SMT) solvers [2], [3]. In this research, we focus on artificial neural network with activation functions beyond the Rectified Linear Unit (ReLU). We are thus leaving the area of piecewise linear function supported by the majority of SMT solvers and specialized solvers for Artificial Neural Networks (ANNs), the successful like Reluplex solver [1]. A major part of this research is using the SMT solver iSAT [4] which aims at solving complex Boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and therefore is suitable to verify the safety properties of a specific kind of neural network known as Multi-Layer Perceptron (MLP) which contain non-linear activation functions.

2021-01-01T00:00:00Z Berani Abdelwahab, Erzana Fränzle, Martin http://dl.gi.de/handle/20.500.12116/37956 2022-01-18T11:31:09Z 2021-01-01T00:00:00Z

A sampling-based approach for handling delays in continuous and hybrid systems Berani Abdelwahab, Erzana; Fränzle, Martin Delays in feedback dynamics of coupled dynamical systems arise regularly, especially in embedded control where the physical plant and the controller continuously interact through digital networks. Systems featuring delays are however notoriously difficult to analyze. Consequently, formal analysis often addresses simplified, delay-free substitute models, risking negligence of the adverse impact of delay on control performance. In this ongoing work, we demonstrate that for continuous systems such as delay differential equations, a major part of the delay-induced complexity can be reduced effectively when adding natural constraints to the model of the delayed feedback channel, namely that it transports a band-limited signal and implements a non-punctual, distributed delay. The reduction is based on a sampling approach which is applicable when the above conditions on the feedback are satisfied. We further discuss the possibilities of lifting this method to mixed discrete-continuous dynamics of delayed hybrid systems and the open issues thereof.

2021-01-01T00:00:00Z Özkan, Okan http://dl.gi.de/handle/20.500.12116/37958 2022-01-18T11:31:09Z 2021-01-01T00:00:00Z

Infinite-state graph transformation systems under adverse conditions Özkan, Okan We present an approach for modeling adverse conditions by graph transformation systems. To this end, we introduce joint graph transformation systems which involve a system, an interfering environment, and an automaton modeling their interaction. For joint graph transformation systems, we present notions of correctness under adverse conditions. Some instances of correctness are expressible in LTL (linear temporal logic), or in CTL (computation tree logic), respectively. In these cases, verification of joint graph transformation systems is reduced to temporal model checking. To handle infinite state spaces, we incorporate the concept of well-structuredness. We discuss ideas for the verification of joint graph transformation systems using results based on well-structuredness.

2021-01-01T00:00:00Z Würdemann , Nick http://dl.gi.de/handle/20.500.12116/37959 2022-01-18T11:31:09Z 2021-01-01T00:00:00Z

Exploiting symmetries of high-level Petri games in distributed synthesis Würdemann , Nick Distributed Synthesis is the problem of automatically generating correct controllers for individual agents in a distributed system. Petri games model this problem by a game between two teams of players on a Petri net structure. Under some restrictions, Petri games can be solved by a reduction to a two player game. The concept of symmetries in Petri nets is closely related to high-level representations of Petri games. Applying symmetries to the states in the two-player game results in a significant state space reduction. We give an overview about (high-level) Petri games and the application of symmetries in this setting. We present ongoing work aiming to concisely describe solutions of Petri games by a high-level representation.

2021-01-01T00:00:00Z