Search

Bachelorarbeit, RWTH Aachen University, 2022; Aachen : RWTH Aachen University 1 Online-Ressource : Illustrationen, Diagramme (2023). = Bachelorarbeit, RWTH Aachen University, 2022, Satisfiability Modulo Theories (SMT) solving is a technique used to determine the satisfiability of Quantifier-free First-order Logic formulae over a fixed theory. The Cylindrical Algebraic Decomposition (CAD) method is a commonly used strategy for solving problems of Non-linear Real Arithmetic. Recently, the Cylindrical Algebraic Covering (CAlC) method has been developed, which is a variant of the CAD method that incrementally tries to construct a satisfying solution for a conjunction of polynomial constraints or to detect its unsatisfiability. On the basis of a given variable and a partial assignment to some other variables, the main principle of the CAlC method is to generate single real values and open intervals of real numbers which can be omitted when searching for a satisfying solution.We present two adaptions of the CAlC method that exploit strict constraints in the input conjunction. Both aim at extending the generated open intervals to include some of their endpoints in order to speed up the computation., Published by RWTH Aachen University, Aachen

Dissertation, RWTH Aachen University, 2022; Aachen : RWTH Aachen University 1 Online-Ressource : Illustrationen, Diagramme (2022). = Dissertation, RWTH Aachen University, 2022, Railway systems are complex systems that are strongly affected by uncertainties like weather, technical problems, or demand. Despite these uncertainties, railway systems need to function efficiently. In general this thesis aims to advance the consideration of uncertainty in the railway planning process to optimally utilise the existing railway network capacity. The focus in this thesis is on the delays that result from the uncertain environmental conditions. To consider these in the railway planning process, a symbolic simulation algorithm is proposed to examine the delay propagation in a railway network for a given timetable. This allows to estimate the timetable robustness and the network capacity. Several performance indicators for railway timetables that can be evaluated using the symbolic simulation are discussed. To optimally utilise the network capacity also an algorithm to schedule additional freight trains is presented. The main contributions of this thesis are the following: 1. An algorithm to schedule additional freight trains is presented, to utilise the remaining network capacity without disturbing an existing timetable. 2. A novel symbolic simulation algorithm for railway timetables is proposed. The algorithm receives as input a railway infrastructure model, a corresponding timetable, and discrete primary delay distributions. It computes iteratively over time the delay propagation in the given railway system. Symbolic expressions are used to represent multiple possible values for the primary delays. This enables to simulate all discrete primary delay combinations at once. 3. An implementation of these algorithms is provided in C++ and evaluated on some real-world railway infrastructure networks and timetables based on the German railway system. The applicability and functionality of the algorithms is demonstrated. The proposed symbolic simulation algorithm is aimed to be a helpful addition to existing railway timetable simulations, which are mostly based on Monte Carlo simulation. In contrast to those, the symbolic approach stores the history of specific train states, which can be used to explain the occurring delays. In addition, the results of the symbolic simulation are exact with respect to the input model and the discrete primary delay distributions., Published by RWTH Aachen University, Aachen

Dissertation, RWTH Aachen University, 2021; Aachen : RWTH Aachen University 1 Online-Ressource : Illustrationen, Diagramme (2021). doi:10.18154/RWTH-2021-02027 = Dissertation, RWTH Aachen University, 2021, Büchi automata can be seen as a straight-forward generalization of ordinary NFA, adapted to handle infinite words. While they were originally introduced for applications in decidability of logics, they became a popular tool for practical applications, e.g. in automata-based approaches to model checking and synthesis problems. Being arguably both the simplest and most well-known variant in the zoo of so-called omega-automata that are considered in this setting, they serve as an intermediate representation of omega-regular specifications ofverification or synthesis requirements that are usually expressed in a more declarative fashion, e.g. using linear temporal logic. Unfortunately, nondeterministic automata are not directly suitable for certain applications, whereas deterministic Büchi automata are less expressive. This problem is usually solved by either constructing deterministic automata of a different kind, or by restricting their ambiguity, i.e., the maximal number of accepting runs on some word. In both cases, the transformation is expensive, yielding an exponential blow-up of the state space in the worst case. Therefore, optimized constructions and heuristics for common special cases are useful and in demand for actual practical applications. In this thesis new results concerning both approaches are presented. On one hand, we present a new general construction for determinization from nondeterministic Büchi to deterministic parity automata that unifies the dominant branches of previous approaches based on the Safra construction and the Muller-Schupp construction. Additionally, we provide a set of new heuristics, some of which exploit properties of our unified construction. Furthermore, we characterize the ambiguity of Büchi automata by a hierarchy that is determined by simple syntactical patterns in the automata, and present a new construction that reduces the ambiguity of an automaton. Apart from the classical nondeterministic and deterministic variants of automata, it is natural to consider probabilistic automata, i.e., automata that instead of utilizing nondeterminism use a probability distribution on the states to decide which state to go to next. It is known that in general, such automata are more expressive than classical automata. We show that subclasses of probabilistic automata that correspond to certain classes of the previously mentioned ambiguity hierarchy are not more expressive than classical automata, providing constructions to obtain classical Büchi automata from them., Published by RWTH Aachen University, Aachen

Dissertation, RWTH Aachen University, 2020; Aachen 1 Online-Ressource (96 Seiten) : Illustrationen, Diagramme (2020). = Dissertation, RWTH Aachen University, 2020, Planning for real-world applications requires algorithms and tools with the ability to handle the complexity such scenarios entail. However, meeting the needs of such applications poses substantial challenges, both representational and algorithmic. On the one hand, expressive languages are needed to build faithful models. On the other hand, efficient solving techniques that can support these languages need to be devised. A response to this challenge is underway, and the past few years witnessed a community effort towards more expressive languages, including decidable fragments of first-order theories. In this work we focus on planning with arithmetic theories and propose Optimal Planning Modulo Theories, a framework that attempts to provide efficient means of dealing with such problems. Leveraging generic Optimization Modulo Theories (OMT) solvers, we first present domain-specific encodings for optimal planning in complex logistic domains. We then present a more general, domain-independent formulation that allows to extend OMT planning to a broader class of well-studied numeric problems in planning. To the best of our knowledge, this is the first time OMT procedures are employed in domain-independent planning., Published by Aachen

Masterarbeit, RWTH Aachen University, 2020; Aachen 79 Seiten (2020). = Masterarbeit, RWTH Aachen University, 2020, Published by Aachen

Satisfiability modulo theories solving is a technology to solve logically encoded problems for many applications like verification, testing, or planning. Among the many theories that are considered within this logical framework, nonlinear real arithmetic stands out as particularly challenging, yet decidable and sufficiently well understood from a mathematical perspective. The most prominent approach that can decide upon nonlinear real questions in a complete way is the cylindrical algebraic decomposition method. We explore the usage of the cylindrical algebraic decomposition method for satisfiability modulo theories solving, both theoretically and experimentally. This method is commonly understood as an almost atomic procedure that gathers information about an algebraic problem and then allows to answer all kinds of questions about this algebraic problem afterward. We essentially break up this method into smaller components that we can then process in varying order to derive the particular piece of information - whether the problem is satisfiable or unsatisfiable - allowing to avoid some amount of computations. As this method often exhibits doubly exponential running time, these savings can be very significant in practice. We furthermore embed this method in the regular satisfiability modulo theories framework where the cylindrical algebraic method is faced with a sequence of problems that are “related” in the sense that they usually share large parts of their problem statements. We devise different approaches to retain information from a previous run so that it can be reused when the problem is only “extended” as well as purging now obsolete information if the problem is “reduced”. These variants change in how much information can be reused, the granularity of the information that is removed, and how much bookkeeping needs to be done. This integration is then enhanced with techniques that are more or less well-known in the computer algebra community, for example, different projection operators, equational constraints, or employing the so-called resultant rule. Furthermore, we present novel features necessary for an efficient embedding in the satisfiability modulo theories frame-work like infeasible subset computations and early termination as well as extensions to integer problems and optimization problems. We then turn to an alternative approach to satisfiability modulo theories solving that is commonly called model-constructing satisfiability calculus. The core idea of this framework is to integrate the theory reasoning, in particular the construction of a theory model, tightly with the Boolean reasoning. The most popular theory reasoning engine is again based on the cylindrical algebraic decomposition method, though we focus on the overall framework here. We start with our own variant of the model-constructing satisfiability calculus and discuss some general insights and changes compared to current implementations. We then proceed to present a whole series of reasoning engines for arithmetic problems and show how a proper (though still naive) combination of those serves to significantly improve a practical solver. We also show how the tight integration into the Boolean reasoning allows for novel strategies for notoriously hard problems like the theory variable ordering or expedient cooperation between the Boolean and the theory reasoning. Finally, we consider the theoretical relation of the model-constructing satisfiability calculus to other proof systems, in particular, the aforementioned regular satisfiability modulo theories solving. Under certain assumptions - that turn out to be instructive in and of themselves - we show that they are equivalent with respect to their proof complexity and even establish what we call “algorithmic equivalency” afterward.

Dissertation, RWTH Aachen University, 2019; Aachen 1 Online-Ressource (217 Seiten) : Illustrationen, Diagramme (2019). = Dissertation, RWTH Aachen University, 2019, Hybrid systems in computer science are systems with combined discrete-continuous behavior. This work presents results obtained in the field of safety verification for linear hybrid systems whose continuous behavior can be described by linear differential equations. We focus on a special technique named flowpipe-construction-based reachability analysis, which over-approximates the reachable states of a given hybrid system as a finite union of state sets. In these computations we can use different geometric and symbolic representations for state sets as datatypes. The choice of the state set representation has a strong impact on the precision of the approximation and on the running time of the analysis method. Additionally, numerous further parameters and heuristics influence the analysis outcome. In this work we investigate on the influence and optimal usage of these parameters. Our results are collected in a publicly available open-source C++ programming library named HyPro. The major contributions of this work are threefold: 1) We present our HyPro library offering implementations for several state set representations that are commonly used in flowpipe-construction-based reachability analysis. A unified interface in combination with reduction and conversion methods supports the fast implementation of versatile analysis methods for linear hybrid systems. 2) We put our library to practice and show its applicability by embedding a flowpipe-construction-based reachability analysis method in a CEGAR-based abstraction refinement framework. The parallelization of this approach further increases its performance. 3) We introduce methods to decompose the search space and replace high-dimensional computations by computations in lower-dimensional subspaces. This method is applicable under certain conditions. An automated check of these conditions, an automated decomposition, and the integration of dedicated analysis methods for subspace computations extend our approach., Published by Aachen

Dissertation, RWTH Aachen University, 2018; Aachen 1 Online-Ressource (ii, 222 Seiten) : Illustrationen, Diagramme (2019). = Dissertation, RWTH Aachen University, 2018, Quantifier-free real-algebraic formulas are Boolean combinations of polynomial equations and inequalities over the domain of the real numbers. Coming with a strong expressiveness and a still decidable satisfiability problem, real-algebraic formulas are a precious modeling language in many academic, industrial and commercial areas. However, only some classes of real-algebraic formulas allow an efficient solving in practice. For instance, conjunctions of linear real-algebraic constraints can be solved with the very successful simplex method. The virtual substitution method can solve also formulas containing quadratic polynomials and, based on recent developments, also polynomials of higher degrees. Other examples are solving methods based on interval constraint propagation, which are able to deal with even more expressive formulas, e.g.~including trigonometric functions. Although those computations are not always terminating with a conclusive answer, they often lead to a reliable result in a short running time. Further special examples are solving techniques based on Gröbner bases. They can be used to solve real-algebraic formulas in combination with other techniques, making the implementation a challenging task. The general quantifier-free real-algebraic satisfiability problem, however, has a worst-case time complexity bound which is exponential in the number of input variables. Methods solving this general problem directly are often inefficient in practice. The most popular method in this respect is the cylindrical algebraic decomposition (CAD) method. Its search space can grow doubly-exponentially with the number of input variables. Thus, its practical usefulness highly depends on search heuristics and search space pruning. In this thesis, both aspects are shed light on. In particular, the CAD method is analyzed in combination with other more specialized solving methods such as Gröbner bases. Moreover, bounds to the variables are used to prune the CAD search space, especially when combining the method with interval-arithmetic techniques. This thesis tackles the solving of general quantifier-free real-algebraic formulas with a combination of different methods in a satisfiability-modulo-theories (SMT) framework: A SAT solver computes partial assignments for the Boolean structure of the real-algebraic formula and real-algebraic solvers check these assignments for consistency in the real domain. If the assignment is infeasible in the real domain, the SAT solver would profit from a small reason for this conflict in terms of a subset of the constraints corresponding to the conflicting assignment. Preferably minimal reasons are a valuable good in an SMT solver. As a main part, this thesis comprises a description and evaluation of their computation using the CAD method. In addition, the new and interesting approach for real-algebraic solving by computing realizable sign conditions is analyzed in terms of its adaptability to the SMT framework., Published by Aachen

Dissertation, RWTH Aachen University, 2018; Aachen 1 Online-Ressource (iv, 163 Seiten) : Illustrationen (2018). = Dissertation, RWTH Aachen University, 2018, The operation of a system or process can be studied by simulation. A simulation of a system starts with designing and developing a model of the selected (actual or theoretical) system by considering its key characteristics and behaviors. Computer simulation is to execute the corresponding model on a digital computer and analyze the results of the execution. The purpose of simulation is to examine and analyze the effect of different conditions or changes on a system. In case that a computer simulation model needs to be optimized, an optimization algorithm should be applied on it. Due to dependence of a lot of numerical algorithms for optimization on derivative information of the underlying problem, efficient evaluation of the derivatives is very important. In the case that the derivative information of the simulation system is required (for example for optimization), the derivatives of its embedded systems should be evaluated. Nonlinear systems are the systems in which the output is not directly roportional to the input and this is the case in many mathematical and physical systems. The Navier-Stokes equations in fluid dynamics are examples of nonlinear differential equations. In physics, integration is used very often, for example, for computing the work, where work is the integral of force over a distance, or as another example, for computing electric flux, which is the integral of the electric field over a surface. According to the above mentioned systems, there exists many simulation systems with embedded nonlinear systems and/or embedded (one- or multidimensional) integrals. For optimization of the corresponding simulation systems with a derivative-based method, the derivatives of the embedded integral(s) and embedded nonlinear equation(s) should also be evaluated. Therefore, different approaches to compute the derivatives of integrals and nonlinear equations are compared in terms of computational complexity, memory requirement and convergence and at the end, one will be able to choose the optimal differentiation method in case of having nonlinear system and/or (one- or multidimensional) integral in the system. On the other hand, the derivatives are not only needed for optimization, but also for example for approximating a function applying Taylor series. Considering the fact that a function can be approximated by using a finite number of terms of its Taylor series, the derivatives are also used for this approximation and if a certain amount of precision is required, higher-order derivatives should be computed, therefore, it is also crucial to have an efficient evaluation of the higher-order derivatives. The goal is to choose the better differentiation alternative in case of evaluating the first- and higher-order derivatives of a system with embedded nonlinear system and/or (one- or multidimensional) integral in terms of run time and memory requirement., Published by Aachen

Em muitas aplicações de métodos formais, como verificação formal, síntese de programas, testes automáticos e análise de programas, é comum depender de solucionadores de satisfatibilidade módulo teorias (SMT) como backends para resolver automaticamente condições que precisam ser verificadas e fornecer certificados de seus resultados. Nesta tese, objetivamos melhorar a eficiência dos solucionadores SMT e aumentar sua confiabilidade. Nossa primeira contribuição é fornecer um arcabouço uniforme e eficiente para raciocinar com fórmulas quantificadas em solucionadores SMT, em que, geralmente, várias técnicas de instanciação são empregadas para lidar com quantificadores. Mostramos que as principais técnicas de instanciação podem ser lançadas neste arcabouço unificador para lidar com fórmulas quantificadas com igualdade e funções não interpretadas. O arcabouço baseia-se no problema de E-ground (dis)unificação, uma variação do problema clássico de E-unificação rígida. Apresentamos um cálculo correto e completo para resolver esse problema na prática: Fechamento de Congruência com Variáveis Livres (CCFV). Uma avaliação experimental é apresentada, na qual medimos o impacto das otimizações e técnicas de instanciação baseadas no CCFV nos solucionadores SMT veriT e CVC4. Mostramos que nossas implementações exibem melhorias em relação às abordagens de última geração em várias bibliotecas de referência, decorrentes de aplicações do mundo real. Nossa segunda contribuição é uma estrutura para o processamento de fórmulas ao mesmo tempo que produz demonstrações detalhadas. Nosso objetivo é aumentar a confiabilidade nos resultados de solucionadores SMT e sistemas de raciocínio automatizado similares, fornecendo justificativas que podem ser verificadas com eficiência de forma independente e para melhorar sua usabilidade por aplicativos externos. Os assistentes de demonstração, por exemplo, geralmente requerem a reconstrução da justificação fornecida pelo solucionador em uma determinada obrigação de prova. Os principais componentes da nossa estrutura de produção de demonstrações são um algoritmo genérico de recursão contextual e um conjunto extensível de regras de inferência. Clausificação, Skolemização, simplificações específicas de teorias e expansão das expressões "let" são exemplos dessa estrutura. Com estruturas de dados adequadas, a geração de demonstrações cria apenas uma sobrecarga de tempo linear, e as demonstrações podem ser verificadas em tempo linear. Também implementamos a abordagem em veriT. Isso nos permitiu simplificar drasticamente a base do código, aumentando o número de problemas para os quais demonstrações detalhadas podem ser produzidas. In many formal methods applications it is common to rely on SMT solvers to automatically discharge conditions that need to be checked and provide certificates of their results. In this thesis we aim both to improve their efficiency of and to increase their reliability. Our first contribution is a uniform framework for reasoning with quantified formulas in SMT solvers, in which generally various instantiation techniques are employed. We show that the major instantiation techniques can be all cast in this unifying framework. Its basis is the problem of E-ground (dis)unification, a variation of the classic rigid E-unification problem. We introduce a decision procedure to solve this problem in practice: Congruence Closure with Free Variables (CCFV). We measure the impact of optimizations and instantiation techniques based on CCFV in the SMT solvers veriT and CVC4, showing that our implementations exhibit improvements over state-of-the-art approaches in several benchmark libraries stemming from real world applications. Our second contribution is a framework for processing formulas while producing detailed proofs. The main components of our proof producing framework are a generic contextual recursion algorithm and an extensible set of inference rules. With suitable data structures, proof generation creates only a linear-time overhead, and proofs can be checked in linear time. We also implemented the approach in veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced.

Rheinisch-Westfälischen Technischen Hochschule Aachen, Diss., 2017; Aachen, 1 Online-Ressource (221 Seiten) : Illustrationen, Diagramme(2017). = Rheinisch-Westfälischen Technischen Hochschule Aachen, Diss., 2017, Calculation and assessment of overall capacity in railway networkOne of the main objectives of railway operation research is the assessment and evalua-tion of railway capacity. In this context, capacity denotes the possible number of train runs, which can be operated on the infrastructure compliant to a predefined level of ser-vice.In view of the forecasted increase of rail traffic in Europe the optimal use of the existing infrastructure is becoming increasingly important. In this regard, the analysis of the re-sidual capacity of railway stations and lines, respectively, is an essential prerequisite to assess the feasibility of additional traffic volume in the network. In medium- and long-term planning of infrastructure and operations analytical queueing-based approaches have been widely used to determine the capacity. Besides being ap-plicable to existing timetables these methods are particularly suited to cope with uncer-tain input, e.g. if only a rough operational concept, but no precise timetable exists. Ac-cording to the state of the art in this sector, the railway network is generally decomposed into smaller infrastructure elements such as lines, set of tracks and route nodes. In terms of capacity, these elements are investigated individually, whereas interdependencies between different elements and the capacity of the entire network cannot be assessed, globally. However, it is precisely the overall capacity, and not the individual results for lines and nodes, which are of particular interest for infrastructure and timetable planning.The goal of this thesis is to provide an approach enabling the optimal utilization of the available capacity in railway networks. By taking a network perspective on capacity in-cluding alternative train routings the developed method allows for a detailed description and capacity evaluation of infrastructure modifications. Apart from the identification and prevention of system bottlenecks in infrastructure planning it also provides valuable in-sights in timetable design facilitating a demand oriented design of operations. At this point, the approach is not limited to the construction of new timetables from scratch, but can also be used to optimally attribute residual capacities to additional train runs in exist-ing timetables. In the present work, the calculation and assessment of overall capacity in railway net-works is performed using a macroscopic model based on railway lines, set of tracks and route nodes. The capacity allocation for train courses is based on a two-stage model. The first step consists of finding all economically feasible train paths for the demanded relations by solving a shortest-path problem. In the second process step, infrastructure capacity is assigned to individual trains using a mixed-integer programming approach. The objective of the routing problem is to maximize the number of feasible train runs through the network. The capacity is determined based on a train specific extrapolation of the existing operating program on each infrastructure section.To determine the individual capacities of lines, set of tracks and route nodes, which pro-vide constraints to the routing MIP commonly used analytical procedures in railway ca-pacity analysis are used. Currently, these procedures rely on differing modeling tech-niques and input data requirements. Capacity analysis of railway stations, for example, usually relies on so-called scheduled waiting times, which originate in timetabling when trains need to be shifted from their original timeslots due to conflicts with other train runs. The assessment of railway lines, by contrast, is performed based on knock-on delays, which arise in operations due to conflicts between trains arising from perturbations or initial delays in the planned timetable. In order to ensure the comparability of the calcula-tion of the capacities for the different infrastructure elements, a methodology for the standardization of the different approaches is developed. For example, the applicability of the Strele-formula – which has previously been used to model railway lines – has been extended to route nodes by incorporating a parameter concatenating different train moves. For the first time, the calculation of capacity for railway lines and railway nodes can now be carried out based on the same database.The presented approach has been validated based on prototypical calculations for a realistic subnetwork of the size of North Rhine-Westphalia. The network consists of 51 set of tracks, 102 route nodes and 150 railway lines. It has been shown that, by optimally assigning residual network capacity based on the developed method, the number of train runs on this network can be increased by up to 18%. The methodology hence provides a significant improvement in network and timetable planning., Published by Aachen

Clinical pathways are care plans which detail essential steps in the care of patients with a specific clinical problem, usually a chronic disease. A pathway includes recommendations of medications prescribed at different stages of the care plan. For patients with three or more chronic diseases (known asmultimorbidities) the multiple pathways have to be applied together. One common problem for such patients is the adverse interaction between medications given for different diseases. This paper proposes a solution for avoiding medication conflicts for patients with multimorbidities through the use of formal methods. We introduce the notion of a pharmaceutical graph to capture the medications associated to different stages of a pathway. We then explore the use of an optimising SMT solver (Z3) to quickly find the set of medications with the minimal number and severity of conflicts which is assumed to be the safest. We evaluate the approach on a well known case of an elderly patient with five multimorbidities. Postprint

RWTH Aachen University, Diss., 2016; 186 pp., (2016)., This thesis addresses the integration of real algebraic procedures as theory solvers into satisfiability modulo theories (SMT) solvers, in order to check non-linear real- and integer-arithmetic formulas for satisfiability. There are plenty of procedures to choose from and we aim for a general framework that allows us to select and combine them. The main part of this thesis concerns one specific example of the aforementioned integration: the virtual substitution method. Here we also optimize this method with respect to satisfiability checking and extend it such that it can be used for integer arithmetic., Published by Aachen

International audience; Microservices is an emerging paradigm for the development of distributed systems that, originating from Service-Oriented Architecture , focuses on the small dimension, the loose coupling, and the dynamic topology of services. Microservices are particularly appropriate for the development of distributed systems in the Cloud. However, their dynamic nature calls for suitable techniques for their automatic deployment. In this paper we address this problem and we propose JRO (Jolie Redeploy-ment Optimiser), a tool for the automatic and optimised deployment of microservices written in the Jolie language. The tool uses Zephyrus, a state of the art tool that automatically generates a fully detailed Service-Oriented Architecture configuration starting from a partial and abstract description of the target application.

This thesis deals with analysis and synthesis methods and their application in the area of engineering. In the first part, we show the application of formal methods in chemical plant control to verify safety critical properties. In general, not only the control program but also the controlled system are relevant to prove a set of requirements. Thus, we show how a hybrid automaton can be generated automatically, that models the controller, its cyclic execution, and the dynamic plant behavior.We propose verification techniques based on counterexample-guided abstraction refinement (CEGAR) to keep the model sizes moderate. However, existing analysis tools do not compute counterexamples for models beyond timed automata. Thus, we present different methods to over-approximate the set of counterexamples for hybrid automata and we employ simulation techniques to validate counterexamples.Afterwards, we develop two CEGAR approaches for our application scenario. The first one starts with an analysis on a purely discrete model. For each discrete counterexample, a reachability analysis that is guided along the discrete counterexample is computed on the hybrid system model. The second approach uses reachability analysis for hybrid systems and abstracts away parts of the dynamic plant behavior.Finally, we show that some special characteristics of our models can be exploited during the analysis to reduce the computation time and to increase the accuracy of the computed reachable state set.In the second part of this thesis, we switch to the synthesis of control strategies for parallel hybrid vehicles where an internal combustion engine and an electrical motor are coupled on the same axis. A control strategy distributes the requested torque over the available engines.We implement a control strategy that optimizes the control using a GA. The basis of this control strategy is our GA library GeneiAL. We analyze the control strategy to determine real-time capable configurations with good optimization results. For promising configurations, we compare the GA-based control strategy with common control strategies. Moreover, we report on the integration of this set of control strategies into a learning-based control strategy. A learning-based control strategy optimizes the fuel consumption using a set of control strategies as experts. We can show that the fuel consumption of the learning-based control strategy is comparable to the fuel consumption of the best expert. On all benchmarks, GA-based control strategies turn out to be the best experts.

The topic of this thesis is roughly to be classified into the formal verification of probabilistic systems. In particular, the generation of counterexamples for discrete-time Markov Models is investigated. A counterexample for discrete-time Markov Chains (DTMCs) is classically defined as a (finite) set of paths. In this work, this set of paths is represented symbolically as a critical part of the original system, a so-called critical subsystem. This notion is extended to Markov decision processes (MDPs) and probabilistic automata (PAs). The results are introduced in four parts: 1. A model checking algorithm for DTMCs based on a decomposition of the system's graph in strongly connected components (SCCs). This approach is extended to parametric discrete-time Markov Chains. 2. The generation of counterexamples for DTMCs and reachability properties based on graph algorithms. A hierarchical abstraction scheme to compute abstract counterexamples is presented, followed by a general framework for both explicitly represented systems and symbolically represented systems using binary decision diagrams (BDDs). 3. The computation of minimal critical subsystems using SAT modulo theories (SMT) solving and mixed integer linear programming (MILP). This is investigated for reachability properties and $\omega$-regular properties on DTMCs, MDPs, and PAs. 4. A new concept of high-level counterexamples for PAs. Markov models can be specified by means of a probabilistic programming language. An approach for computing critical parts of such a symbolic description of a system is presented, yielding human-readable counterexamples. All results have been published in conference proceedings or journals. A thorough evaluation on common benchmarks is given comparing all methods and also competing with available implementations of other approaches.

With the ubiquitous use of computers in controlling physical systems, it requires to have a new formalism that could model both continuous flows and discrete jumps. Hybrid systems are introduced to this purpose. A hybrid system, which is modeled by a hybrid automaton in the thesis, is equipped with finitely many discrete modes and continuous real-valued variables. A state of it is then represented by a mode along with a valuation of the variables. Given that the system is in a mode l, the variable values are changed continuously according to the Ordinary Differential Equation (ODE) associated to l, or discretely by a jump starting from l. The thesis focuses on the techniques to compute all reachable states over a bounded time horizon and finitely many jumps for a hybrid system with non-linear dynamics. The results of that can then be used in safety verification of the system.Although a great amount of work has been devoted to the reachability analysis of hybrid systems with linear dynamics, there are few effective approaches proposed for the non-linear case which is very often in applications. The difficulty is twofold. Firstly, it is not easy to find an over-approximation with acceptable accuracy for a set of the solutions of a non-linear ODE. Secondly, to detect and compute the reachable states under a jump requires solving non-linear real arithmetic problems which is also difficult in general. In the thesis, we present our approaches to deal with the above difficulties. For the first one, we present the use of Taylor models as the over-approximate representations for non-linear ODE solutions. Our work can be viewed as a variant of the Taylor model method proposed by Berz et al., such that we are able to efficiently deal with some examples with more than $10$ variables. Besides, we also extend the work of Lin and Stadtherr to handle the ODEs with bounded time-varying parameters. For the second difficulty, we present two techniques: (a) domain contraction and (b) range over-approximation to compute an enclosure for the reachable set from which a jump is enabled. They can be seen as Satisfiability Modulo Theories (SMT) solving algorithms which are specialized for the reachability analysis of hybrid systems. In order to reduce the computational cost, we also propose different heuristics for aggregating Taylor models. Besides the above contributions, we describe a method to fast generate Taylor model over-approximations for linear ODE solutions. Its performance is demonstrated via a comparison with the tool SpaceEx. To make our methods accessible by other people, we implement them in a tool named Flow*. To examine the effectiveness, we thoroughly compare it with some related tools which are popularly used, according to their functionalities, over a set of non-trivial benchmarks that are collected by us from the areas of mechanics, biology, electronic engineering and medicine. From the experimental results, the advantage of Flow* over the other tools becomes more apparent when the scale of the system grows. On the other hand, it also shows that Flow* can be applied to analyzing realistic systems.

The branch displacement problem is a well-known problem in assembler design. It revolves around the feature, present in several processor families, of having different instructions, of different sizes, for jumps of different displacements. The problem, which is provably NP-hard, is then to select the instructions such that one ends up with the smallest possible program.\ud \ud During our research with the CerCo project on formally verifying a C compiler, we have implemented and proven correct an algorithm for this problem. In this paper, we discuss the problem, possible solutions, our specific solutions and the proofs.

This paper presents APTE, a new tool for automatically proving the security of cryptographic protocols. It focuses on proving trace equivalence between processes, which is crucial for specifying privacy type properties such as anonymity and unlinkability.\ud \ud The tool can handle protocols expressed in a calculus similar to the applied-pi calculus, which allows us to capture most existing protocols that rely on classical cryptographic primitives. In particular, APTE handles private channels and else branches in protocols with bounded number of sessions. Unlike most equivalence verifier tools, APTE is guaranteed to terminate\ud \ud Moreover, APTE is the only tool that extends the usual notion of trace equivalence by considering ``side-channel'' information leaked to the attacker such as the length of messages and the execution times. We illustrate APTE on different case studies which allowed us to automatically (re)-discover attacks on protocols such as the Private Authentication protocol or the protocols of the electronic passports.