Symbolic Approaches to Analysis and Hybrid Systems

点击翻译按钮获取中文摘要

Abstract:Hybrid systems consist of discrete time systems interacting withcontinuous time systems. Most frequently they arise when a discretecomputational device functions in a continuous physical environment.Such systems have become very common, thanks to the proliferation ofsoftware in controlling physical systems. Modeling and analysis ofhybrid systems is, therefore, paramount for efficient development ofhigh quality safe devices. Formal models of hybrid systems have been developed by combining discretestate transition formalisms with continuous dynamical systems. Developinganalysis technology for such expressive formalisms is a challenging task.In recent years, several analysis tools have been developed forspecialized classes of hybrid models that either restrict the continuousbehavior or the discrete behavior severely. The continuous component of ahybrid system, in particular, presents a great challenge to thedevelopment of sound analysis techniques. This project aims to develop sound and effective techniques and tools foranalysis of large hybrid system models. The approach centers around theconstruction of approximate abstractions for hybrid systems usingintelligent abstraction mappings that yield effective computability andscalability. The project builds on the hybrid abstraction technique that combinespredicate abstraction for discrete systems with qualitative abstraction ofcontinuous dynamical systems. It focuses on (i) improving techniques to generatethe most appropriate abstraction mappings by structurally analyzing thecontinuous dynamics; (ii) the exploitation of the modular structure of thediscrete and continuous components, and the compositional structure of thehybrid system; and (iii) developing the necessary symbolic methods foreffective automation.The tools and techniques developed under this project will have broader impacts by making analysisamenable to intermediate and large hybrid system models in application areas such as embedded systemdesign for automotive and other applications and bioinformatics. It alsohelps students develop intuitions about complex system behaviors withoutanalytically solving them. The results are disseminated through researchpublications and the tools are made available for academic use.