Biblio

In this paper we present a method based on linear programming that facilitates reliable safety verification of hybrid dynamical systems over the infinite time horizon subject to perturbation inputs. The verification algorithm applies the probably approximately correct (PAC) learning framework and consequently can be regarded as statistically formal verification in the sense that it provides formal safety guarantees expressed using error probabilities and confidences. The safety of hybrid systems in this framework is verified via the computation of so-called PAC barrier certificates, which can be computed by solving a linear programming problem. Based on scenario approaches, the linear program is constructed by a family of independent and identically distributed state samples. In this way we can conduct verification of hybrid dynamical systems that existing methods are not capable of dealing with. Some preliminary experiments demonstrate the performance of our approach.

Emerging industrial platforms such as the Internet of Things (IoT), Industrial Internet (II) in the US and Industrie 4.0 in Europe have tremendously accelerated the development of new generations of Cyber-Physical Systems (CPS) that integrate humans and human organizations (H-CPS) with physical and computation processes and extend to societal-scale systems such as traffic networks, electric grids, or networks of autonomous systems where control is dynamically shifted between humans and machines. Although such societal-scale CPS can potentially affect many aspect of our lives, significant societal strains have emerged about the new technology trends and their impact on how we live. Emerging tensions extend to regulations, certification, insurance, and other societal constructs that are necessary for the widespread adoption of new technologies. If these systems evolve independently in different parts of the world, they will ‘hard-wire’ the social context in which they are created, making interoperation hard or impossible, decreasing reusability, and narrowing markets for products and services. While impacts of new technology trends on social policies have received attention, the other side of the coin – to make systems adaptable to social policies – is nearly absent from engineering and computer science design practice. This paper focuses on technologies that can be adapted to varying public policies and presents (1) hard problems and technical challenges and (2) some recent research approaches and opportunities. The central goal of this paper is to discuss the challenges and opportunities for constructing H-CPS that can be parameterized by social context. The focus in on three major application domains: connected vehicles, transactive energy systems, and unmanned aerial vehicles.Abbreviations: CPS: Cyber-physical systems; H-CPS: Human-cyber-physical systems; CV: Connected vehicle; II: Industrial Internet; IoT: Internet of Things