期刊
IEEE TRANSACTIONS ON AUTOMATIC CONTROL
卷 66, 期 1, 页码 17-32出版社
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TAC.2020.2975028
关键词
Formal synthesis; formal verification; probabilistic model checking; stochastic hybrid systems; switched diffusions; temporal logics
资金
- EPSRC [EP/M019918/1]
- Royal Society [RP120138]
- Turing Institute, London, U.K.
- Royal Society [RP120138] Funding Source: Royal Society
- EPSRC [EP/M019918/1] Funding Source: UKRI
Stochastic processes are important for modeling real-world systems, but formal analysis of continuous-time processes is challenging. This article presents a theoretical framework and computational method for switched diffusions to ensure safety.
Stochastic processes are expressive mathematical tools for modeling real-world systems that are subject to uncertainty. It is hence crucial to be able to formally analyze the behavior of these processes, especially in safety-critical applications. Most of the existing formal methods are not designed for continuous-time processes, and those that are typically suffering from state explosion in practice. This article introduces a theoretical framework and a scalable computational method for formal analysis and control synthesis for switched diffusions, a class of stochastic models with linear dynamics that are continuous in both time and space domains; the focus is on safety with possible extensions to other properties. The proposed framework first constructs a finite abstraction in the form of an uncertain Markov process through discretization of both time and space domains. The errors caused by the discretization in each domain are formally characterized and cast into the abstraction model. Then, a strategy that maximizes the probability of the safety property and is robust against the errors is synthesized over the abstraction model. Finally, this robust strategy is mapped to a switching strategy for the stochastic processes that guarantees the safety property. The framework is demonstrated in three case studies, including one that illustrates the tradeoff of the error contribution by the time and space discretization parameters.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据