AVACS - Subproject H4: Automatic Verification of Hybrid System Stability
Start of the project 2004, end of the project 2016
Description of the
Hybrid systems are control systems that can contain both continuous-time behaviour and discrete state jumps. They therefore represent a combination of classical controllers (continuous-time) and computer-aided controllers (discrete-time) and are therefore particularly relevant in practice. Hybrid models are used, for example, for modelling embedded systems, biological systems or industrial processes. Stability refers to the property that temporally limited disturbances of the system do not permanently influence the behaviour, but are independently compensated by the system. A stable control system is therefore inherently robust against unforeseen disturbances. Stability is a liveness property of a system and is therefore usually difficult to prove. We concentrate on the proof of so-called asymptotic stability. A control system is globally asymptotically stable if it ultimately settles to a rest point for every possible initial state in the absence of disturbances. This resting point can be regarded as the desirable state of the system. The consequence is robustness against temporary disturbances of the system: the system will always return to the vicinity of the resting point when the disturbance effects subside. The proof of such a property can be provided by means of Lyapunov functions. Such a function can be understood as a measure of the energy of the system. If it is ensured that the energy minimum lies at the rest point and that the energy level continuously decreases over time, this can be used to prove global asymptotic stability. The central problem here is that such a function must be found -- this is a non-trivial task. The problem of finding such a Lyapunov function can be transformed into an efficiently solvable optimisation problem whose optimal solution is the parameterisation of such a Lyapunov function. Our goal is to advance these computational methods so that they can be integrated into verification tools. For example, decomposition methods are used that break down a large, possibly not numerically robust optimisation problem into several more robust ones. This makes it possible to analyse more complex systems than would otherwise be possible. Furthermore, we deal with the extension of these methods to systems with probabilistic behaviour and time delays.
J. Oehlerking, A. Dhama, and O. E. Theel, "Towards Automatic Convergence Verification of Self-Stabilizing Algorithms" in Proc. Self-Stabilizing Systems, 7th International Symposium, SSS 2005, 2005.
doi: 10.1007/11577327_14
@inproceedings{Oehlerking2005a,
author = {Jens Oehlerking and Abhishek Dhama and Oliver E. Theel},
title = {Towards Automatic Convergence Verification of Self-Stabilizing Algorithms},
editor = {Ted Herman and S{\'{e}}bastien Tixeuil},
booktitle = {Self-Stabilizing Systems, 7th International Symposium, {SSS} 2005},
pages = {198-213},
year = {2005},
url = {http://dx.doi.org/10.1007/11577327_14},
doi = {10.1007/11577327_14},
series = {Lecture Notes in Computer Science},
volume = {3764},
publisher = {Springer},
isbn = {3-540-29814-2},
volume = {3764},
abstract = {The verification of the self-stabilization property of a distributed algorithm is a complicated task. By exploiting certain analogies between self-stabilizing distributed algorithms and globally asymptotically stable feedback systems, techniques originally developed for the verification of feedback system stability can be adopted for the verification of self-stabilization of distributed algorithms. In this paper, we show how for a certain subclass of dynamic systems -- namely piecewise affine hybrid systems -- and distributed algorithms suitable to be modeled in terms of these dynamic systems, a proof of convergence can be obtain fully automatically. Together with some additional non-automated arguments, the complete proof of self-stabilization can be derived.},
}
J. Oehlerking, H. Burchardt, and O. E. Theel, "Towards Automatic Verification of Affine Hybrid System Stability" SIGBED Review,Special Issue on IEEE RTAS 2005 Work-in-Progress, vol. 2, iss. 2, p. 27.
2005.
doi: 10.1145/1121788.1121797
@article{Oehlerking2005,
author = {Jens Oehlerking and Henning Burchardt and Oliver E. Theel},
title = {Towards Automatic Verification of Affine Hybrid System Stability},
journal = {{SIGBED} Review,Special Issue on IEEE RTAS 2005 Work-in-Progress},
volume = {2},
number = {2},
pages = {27–30},
month = {apr},
year = {2005},
issn = {1551-3688},
url = {http://doi.acm.org/10.1145/1121788.1121797},
doi = {10.1145/1121788.1121797},
acmid = {1121797},
publisher = {ACM},
address = {New York, NY, USA},
}
H. Burchardt, J. Oehlerking, and O. Theel, "The Role of State-space Partitioning in Automated Verification of Affine Hybrid System Stability" in Proc. Proceedings of the 3rd International Conference on Computing, Communications and Control Technologies, 2005, p. 187.
@inproceedings{Burchardt2005a,
author = {Henning Burchardt and Jens Oehlerking and Oliver Theel},
title = {The Role of State-space Partitioning in Automated Verification of Affine Hybrid System Stability},
booktitle = {Proceedings of the 3rd International Conference on Computing, Communications and Control Technologies},
year = {2005},
volume = {1},
pages = {187–192},
abstract = {In this paper we examine methods for automatic stability verification of hybrid feedback control systems. We utilize a linear matrix inequality approach that allows efficient computation of a Lyapunov-like energy function by partitioning the state space and finding a separate function for each region. The prerequisites for automation of this method are presented in detail. These include the choice of a suitable state space partitioning and knowledge about possible transitions between those regions. An algorithm for the latter problem is outlined, as well as examples that illustrate how to suitably choose partitionings.},
keywords = {stability, hybrid systems, Lyapunov functions, piecewise affine systems, linear matrix inequalities, partitioning},
}
H. Burchardt, J. Oehlerking, and O. E. Theel, "Towards Push-of-a-Button Stability Verification for Discrete-Time Hybrid Systems" in Proc. 11th IEEE Pacific Rim International Symposium on Dependable Computing, Los Alamitos, CA, USA, 2005.
doi: 10.1109/PRDC.2005.59
@inproceedings{Burchardt2005,
author = {Henning Burchardt and Jens Oehlerking and Oliver E. Theel},
title = {Towards Push-of-a-Button Stability Verification for Discrete-Time Hybrid Systems},
booktitle = {11th {IEEE} Pacific Rim International Symposium on Dependable Computing},
pages = {374--378},
month = {dec},
year = {2005},
isbn = {0-7695-2492-3},
url = {http://doi.ieeecomputersociety.org/10.1109/PRDC.2005.59},
doi = {10.1109/PRDC.2005.59},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
abstract = {Stability is an important system property. In this paper we examine the steps toward fully automated stability verification for a class of discrete-time hybrid systems. These systems are hybrid in the sense that they can have several modes with possibly different discrete-time dynamics. For systems with affine discrete-time dynamics in each mode, we employ a method that is based on Lyapunov theory and reduces the verification task to convex optimization. We detail the steps that are needed for automatic stability verification using this method: 1) choice of a state space partitioning 2) calculation of possible transitions between the different regions of the partitioning and 3) conversion of the problem into linear matrix inequalities, which can be solved through convex optimization. For steps 2) and 3) we present solutions that are suitable for full automation.},
}
A. Dhama, J. Oehlerking, and O. Theel, "Verification of Orbitally Self-Stabilizing Distributed Algorithms using Lyapunov Functions and Poincaré Maps" in Proc. 1st Workshop on Feedback Control Implementation and Design in Computing Systems and Networks (FeBID'06), 2006.
@inproceedings{Dhama2006a,
author = {Abhishek Dhama and Jens Oehlerking and Oliver Theel},
title = {Verification of Orbitally Self-Stabilizing Distributed Algorithms using Lyapunov Functions and Poincaré Maps},
booktitle = {1st Workshop on Feedback Control Implementation and Design in Computing Systems and Networks (FeBID'06)},
year = {2006},
keywords = {Fault Tolerance, Self-Stabilization, Verification, Hybrid Systems, Lyapunov Theory, Poincare Maps},
}
A. Dhama, J. Oehlerking, and O. Theel, "Verification of Orbitally Self-stabilizing Distributed Algorithms using Lyapunov Functions and Poincaré Maps" in Proc. Twelfth International Conference on Parallel and Distributed Systems, 2006.
doi: 10.1109/ICPADS.2006.108
@inproceedings{Dhama2006,
author = {Abhishek Dhama and Jens Oehlerking and Oliver Theel},
title = {Verification of Orbitally Self-stabilizing Distributed Algorithms using Lyapunov Functions and Poincaré Maps},
booktitle = {Twelfth International Conference on Parallel and Distributed Systems},
volume = {1},
publisher = {IEEE Computer Society},
year = {2006},
pages = {23 -- 30},
abstract = {Self-stabilization is a novel method for achieving fault tolerance in distributed applications. A self-stabilizing algorithm will reach a legal set of states, regardless of the starting state or states adopted due to the effects of transient faults, in finite time. However, proving self-stabilization is a difficult task. In this paper, we present a method for showing self-stabilization of a class of non-silent distributed algorithms, namely orbitally self-stabilizing algorithms. An algorithm of this class is modeled as a hybrid feedback control system. We then employ the control theoretic methods of Poincar{\'e} maps and Lyapunov functions to show convergence to an orbit cycle.},
keywords = {Fault Tolerance, Self-Stabilization, Verification, Hybrid Systems, Lyapunov Theory, Poincare Maps},
url = {http://dx.doi.org/10.1109/ICPADS.2006.108},
doi = {10.1109/ICPADS.2006.108},
ISSN = {1521-9097},
}
J. Oehlerking, H. Burchardt, and O. Theel, "Fully Automated Stability Verification for Piecewise Affine Systems" in Proc. Hybrid Systems: Computation and Control, 10th International Workshop, HSCC 2007, 2007.
doi: 10.1007/978-3-540-71493-4_74
@inproceedings{Oehlerking2007,
author = {Jens Oehlerking and Henning Burchardt and Oliver Theel},
title = {Fully Automated Stability Verification for Piecewise Affine Systems},
booktitle = {Hybrid Systems: Computation and Control, 10th International Workshop, {HSCC} 2007},
pages = {741--745},
year = {2007},
url = {http://dx.doi.org/10.1007/978-3-540-71493-4_74},
doi = {10.1007/978-3-540-71493-4_74},
series = {Lecture Notes in Computer Science},
volume = {4416},
publisher = {Springer},
isbn = {978-3-540-71492-7},
abstract = {We provide a framework for fully automated stability verification of piecewise affine systems, both in discrete and continuous time. Starting from the well known linear matrix inequality approach for piecewise quadratic Lyapunov functions, we provide algorithms for the remaining steps needed for full automation. This includes the choice of an adequate state space partitioning into regions and the possible transitions trajectories can take between the regions. To demonstrate the viability of our algorithms, we give examples of systems for which Lyapunov functions can be computed fully automatically.},
}
W. Damm, A. Mikschl, J. Oehlerking, E. Olderog, J. Pang, A. Platzer, M. Segelken, and B. Wirtz, Automating Verification of Cooperation, Control, and Design in Traffic ApplicationsSpringer Berlin Heidelberg.
2007.
doi: 10.1007/978-3-540-75221-9_6
@incollection{DammMOOPPSW2007,
author = {Damm, Werner and Mikschl, Alfred and Oehlerking, Jens and Olderog, Ernst-Rüdiger and Pang, Jun and Platzer, André and Segelken, Marc and Wirtz, Boris},
title = {Automating Verification of Cooperation, Control, and Design in Traffic Applications},
editor = {Jones, CliffB. and Liu, Zhiming and Woodcock, Jim},
booktitle = {Formal Methods and Hybrid Real-Time Systems},
pages = {115-169},
year = {2007},
url = {http://dx.doi.org/10.1007/978-3-540-75221-9_6},
doi = {10.1007/978-3-540-75221-9_6},
series = {Lecture Notes in Computer Science},
volume = {4700},
publisher = {Springer Berlin Heidelberg},
isbn = {978-3-540-75220-2},
language = {English},
abstract = {We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.},
}
J. Oehlerking and O. Theel, "Decompositional Construction of Lyapunov Functions for Hybrid Systems" in Proc. Hybrid Systems: Computation and Control, 12th International Conference, HSCC 2009, 2009.
doi: 10.1007/978-3-642-00602-9_20
@inproceedings{Oehlerking2009a,
author = {Jens Oehlerking and Oliver Theel},
title = {Decompositional Construction of Lyapunov Functions for Hybrid Systems},
editor = {Rupak Majumdar and Paulo Tabuada},
booktitle = {Hybrid Systems: Computation and Control, 12th International Conference, {HSCC} 2009},
year = {2009},
month = {apr},
number = {5469},
pages = {276--290},
url = {http://dx.doi.org/10.1007/978-3-642-00602-9_20},
doi = {10.1007/978-3-642-00602-9_20},
publisher = {Springer},
isbn = {978-3-642-00601-2},
note = {A postprint version is available on this website. The original publication is available at springerlink.com.},
abstract = {In this paper, we present an automatable decompositional method for the computation of Lyapunov functions for hybrid systems with complex discrete state spaces. We use graph-based reasoning to decompose hybrid automata into subgraphs, for which we then solve semidefinite optimization problems to obtain local Lyapunov functions. These local computations are made in a way that ensures that the family of local Lyapunov functions forms a global Lyapunov function, proving asymptotic stability of the system. The main advantages over standard LMI methods are 1) improved numerical stability due to smaller optimization problems, 2) the possibility of incremental construction of stable hybrid automata and 3) easier diagnosis of unstable parts of the automaton in case no Lyapunov function can be found.},
}
J. Oehlerking and O. Theel, "A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems" in Proc. Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, 2009.
doi: 10.1007/978-3-642-04761-9_13
@inproceedings{Oehlerking2009,
author = {Jens Oehlerking and Oliver Theel},
title = {A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems},
editor = {Zhiming Liu and Anders P. Ravn},
booktitle = {Automated Technology for Verification and Analysis, 7th International Symposium, {ATVA} 2009},
month = {oct},
year = {2009},
url = {http://dx.doi.org/10.1007/978-3-642-04761-9_13},
doi = {10.1007/978-3-642-04761-9_13},
series = {Lecture Notes in Computer Science},
volume = {5799},
publisher = {Springer},
isbn = {978-3-642-04760-2},
note = {An updated version is available on this website. The proof sequence on pages 10-11 has been corrected. The original publication is available at springerlink.com.},
abstract = {In this paper, we describe a decompositional approach to convergence proofs for stochastic hybrid systems given as probabilistic hybrid automata. We focus on a concept called "stability in probability," which implies convergence of almost all trajectories of the stochastic hybrid system to a designated equilibrium point. By adapting classical Lyapunov function results to the stochastic hybrid case, we show how automatic stability proofs for such systems can be obtained with the help of numerical tools. To ease the load on the numerical solvers and to permit incremental construction of stable systems, we then propose an automatable Lyapunov-based decompositional framework for stochastic stability proofs. This framework allows conducting sub-proofs separately for different parts of the automaton, such that they still yield a proof for the entire system. Finally, we give an outline on how these decomposition results can be applied to conduct quantitative probabilistic convergence analysis, i.e., determining convergence probabilities below 1.},
}
W. Damm, H. Dierks, J. Oehlerking, and A. Pnueli, Towards Component Based Design of Hybrid Systems: Safety and StabilitySpringer Berlin Heidelberg.
2010.
doi: 10.1007/978-3-642-13754-9_6
@incollection{DammDOP2010,
author = {Damm, Werner and Dierks, Henning and Oehlerking, Jens and Pnueli, Amir},
title = {Towards Component Based Design of Hybrid Systems: Safety and Stability},
editor = {Manna, Zohar and Peled, DoronA},
booktitle = {Time for Verification},
pages = {96-143},
year = {2010},
series = {Lecture Notes in Computer Science},
volume = {6200},
doi = {10.1007/978-3-642-13754-9_6},
url = {http://dx.doi.org/10.1007/978-3-642-13754-9_6},
publisher = {Springer Berlin Heidelberg},
isbn = {978-3-642-13753-2},
language = {English},
abstract = {We propose a library based incremental design methodology for constructing hybrid controllers from a component library of models of hybrid controllers, such that global safety and stability properties are preserved. To this end, we propose hybrid interface specifications of components characterizing plant regions for which safety and stability properties are guaranteed, as well as exception mechanisms allowing safe and stability-preserving transfer of control whenever the plant evolves towards the boundary of controllable dynamics. We then propose a composition operator for constructing hybrid automata from a library of such pre-characterized components supported by compositional and automatable proofs of hybrid interface specifications.},
}
J. Oehlerking, "Decomposition of Stability Proofs for Hybrid Systems" PhD Thesis , 2011.
@phdthesis{Oehlerking2011,
author = {Jens Oehlerking},
title = {{D}ecomposition of {S}tability {P}roofs for {H}ybrid {S}ystems},
school = {Carl von Ossietzky University of Oldenburg, Department of Computer Science, Oldenburg, Germany},
year = {2011},
url = {http://www.uni-oldenburg.de/fileadmin/user_upload/informatik/download/Promotionen/DissertationOehlerking.pdf},
abstract = {The verification of hybrid systems, encompassing both discrete-time and continuoustime behavior, is a problem of rising importance. Hybrid behavior occurs wherever a digital system, operating in discrete time, interacts with a real-world environment, which evolves in continuous time. One desired property of hybrid systems is global asymptotic stability. A globally asymptotically stable system converges toward a pre-defined target state from everywhere in the state space. This property guarantees that the system is robust to temporary external disturbances, correcting their effects on its own accord. Stability proofs are usually conducted with the help of so-called Lyapunov functions, which act as generalized energy functions of the system. A Lyapunov function maps each of the possible system states onto an energy value, such that the energy decreases as the system evolves. The existence of such a function serves as a proof of global asymptotic stability. Furthermore, numerical methods for the computation of such functions exist, allowing for automated stability verification. While these methods work well for smallscale systems, they do, however, not scale up well to systems with large discrete state spaces that appear in many real-world applications. Therefore, it is desirable to conduct these computations in a decompositional manner, solving many small-scale problems instead of one large-scale problem. This thesis bridges this gap by introducing an automatable decomposition methodology that works on hybrid automaton models. A hybrid automaton is viewed as a graph and decomposed into sub-components, for which Lyapunov function computation are conducted individually. The results of these computations are then combined to yield a stability proof for the entire system. These local proofs are not only more lightweight than the larger (and possibly intractable) standard proof, but also allow for the localization of the problem if the computation fails, and the compositional construction of complex stable hybrid automata. The decomposition takes place on two levels: strongly connected components and cycles of the automaton. Our results prove that strongly connected components can be analyzed completely separately. For the cycle-based second level, properties of Lyapunov functions are exploited to combine local proofs into a global proof. Furthermore, the results are extended to the domain of probabilistic hybrid automata, which are a combination of hybrid systems and Markov processes. The decomposition results in this thesis are generalized to this setting, to allow for automatable decompositional stability proofs for probabilistic systems. For both non-probabilistic and probabilistic systems, the decompositional approach is also exploited to yield a set of rules for the structured construction of stable hybrid systems with complex discrete behavior. Furthermore, we derive a general method for the hierarchical component-based design of stabilizing hybrid controllers for a given plant, building on the decomposition results.},
}
O. Jubran and B. Westphal, "Formal approach to guard time optimization for TDMA" in Proc. 21st International Conference on Real-Time Networks and Systems, RTNS 2013, Sophia Antipolis, France, October 17-18, 2013, New York, NY, USA, 2013.
doi: 10.1145/2516821.2516849
@inproceedings{JubranW13,
author = {Oday Jubran and Bernd Westphal},
title = {Formal approach to guard time optimization for {TDMA}},
editor = {Michel Auguin and Robert de Simone and Robert I. Davis and Emmanuel Grolleau},
booktitle = {21st International Conference on Real-Time Networks and Systems, {RTNS} 2013, Sophia Antipolis, France, October 17-18, 2013},
pages = {223--233},
year = {2013},
series = {RTNS '13},
publisher = {{ACM}},
address = {New York, NY, USA},
isbn = {978-1-4503-2058-0},
url = {http://doi.acm.org/10.1145/2516821.2516849},
doi = {10.1145/2516821.2516849},
abstract = {Treating clock drift to avoid message collision and loss is a major challenge when the Time Division Multiple Access (TDMA) protocol is used to schedule communication over a shared medium in networks. We consider clock drift in synchronized networks with tree topology and limited energy, where the root provides the reference clock. We provide a formal approach for analyzing the effect of the slot assignment on the maximal clock drift, given an upper bound on the drift rates of the clocks. We give exact topological characterizations of the slot assignments with largest and least existing clock drift and provide least upper bounds on the clock drift in both cases. We apply our results to derive an optimal, i.e. minimal, safe guard time which effectively avoids message collision or loss due to clock drift.},
}
O. Jubran and B. Westphal, "Optimizing guard time for TDMA in a wireless sensor network - Case study" in Proc. Local Computer Networks Workshops (LCN Workshops), 2014 IEEE 39th Conference on, 2014.
doi: 10.1109/LCNW.2014.6927708
@inproceedings{JubranW2014,
author = {Oday Jubran and Bernd Westphal},
booktitle = {Local Computer Networks Workshops (LCN Workshops), 2014 IEEE 39th Conference on},
title = {Optimizing guard time for TDMA in a wireless sensor network - Case study},
year = {2014},
month = {Sept},
pages = {597-601},
url = {http://dx.doi.org/10.1109/LCNW.2014.6927708},
doi = {10.1109/LCNW.2014.6927708},
publisher = {{IEEE}},
isbn = {978-1-4799-3782-0},
year = {2014},
url = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6974756},
isbn = {978-1-4799-6474-1},
abstract = {When the Time Division Multiple Access (TDMA) protocol is used to schedule communication over a shared medium in wireless sensor networks, clock drift can be tolerated using guard time. A guard time is a short time interval that is added between the TDMA slots. Using guard time requires extra time and energy, which is critical in wireless sensor networks operating on limited energy. In this case study, we apply a formal approach to compute optimal safe guard times, i.e. shortest guard times which avoid message collision and loss due to clock drift in a wireless sensor network. We show the flexibility of the formal approach and its usefulness under several real-world conditions.},
keywords = {Clock Drift, Guard Time, Slot Assignment, TDMA},
}
N. Müllner, O. Theel, and M. Fränzle, "Combining Decomposition and Reduction for State Space Analysis of a Self-Stabilizing System" in Proc. Proceedings of the 2012 IEEE 26th International Conference on Advanced Information Networking and Applications, 2012, p. 8.
@InProceedings{ muellner2012,
author = {Nils M\"ullner and Oliver Theel and Martin Fr\"anzle},
title = {Combining Decomposition and Reduction for State Space Analysis of a Self-Stabilizing System},
booktitle = {Proceedings of the 2012 IEEE 26th International Conference on Advanced Information Networking and Applications},
year = {2012},
series = {AINA'12},
pages = {8},
month = {March},
organization = {IEEE Computer Society},
publisher = {IEEE Computer Society},
note = {Best Paper Award},
abstract = {Verifying fault tolerance properties of a distributed system can be achieved by state space analysis via Markov chains. Yet, the power of such exact analytic methods is very limited as the state space is exponentially proportional to the system size. We propose a method that alleviates this limit. Lumping is a well known reduction technique that can be applied to a Markov chain to prune redundant information. We propose a system decomposition to employ lumping piecewise on the considerably smaller Markov chains of the subsystems which are much more likely to be tractable. Recomposing the lumped Markov chains of the subsystems results in a configuration space that is likely to be considerably smaller. An example demonstrates how the limiting window availability (i.e. a fault tolerance property) can be computed for a system while exploiting the combination of lumping and decomposition.},
}
N. Müllner, O. Theel, and M. Fränzle, "Combining Decomposition and Reduction for State Space Analysis of a Self-stabilizing System" Journal of Computer and System Sciences (JCSS), vol. 79, iss. 7.
2013.
doi: 10.1016/j.jcss.2013.01.022
@Article{ muellner2013, title = {Combining Decomposition and Reduction for State Space Analysis of a Self-stabilizing System},
journal = "Journal of Computer and System Sciences (JCSS)", volume = {79},
number = {7},
pages = {1113--1125},
year = {2013},
issn = "0022-0000", doi = "10.1016/j.jcss.2013.01.022", url = "http://www.sciencedirect.com/science/article/pii/S0022000013000329",
author = "Nils M{\"u}llner and Oliver Theel and Martin Fr{\"a}nzle", keywords = "Fault tolerance, Self stabilization, Probabilistic model checking, Probabilistic bisimilarity, Markov chains, Limiting window availability", abstract = "Fault tolerance measures of distributed systems can be calculated precisely by state space analysis of the Markov chain corresponding to the product of the system components. The power of such an approach is inherently confined by the state space explosion, i.e. the exponential growth of the Markov chain in the size of the underlying system. We propose a decompositional method to alleviate this limitation. Lumping is a well-known reduction technique facilitating computation of the relevant measures on the quotient of the Markov chain under lumping equivalence. In order to avoid computation of lumping equivalences on intractably large Markov chains, we propose a system decomposition supporting local lumping on the considerably smaller Markov chains of the subsystems. Recomposing the lumped Markov chains of the subsystems constructs a lumped transition model of the whole system, thus avoiding the construction of the full product chain. An example demonstrates how the limiting window availability (i.e. a particular fault tolerance measure) can be computed for a self-stabilizing system exploiting lumping and decomposition." }
N. Müllner, O. Theel, and M. Fränzle, "Combining Decomposition and Lumping to Evaluate Semi-hierarchical Systems" in Proc. Proceedings of the 28th IEEE International Conference on Advanced Information Networking and Applications (AINA2014), 2014.
@InProceedings{ muellner2014,
author = {Nils M\"ullner and Oliver Theel and Martin Fr\"anzle},
title = {Combining Decomposition and Lumping to Evaluate Semi-hierarchical Systems},
booktitle = {Proceedings of the 28th IEEE International Conference on Advanced Information Networking and Applications (AINA2014)},
year = {2014},
pages = {1049 -- 1056},
month = {May},
publisher = {IEEE},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/muellner.aina2014.pdf},
abstract = {Determining performance and fault tolerance properties of distributed systems is a challenging task. One common approach to quantify such properties is to construct the state space and the transition model of the distributed system that is to be evaluated. The challenge lies in the state space being exponentially large in the size of the system. One popular approach to tackle this challenge is to combine decomposition and lumping. The system is decomposed, the transition models of the subsystems are constructed and minimized by lumping bisimilar states under an equivalence relation, and the intermediate marginal transition systems are composed to construct the minimal aggregate transition model. The approach allows to circumvent the necessity to construct the full transition model while preserving the ability to compute precise measures. The decomposition yet hinges on the structure of the communication within the system. When processes do not influence each other, decomposition is trivial as it is arbitrary. On the contrary, when all processes are influenced by all other processes ---\, known as heterarchical structure \,--- systems cannot be decomposed at all. Between systems of independent and heterarchical processes are i) hierarchically structured systems and ii) systems that are globally hierarchical, but contain locally heterarchical subsystems. The hierarchical type has been addressed previously. This paper targets the second type ---\, referred to as semi-hierarchically structured \,---, thus expanding the frontier from decomposing purely hierarchically structured systems to decomposing semi-hierarchically structured systems. Furthermore, this paper points out the role of different types of execution semantics regarding the decomposition.},
}
N. Müllner, O. Theel, and M. Fränzle, "Composing Thermostatically Controlled Loads to Determine the Reliability against Blackouts" in Proc. Proceedings of the 10th International Symposium on Frontiers of Information Systems and Network Applications (FINA2014), 2014.
@InProceedings{ muellner2014a,
author = {Nils M\"ullner and Oliver Theel and Martin Fr\"anzle},
title = {Composing Thermostatically Controlled Loads to Determine the Reliability against Blackouts},
booktitle = {Proceedings of the 10th International Symposium on Frontiers of Information Systems and Network Applications (FINA2014)},
year = {2014},
pages = {334 -- 341},
month = {May},
publisher = {IEEE},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/muellner.fina2014.pdf},
abstract = {Power grids are parallel systems in which consumers demand a shared resource independent of each other. A blackout occurs when the total demand increases or decreases too rapidly. This paper combines methods and concepts from three domains. The first stems from estimating the power consumption based on thermostatically controlled loads via Markov chains. The second domain provides the composition of parallel systems enriched by intermediate lumping to construct a minimal aggregate transition model, in this case of a community of housings. The third domain provides reasoning about fault tolerance properties by introducing limiting window reliability as measure, suitable to account for the continuous risk of blackouts. Combined, the three methods and concepts allow to determine the risk of blackout of a community over time.},
}
H. Burchardt, J. Oehlerking, and O. Theel, Developing a Tool for Automatic Stability Verification of Hybrid Systems.
@Misc{BurOehThe06,
author = {Henning Burchardt and Jens Oehlerking and Oliver Theel},
title = {Developing a Tool for Automatic Stability Verification of Hybrid Systems},
howpublished = {Poster Session, 1st Workshop on Feedback Control Implementation and Design in Computing Systems and Networks (FeBID '06)},
year = {2006},
}
H. Burchardt and S. Ratschan, "Estimating the Region of Attraction of Ordinary Differential Equations by Quantified Constraint Solving" in Proc. 3rd WSEAS International Conference on Dynamical Systems and Control (CONTROL'07), 2007.
@INPROCEEDINGS{BurRat07,
author = {Henning Burchardt and Stefan Ratschan},
title = {Estimating the Region of Attraction of Ordinary Differential Equations by Quantified Constraint Solving},
editors = {Ph. Dondon and V. Mladenov and S. Impedovo and C. Cepisca},
booktitle = {3rd WSEAS International Conference on Dynamical Systems and Control ({CONTROL}'07)},
year = {2007},
pages = {241--246},
publisher = {WSEAS Press},
url = {http://www2.cs.cas.cz/~ratschan/papers/region_of_attraction.pdf},
abstract = {We formulate the problem of estimating the region of attraction using quantified constraints and show how the resulting constraints can be solved using existing software packages. We discuss the advantages of the resulting method in detail.},
keywords = {region of attraction, constraint solving},
}
A. Dhama and O. Theel, "A Transformational Approach for Designing Scheduler-Oblivious Self-Stabilizing Algorithms" in Proc. 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2010), 2010.
@INPROCEEDINGS{DhTh:schdtransfor:2010,
author = {Abhishek Dhama and Oliver Theel},
title = {A Transformational Approach for Designing Scheduler-Oblivious Self-Stabilizing Algorithms},
booktitle = {12th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2010)},
year = {2010},
editor = {Shlomi Dolev and Jorge Cobb and Michael Fischer and Moti Yung},
series = {Lecture Notes in Computer Science (LNCS)},
pages = {80-95},
publisher = {Springer-Verlag},
abstract = {The complexity of designing self-stabilizing systems is often compounded by the assumptions about the underlying schedulers. This paper presents a method to transform a self-stabilizing algorithm working under a given arbitrary, but potentially very restrictive, scheduler to a self-stabilizing algorithm under any weakly fair scheduler. The method presented here implements a \emph{progress monitor} by exploiting the knowledge of a ranking function --used for proving convergence under the original scheduler-- to carry out the transformation.},
pdf = {dhama.sss2010.pdf},
}
N. Müllner, A. Dhama, and O. Theel, "Derivation of Fault Tolerance Measures of Self-Stabilizing Algorithms by Simulation" in Proc. ANSS '08: Proceedings of the 41st annual symposium on Simulation, Ottawa, ON, Canada, 2008.
@INPROCEEDINGS{AnSS08:MDT08,
author = {Nils M{\"u}llner and Abhishek Dhama and Oliver Theel},
title = {Derivation of Fault Tolerance Measures of Self-Stabilizing Algorithms by Simulation},
booktitle = {ANSS '08: Proceedings of the 41st annual symposium on Simulation},
year = {2008},
pages = {183 - 192},
address = {Ottawa, ON, Canada},
month = {apr},
publisher = {Institute of Electrical and Electronics Engineers (IEEE) Computer Society Press},
abstract = {Fault tolerance measures can be used to distinguish between different self-stabilizing solutions to the same problem. However, derivation of these measures via analysis suffers from limitations with respect to scalability of and applicability to a wide class of self-stabilizing distributed algorithms. We describe a simulation framework to derive fault tolerance measures for self-stabilizing algorithms which can deal with the complete class of self-stabilizing al- gorithms. We show the advantages of the simulation framework in contrast to the analytical approach not only by means of accuracy of results, range of applicable scenarios and performance, but also for investigation of the influence of schedulers on a meta level and the possibility to simulate large scale systems featuring dynamic fault probabilities.},
location = {Ottawa, ON, Canada},
pdf = {muellner.anss08.pdf},
}
E. Möhlmann and O. E. Theel, "Stabhyli: A Tool for Automatic Stability Verification of Non-Linear Hybrid Systems" in Proc. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'13, 2013.
@inproceedings{conf/hybrid/MohlmannT13,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {Stabhyli: {A} {T}ool for {A}utomatic {S}tability {V}erification of {N}on-{L}inear {H}ybrid {S}ystems},
booktitle = {Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'13},
year = {2013},
pages = {107-112},
url = {http://doi.acm.org/10.1145/2461328.2461347},
crossref = {DBLP:conf/hybrid/2013},
location = {Philadelphia, Pennsylvania, USA},
acmid = {2461347},
keywords = {LMIS, automatic verification, computer-aided design, hybrid systems, lyapunov theory, stability, sums-of-squares},
abstract = {We present Stabhyli, a tool that automatically proves stability of non-linear hybrid systems. Hybrid systems are systems that exhibit discrete as well as continuous behavior. The stability property basically ensures that a system exposed to a faulty environment (e.g. suffering from disturbances) will be able to regain a "good" operation mode as long as errors occur not too frequently. Stabilizing Hybrid systems are omnipresent, for instance in control applications where a discrete controller is controlling a time-continuous process such as a car's movement or a particular chemical reaction. We have implemented a tool to automatically derive a certificate of stability for non-linear hybrid systems. Certificates are obtained by Lyapunov theory combined with decomposition and composition techniques.},
editor = {Calin Belta and Franjo Ivancic},
publisher = {ACM},
isbn = {978-1-4503-1567-8},
}
E. Möhlmann and O. E. Theel, "Towards Automatic Detection of Implicit Equality Constraints in Stability Verification of Hybrid Systems" in Proc. Proceedings of the 1th Congreso Nacional de Ingeniería Informática / Aplicaciones Informáticas y de Sistemas de Información, CoNaIISI 2013, 2013.
@inproceedings{conf/CoNaIISI/MohlmannT13,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {{Towards Automatic Detection of Implicit Equality Constraints in Stability Verification of Hybrid Systems}},
booktitle = {Proceedings of the 1th Congreso Nacional de Ingeniería Inform{\'{a}}tica / Aplicaciones Inform{\'{a}}ticas y de Sistemas de Informaci{\'{o}}n, CoNaIISI 2013},
year = {2013},
url = {http://conaiisi.frc.utn.edu.ar/PDFsParaPublicar/1/schedConfs/1/104-504-1-DR.pdf},
location = {C{\'{o}}rdoba, C{\'{o}}rdoba, Argentina},
keywords = {Hybrid Systems; Automatic Verification; Stability; Lyapunov Theory; Optimization; Sums-of-Squares},
editor = {Marcelo M. Marciszack and Roberto M. Mu{\~{n}}oz and Mario A. Groppo},
publisher = {Red de Carreras de Ingenier{\'{i}}a Inform{\'{a}}tica / Sistemas de Informati{\'{o}}n (RIISIC)},
issn = {2346-9927},
abstract = {We present a powerful heuristic that detects implicit equality constraints that may occur in the specification of systems of constraints in order to find Lyapunov-based certificates of stability for hybrid systems. A hybrid system is a fusion of systems exhibiting discrete-time as well as continuous-time behavior, e.g.\ embedded systems within a physical environment. Stability is a property which ensures that a system starting in any possible state will reach a desired state and remain there. Such systems are particularly useful where a certain autonomous operation is required, e.g.\ keeping a certain temperature or speed of a chemical reaction or steering a vehicle over a predefined track. Stable hybrid systems are extremely valuable because after an error has disturbed their normal operation, they automatically \enquote{steer back} to normal operation. Stability can be certified by finding a so-called Lyapunov function. The search for this kind of function usually involves solving systems of inequality constraints. We have identified and implemented a heuristic that detects implicitly specified equality constraints and tries to resolve them by substitution.},
}
E. Möhlmann and O. E. Theel, "Towards Counterexample-Guided Computation of Validated Stability Certificates for Hybrid Systems" in Proc. Proceedings of the 2nd Congreso Nacional de Ingeniería Informática / Aplicaciones Informáticas y de Sistemas de Información, CoNaIISI 2014, 2014.
@inproceedings{conf/CoNaIISI/MohlmannT14,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {{Towards Counterexample-Guided Computation of Validated Stability Certificates for Hybrid Systems}},
year = {2014},
month = {November},
issn = {2346-9927},
editor = {Marcelo M. Marciszack and Roberto M. Mu{\~{n}}oz and Mario A. Groppo},
booktitle = {Proceedings of the 2nd Congreso Nacional de Ingeniería Inform{\'{a}}tica / Aplicaciones Inform{\'{a}}ticas y de Sistemas de Informaci{\'{o}}n, CoNaIISI 2014},
location = {San Luis, Argentina},
publisher = {Red de Carreras de Ingenier{\'{i}}a Inform{\'{a}}tica / Sistemas de Informati{\'{o}}n (RIISIC)},
volume = {2},
issn = {2346-9927},
url = {http://www.informatik.uni-oldenburg.de/~eikemoe/pubs/CoNaIISI_123.pdf},
abstract = {We propose a method to obtain trustable Lyapunov-based certificates of stability for hybrid systems. A hybrid system is a system exhibiting discrete-time as well as continuous-time behaviors, e.g. embedded systems within a physical environment. Stability is a property which ensures that a system starting in any possible state will reach a desired state and remain there. Such systems are particularly useful when a certain autonomous operation is required, e.g. keeping a certain temperature or speed of a chemical reaction or steering a vehicle over a predefined track. Stable hybrid systems are extremely valuable because if an error disturbs their normal operation, they automatically "steer back" to normal operation. Stability can be certified by finding a so-called Lyapunov function. The search for this kind of functions usually involves solving systems of constraints. The state-of-the-art in Lyapunov-based stability verification is to use numerical methods to solve systems of inequalities, which if solvable indicate stability. We propose to use Satisfiability-Modulo-Theory (SMT) methods to (a) validate the results of a numerical solver and (b) use counterexamples to guide the numerical solver towards a valid solution.},
}
E. Möhlmann, W. Hagemann, and A. Rakow, "Verifying a PI Controller using SoapBox and Stabhyli" in Proc. ARCH@CPSWeek 2016, 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Vienna, Austria, 2016.
@inproceedings{workshop/arch/MohlmannHR16,
author = {Eike M{\"{o}}hlmann and Willem Hagemann and Astrid Rakow},
title = {Verifying a {PI} Controller using SoapBox and Stabhyli},
booktitle = {ARCH@CPSWeek 2016, 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Vienna, Austria},
editor = {Goran Frehse and Matthias Althoff},
series = {EPiC Series in Computing},
volume = {43},
pages = {115-125},
year = {2016},
publisher = {EasyChair},
url = {http://www.easychair.org/publications/paper/Verifying_a_PI_Controller_using_SoapBox_and_Stabhyli},
abstract = {We describe practical experiences on verifying a steering controller specification. The hybrid automaton implements a PI control rule and considers the vehicle's velocity as input from the environment. By combining the tools Stabhyli and SoapBox, we establish several safety and liveness properties for the steering controller, including convergence towards an equilibrium.},
note = {originally submitted and accepted for ARCH14},
issn = {2398-7340}
}
W. Damm, W. Hagemann, E. Möhlmann, and A. Rakow, "Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 95, 2014.
@techreport{report/ATR/DammHMR14,
author = {Werner Damm and Willem Hagemann and Eike M{\"o}hlmann and Astrid Rakow},
title = {Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling},
institution= {SFB/TR 14 AVACS},
month = {February},
year = {2014},
type = {Reports of SFB/TR 14 AVACS},
note = {http://www.avacs.org},
number = {95},
access = {open},
bibtex = {atr095.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski},
series = {ATR},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_095.pdf},
pdf = {avacs_technical_report_095.pdf},
subproject = {H3,H4},
abstract = {In the search of design principles that allow compositional reasoning about safety and stability properties of hybrid controllers we examine a case study on a simplified driver assistance system for lane keeping and velocity control. We thereby target loosely coupled systems: the composed system has to accomplish a task that may depend on several of its subcomponents while little coordination between them is necessary. Our assistance system has to accomplish a comfortable centrifugal force, lane keeping and velocity control. This leads to an architecture composed of a velocity controller and a steering controller, where each controller has its local objectives and together they maintain a global objective. The steering controller makes time bounded promises about its steering, which the velocity controller uses for optimization. For this system, we deductively prove from the components' properties that the objectives of the composed system are accomplished.},
}
W. Damm, E. Möhlmann, and A. Rakow, "Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling" in Proc. Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14, 2014.
doi: 10.1145/2562059.2562120
@inproceedings{conf/hybrid/DammMR14,
author = {Werner Damm and Eike M{\"o}hlmann and Astrid Rakow},
title = {Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling},
editor = {Martin Fr{\"a}nzle and John Lygeros},
booktitle = {Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14},
location = {Berlin, Berlin, Germany},
month = {April},
year = {2014},
pages = {145-150},
numpages = {6},
ee = {http://doi.acm.org/10.1145/2562059.2562120},
crossref = {DBLP:conf/hybrid/2014},
publisher = {ACM},
isbn = {978-1-4503-2732-9},
acmid = {2562120},
url = {http://doi.acm.org/10.1145/2562059.2562120},
doi = {10.1145/2562059.2562120},
keywords = {Hybrid Systems, Automatic Verification, Stability, Safety, Composition, Interfaces, Specifications, Assume-Guarantee, Computer-Aided Design},
abstract = {In the search of design principles that allow compositional reasoning about safety and stability properties of hybrid controllers we examine a case study on a simplified driver assistance system for lane keeping and velocity control. We thereby target loosely coupled systems: the composed system has to accomplish a task that may depend on several of its subcomponents while little coordination between them is necessary. Our assistance system has to accomplish a comfortable centrifugal force, lane keeping and velocity control. This leads to an architecture composed of a velocity controller and a steering controller, where each controller has its local objectives and together they maintain a global objective. The steering controller makes time bounded promises about its steering, which the velocity controller uses for optimization. For this system, we deductively prove from the components' properties that the objectives of the composed system are accomplished.},
}
E. Möhlmann and O. E. Theel, "Breaking Dense Structures: Proving Stability of Densely Structured Hybrid Systems" in Proc. Proceedings of the 4th International Workshop on Engineering Safety and Security Systems, ESSS 2015, Oslo, Norway, June 22, 2015., 2015.
doi: 10.4204/EPTCS.184.4
@inproceedings{conf/corr/MohlmannT15,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {Breaking Dense Structures: Proving Stability of Densely Structured Hybrid Systems},
booktitle = {Proceedings of the 4th International Workshop on Engineering Safety and Security Systems, {ESSS} 2015, Oslo, Norway, June 22, 2015.},
editor = {Pang, Jun and Liu, Yang and Mauw, Sjouke},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {184},
year = {2015},
publisher = {Open Publishing Association},
pages = {49--63},
doi = {10.4204/EPTCS.184.4},
ISSN = {2075-2180},
month = {June},
url = {http://dx.doi.org/10.4204/EPTCS.184.4},
subproject= {H4},
abstract = {Abstraction and refinement is widely used in software development. Such techniques are valuable since they allow to handle even more complex systems. One key point is the ability to decompose a large system into subsystems, analyze those subsystems and deduce properties of the larger system. As cyber-physical systems tend to become more and more complex, such techniques become more appealing. In 2009, Oehlerking and Theel presented a (de-)composition technique for hybrid systems. This technique is graph-based and constructs a Lyapunov function for hybrid systems having a complex discrete state space. The technique consists of (1) decomposing the underlying graph of the hybrid system into subgraphs, (2) computing multiple local Lyapunov functions for the subgraphs, and finally (3) composing the local Lyapunov functions into a piecewise Lyapunov function. A Lyapunov function can serve multiple purposes, e.g., it certifies stability or termination of a system or allows to construct invariant sets, which in turn may be used to certify safety and security. In this paper, we propose an improvement to the decomposing technique, which relaxes the graph structure before applying the decomposition technique. Our relaxation significantly reduces the connectivity of the graph by exploiting super-dense switching. The relaxation makes the decomposition technique more efficient on one hand and on the other allows to decompose a wider range of graph structures.},
}
W. Hagemann, E. Möhlmann, and O. E. Theel, "Hybrid Tools for Hybrid System: Proving Safety and Stability at once (Extended Version)" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 108, 2015.
@techreport{report/ATR/HagemannMT2015b,
author = {Willem Hagemann and Eike M{\"o}hlmann and Oliver E. Theel},
title = {Hybrid Tools for Hybrid System: Proving Safety and Stability at once (Extended Version)},
month = {September},
year = {2015},
institution= {SFB/TR 14 AVACS},
type = {Reports of SFB/TR 14 AVACS},
note = {http://www.avacs.org},
number = {108},
access = {open},
bibtex = {atr108.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski},
series = {ATR},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_108.pdf},
pdf = {avacs_technical_report_108.pdf},
subproject = {H3,H4},
abstract = {Industrial applications usually require safety and stability properties. The safety property guarantees that "something bad" never happens, and the stability property guarantees that "something good" eventually happens. The analyses of both properties are usually performed in isolation. In this work, we consider analyzing both properties by a single automatic approach for hybrid systems. We basically merge analyses of both properties to exploit the knowledge gained from the analysis of each of them in the analysis of the other. We show how both analyses can be divided into multiple steps and interlocked such that both benefit from each other. In fact, we compute single-mode Lyapunov functions, unroll the hybrid system's automaton via repeated reachability queries, and, finally, compute a global Lyapunov function. Each reachability query is simplified by exploiting the knowledge gained from the single-mode Lyapunov functions. The final computation of the global Lyapunov function is simplified by a precise characterization of the reachable states and reuses the single-mode Lyapunov functions. We provide automated tools necessary to link the analyses and report on promising experiments we performed using our new prototype tool.},
}
W. Hagemann and E. Möhlmann, "Inscribing H-Polyhedra in Quadrics using a Projective Generalization of Closed Sets" in Proc. Proceedings of the 27th Canadian Conference on Computational Geometry, CCCG 2015, 2015.
@inproceedings{conf/cccg/HagemannM2015a,
author = {Willem Hagemann and Eike M{\"o}hlmann},
title = {Inscribing H-Polyhedra in Quadrics using a Projective Generalization of Closed Sets},
booktitle = {Proceedings of the 27th Canadian Conference on Computational Geometry, {CCCG} 2015},
location = {Kingston, Ontario, Canada},
month = {August},
year = {2015},
url = {http://research.cs.queensu.ca/cccg2015/CCCG15-papers/07.pdf},
bookurl = {http://research.cs.queensu.ca/cccg2015/CCCG.pdf},
publisher = {Queen's University, Ontario, Canada},
subproject = {H3,H4},
abstract = {We present a projective generalization of closed sets, called complete projective embeddings, which allows us to inscribe H-polyhedra in quadrics efficiently. Essentially, the complete projective embedding of a closed convex set $P \subseteq K^d$ is a double cone in $K^{d+1}$. We show that complete projective embeddings of polyhedral sets are of particular interest and already occurred in the theory of linear fractional programming. Our approach works as follows: By projective principal axis transformation the quadric is converted to a hyperboloid and then approximated by an inner (right) spherical cylinder. Now, given an inscribed H-polytope of the spherical cross section, cylindrification of the polyhedron yields an inscribed H-polyhedron of the spherical cylinder and, hence, of the hyperboloid. After application of the inverse base transformation this approach finally yields an inscribed set of the quadric. The crucial task of this procedure is to find an appropriate generalization of closed sets, which is closed under the involved projective transformations and allows us to recover the non-projective equivalents to the inscribed sets obtained by our approach. It turns out that complete projective embeddings are the requested generalizations.},
}
E. Möhlmann, W. Hagemann, and O. E. Theel, "Hybrid Tools for Hybrid Systems - Proving Stability and Safety at Once" in Proc. Formal Modeling and Analysis of Timed Systems - 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings, 2015.
doi: 10.1007/978-3-319-22975-1_15
@inproceedings{conf/formats/MohlmannHT15,
author = {Eike M{\"{o}}hlmann and Willem Hagemann and Oliver E. Theel},
title = {Hybrid Tools for Hybrid Systems - Proving Stability and Safety at Once},
booktitle = {Formal Modeling and Analysis of Timed Systems - 13th International Conference, {FORMATS} 2015, Madrid, Spain, September 2-4, 2015, Proceedings},
pages = {222--239},
year = {2015},
month = {September},
url = {http://dx.doi.org/10.1007/978-3-319-22975-1_15},
doi = {10.1007/978-3-319-22975-1_15},
series = {Lecture Notes in Computer Science},
volume = {9268},
publisher = {Springer},
isbn = {978-3-319-22974-4},
subproject = {H3,H4},
abstract = {Industrial applications usually require safety and stability properties. The safety property guarantees that "something bad" never happens, and the stability property guarantees that "something good" eventually happens. The analyses of both properties are usually performed in isolation. In this work, we consider analyzing both properties by a single automatic approach for hybrid systems. We basically merge analyses of both properties to exploit the knowledge gained from the analysis of each of them in the analysis of the other. We show how both analyses can be divided into multiple steps and interlocked such that both benefit from each other. In fact, we compute single-mode Lyapunov functions, unroll the hybrid system’s automaton via repeated reachability queries, and, finally, compute a global Lyapunov function. Each reachability query is simplified by exploiting the knowledge gained from the single-mode Lyapunov functions. The final computation of the global Lyapunov function is simplified by a precise characterization of the reachable states and reuses the single-mode Lyapunov functions. We provide automated tools necessary to link the analyses and report on promising experiments we performed using our new prototype tool.},
}
W. Damm, E. Möhlmann, and A. Rakow, "A Design Framework for Concurrent Hybrid System Controllers with Safety and Stability Annotations" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 105, 2016.
@techreport{report/ATR/DammMR2016,
author = {Werner Damm and Eike M{\"o}hlmann and Astrid Rakow},
title = {A Design Framework for Concurrent Hybrid System Controllers with Safety and Stability Annotations},
institution= {SFB/TR 14 AVACS},
year = {2016},
type = {Reports of SFB/TR 14 AVACS},
number = {105},
month = {April},
note = {http://www.avacs.org},
abstract = {We present an assume guarantee framework for hybrid systems which implements design principles tailored for loosely coupled controllers of safety critical applications. To bridge the gap between design and implementation level, the framework takes into account signal latencies and potential loss of coordination messages between controllers on a common plant. Safety as well as stability properties of a controller can be derived compositionally from its subcomponents. Industrial applications usually require safety and stability properties.},
access = {open},
bibtex = {atr105.bib},
pdf = {avacs_technical_report_105.pdf},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_105.pdf},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski},
series = {ATR},
subproject = {H3,H4}
Hybrid systems are control systems that can contain both continuous-time behaviour and discrete state jumps. They therefore represent a combination of classical controllers (continuous-time) and computer-aided controllers (discrete-time) and are therefore particularly relevant in practice. Hybrid models are used, for example, for modelling embedded systems, biological systems or industrial processes. Stability refers to the property that temporally limited disturbances of the system do not permanently influence the behaviour, but are independently compensated by the system. A stable control system is therefore inherently robust against unforeseen disturbances. Stability is a liveness property of a system and is therefore usually difficult to prove. We concentrate on the proof of so-called asymptotic stability. A control system is globally asymptotically stable if it ultimately settles to a rest point for every possible initial state in the absence of disturbances. This resting point can be regarded as the desirable state of the system. The consequence is robustness against temporary disturbances of the system: the system will always return to the vicinity of the resting point when the disturbance effects subside. The proof of such a property can be provided by means of Lyapunov functions. Such a function can be understood as a measure of the energy of the system. If it is ensured that the energy minimum lies at the rest point and that the energy level continuously decreases over time, this can be used to prove global asymptotic stability. The central problem here is that such a function must be found -- this is a non-trivial task. The problem of finding such a Lyapunov function can be transformed into an efficiently solvable optimisation problem whose optimal solution is the parameterisation of such a Lyapunov function. Our goal is to advance these computational methods so that they can be integrated into verification tools. For example, decomposition methods are used that break down a large, possibly not numerically robust optimisation problem into several more robust ones. This makes it possible to analyse more complex systems than would otherwise be possible. Furthermore, we deal with the extension of these methods to systems with probabilistic behaviour and time delays.