Symbolic Approaches to Analysis and Hybrid Systems

Sri International, Menlo Park CA

Investigators

Abstract

Abstract: Hybrid systems consist of discrete time systems interacting with continuous time systems. Most frequently they arise when a discrete computational device functions in a continuous physical environment. Such systems have become very common, thanks to the proliferation of software in controlling physical systems. Modeling and analysis of hybrid systems is, therefore, paramount for efficient development of high quality safe devices. Formal models of hybrid systems have been developed by combining discrete state transition formalisms with continuous dynamical systems. Developing analysis technology for such expressive formalisms is a challenging task. In recent years, several analysis tools have been developed for specialized classes of hybrid models that either restrict the continuous behavior or the discrete behavior severely. The continuous component of a hybrid system, in particular, presents a great challenge to the development of sound analysis techniques. This project aims to develop sound and effective techniques and tools for analysis of large hybrid system models. The approach centers around the construction of approximate abstractions for hybrid systems using intelligent abstraction mappings that yield effective computability and scalability. The project builds on the hybrid abstraction technique that combines predicate abstraction for discrete systems with qualitative abstraction of continuous dynamical systems. It focuses on (i) improving techniques to generate the most appropriate abstraction mappings by structurally analyzing the continuous dynamics; (ii) the exploitation of the modular structure of the discrete and continuous components, and the compositional structure of the hybrid system; and (iii) developing the necessary symbolic methods for effective automation. The tools and techniques developed under this project will have broader impacts by making analysis amenable to intermediate and large hybrid system models in application areas such as embedded system design for automotive and other applications and bioinformatics. It also helps students develop intuitions about complex system behaviors without analytically solving them. The results are disseminated through research publications and the tools are made available for academic use.