Hybrid systems

We have developed a number of algorithms to efficiently analyze hybrid systems. In particular, we have worked on the following projects: 

• SpaceEx bug finder. We have developed a version of SpaceEx adjusted towards solving falsification problems, i.e., our primary goal is to find a path to the bad states as fast as possible. To this end, we have introduced two heuristics which prioritize symbolic successors during the exploration of the state space of a considered hybrid system: box-based heuristicand PDB heuristic. 
• Compositional reasoning in SpaceEx. We have investigated the application of compositional methods to hybrid systems. We have implemented a version of SpaceEx incorporating assume-guarantee abstraction refinement schema (AGAR).
• Benchmark suite. We provide a parameterized benchmark generator for stratified controllers of tank networks.
• SpaceEx-Simulink translation. We have developed a source-to-source translation from SpaceEx models to Simulink. 
• Support-function based refinement framework for hybrid systems. We have developed a version of SpaceEx which automatically refines the region representation based on transition guards and bad states. In this way, we can leverage precision and performance. 
• Functional Mock-Up Interface support in SpaceEx. We have integrated FMI into SpaceEx and Uppaal to support co-simulation of hybrid and timed systems. 
• Parameter identification for hybrid systems. We have proposed an abstraction based framework to identify parameters of multi-affine dynamic systems for a given safety property.