CPS: Breakthrough: A Mathematical Theory of Cyber-Physical Systems

Abstract: Title: CPS: Breakthrough: A Mathematical Theory of Cyber-Physical Systems The fundamental challenge in cyber-physical systems is the confluence of distinct scientific and engineering models, methods, and tools for cyber and physical systems. Cyber systems are primarily about processing information. Physical systems are primarily about structure and dynamics, the evolution of state in time. This project develops a mathematical theory of cyber-physical systems that provides a formal interface between the cyber and the physical. The intellectual merits of the project are a solid basis for the modeling and design as well as the implementation and verification of cyber-physical systems, and a fruitful connection of the nascent discipline of cyber-physical-systems engineering with standard mathematical practice. The project's broader significance and importance are providing a sound foundation by which cyber-physical system technologies can be assessed, and enabling the discipline of cyber-physical-system engineering to evolve into a mature and durable field of study. The project builds on the theory of generalized ultrametric semilattices and the fixed-point theory of strictly contracting functions on generalized ultrametric semilattices to develop a cyber-physical domain theory, providing a firm mathematical footing for arbitrary composition and higher-order behavior, formulating the right notion of convergence and continuity for cyber-physical computation, and developing a notion of approximation and effectiveness that allows for a two-way connection between the abstractions of the theory and the realizations of practice. It further applies the theory to a wide range of classic problems of modeling and simulating mixed discrete and continuous phenomena, and extends it to embrace the discrete interventions of a cyber subsystem on its physical counterpart in a cyber-physical system. It also investigates the practical implications of the theory for the implementation and verification of cyber-physical systems by reexamining currently used timed models of computation through the prism of the theory, exploring the extension of programming languages with temporal constructs that are complete over the theoretical abstractions, and integrating the theory in automated and interactive theorem provers to supplement existing model-checking methods that might succumb to the scale of cyber-physical systems.