From Discrete to Continuous-Time Verification for Probabilistic Hybrid Systems
Abstract
Approved for Public Release.Research Problem and Objectives. The dynamics of a program that interacts with the physical world#a cyberphysicalsystem#is naturally described by a continuous-time process. As CPS become more common and more complex, we needtools to make programming continuous-time systems simpler and more correct.Since CPS often interact with the physical world, errors and bugs can have immediate effects and seriousconsequences. Verification today remains highly challenging, especially for CPS with complex features likeprobabilistic behavior. Researchers in programming languages and verification have developed a wide array oftechniques forproving correctness of programs, but there is currently no way to apply these tools to CPS.Technical Approaches. Our proposal is guided by a key perspective:A continuous-time system is a discrete-time system with infinitesimal time steps.In the 1960s, the logician Abraham Robinson developed non-standard analysis in order to formalize this view. Acornerstone of his theory is the transfer principle: regular definitions and theorems can be directly#transferred# to definitions and theorems about infinitesimal entities. We will put this theory to work, extendingstandard programming languages and verification methods to continuous time.As our primary application, we focus on probabilistic CPS for two reasons. First, these programs have broadapplication: they can model uncertainty and noise in physical environments. Second, there are many verificationmethods for probabilistic programs, but few methods for probabilistic CPS. Accordingly, this application servesas a challenging test case for transferring methods from discrete to continuous time.Ourfirst goal is to develop new languages for continuous-time systems with random sampling, by transferringstandard probabilistic programming languages into non-standard languages with infinitesimal time-steps. The visionis that a programmer will be able to program a probabilistic, continuous-time system with a standard programminglanguage.Our second goal is to adapt standard verification methods to continuous-time. We will consider a variety ofprobabilistic properties, and explore how to translate existing verification methods to handle continuous-timeprograms. The goal is that a programmer will be able to use cutting-edge verification methods for analyzingprobabilistic CPS.Impact on DoD Capabilities. Cyberphysical and hybrid systems play many roles in computational devices used acrossthe Navy, and we expect that such systems will see increasing usage. There is a lack of technology for verifyingcorrect behavior for randomized hybrid systems and for CPS that handle uncertain inputs from the physicalenvironment. The proposed research will yield concrete tools#backed by formal, theoretical guarantees#that canincrease our confidence in the correctness of complex and probabilistic CPS.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jan 12, 2023
- Source ID
- N000142312134
Entities
People
- Justin Hsu
Organizations
- Cornell University
- Office of Naval Research
- United States Navy