4.7 Article

Formal and Efficient Synthesis for Continuous-Time Linear Stochastic Hybrid Processes

期刊

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

资金

  1. EPSRC [EP/M019918/1]
  2. Royal Society [RP120138]
  3. Turing Institute, London, U.K.
  4. Royal Society [RP120138] Funding Source: Royal Society
  5. 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.

作者

我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。

评论

主要评分

4.7
评分不足

次要评分

新颖性
-
重要性
-
科学严谨性
-
评价这篇论文

推荐

暂无数据
暂无数据