Collaborative Research: A Coalgebraic Framework for Development and Composition of Hybrid Systems

Mislove PavlovicCCR-0208743--0209004该项目侧重于嵌入式混合系统（EHS）的数学基础和设计方法。这种系统的基本特征是，软件组件不仅彼此交互，而且通过传感器和执行器与物理世界交互。因此，计算的离散动力学与物理系统的连续动力学相结合。混合系统试图在一个统一的框架中捕捉这种双重动力。为了限制这两种类型的动力系统的强大复杂性的干扰，连续轨迹通常被封装成状态，在离散计算路径的静态点。连续数学的方法，然后简单地结合离散数学的方法来分析这样的组合system.The出发点计划的研究是一个信念，即蓬勃发展的领域的余代数提供的方法和技术，将允许统一的表示和实现方法的连续和离散的对象和方面。虽然代数方法允许指定和编程有限对象和归纳结构，如表达式或良基树，但共代数方法允许指定和编程无限对象，如共归纳结构：它们一方面包括自动机和各种状态机，另一方面也包括迭代函数系统、解析函数和算子以及真实的数。在真实的意义上，共归纳法渗透于分析，就像归纳法渗透于算术一样。不同之处在于，后者在很久以前就被承认为基本的逻辑原则，而前者只是最近才被承认，尽管它已经隐含地出现了一段时间（例如在大多数解的存在性定理中，尽管它在博弈论中被认为是向后归纳）。现在的任务是明确和系统地使用共归纳和共代数方法，并将其应用于嵌入式混合系统的分析与设计。

Mislove & PavlovicCCR-0208743--0209004This project focuses on mathematical foundations and design methodologies for embedded hybrid systems (EHS). The essential feature of such systems is that software components interact not only with each other, but also with the physical world, through sensors and actuators. The discrete dynamics of computation thus adds up with the continuous dynamics of physical systems. Hybrid systems are an attempt to capture this double dynamism in a unified framework. To limit the interference of the formidable complexities of dynamical systems of both types, the continuous trajectories are usually encapsulated into states, at the static points of the discrete computational paths. The methods of continuous mathematics are then simply combined with the methods of discrete mathematics to analyze such combined systems.The starting point of the planned research is a belief that the burgeoning field of coalgebra provides methods and techniques that will allow uniform representation and implementation methods for continuous and discrete objects and aspects. While algebraic methods allow specifying and programming of finite objects and inductive structures, such as expressions or well-founded trees, coalgebraic methods allow specifying and programming infinite objects, as coinductive structures: they include automata and various state machines on the one hand, as well as iterative function systems, analytic functions and operators, and real numbers on the other hand.In a real sense, coinduction permeates analysis just like inductionpermeates arithmetic. The difference is that the latter has been recognized as a fundamental logical principle a long time ago, whereas the the former has been recognized only recently, although it has appeared implicitly for some time (e.g. in most existence-of-the-solutions theorems, although it has been recognized as backwards induction in game theory).The task is now to make explicit and systematize the use of coinductive and coalgebraic methods, and to apply them in analysis and design of embedded hybrid systems.