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

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

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.