Symbolic Approaches to Analysis and Hybrid Systems

摘要：混杂系统是由离散时间系统和连续时间系统相互作用而成。最常见的情况是，当离散计算设备在连续的物理环境中运行时，这种系统已经变得非常常见，这要归功于控制物理系统的软件的激增。因此，混合系统的建模和分析对于高效开发高质量的安全设备至关重要。将离散状态转换形式与连续动态系统相结合，建立了混杂系统的形式模型。开发这种表达形式的分析技术是一项具有挑战性的任务，近年来，针对严重限制连续行为或离散行为的混合模型的专业类，已经开发了几种分析工具。尤其是混合系统中的连续成分，对声音分析技术的发展提出了巨大的挑战。该项目旨在开发用于大型混合系统模型分析的可靠和有效的技术和工具。该方法以构建混合系统的近似抽象为中心，使用智能抽象映射产生有效的可计算性和可伸缩性。该项目建立在混合抽象技术的基础上，该技术结合了离散系统的谓词抽象和连续动力系统的定性抽象。它侧重于(I)改进技术，通过对连续动力学的结构化分析来生成最合适的抽象映射；(Ii)开发离散和连续组件的模块化结构，以及混合系统的组成结构；以及(Iii)开发必要的符号方法以实现有效的自动化。在该项目下开发的工具和技术将产生更广泛的影响，使分析适用于应用领域的中型和大型混合系统模型，例如汽车和其他应用程序的嵌入式系统设计和生物信息学。它还帮助学生发展对复杂系统行为的直觉，而不是通过分析来解决这些问题。这些成果通过研究出版物传播，这些工具可供学术使用。

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.