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.