Formal Verification and Synthesis for Discrete-Time Stochastic Systems
Transactions on Automatic Control(2015)
摘要
Formal methods are increasingly being used for control and verification of dynamic systems against complex specifications. In general, these methods rely on a relatively simple system model, such as a transition graph, Markov chain, or Markov decision process, and require abstraction of the original continuous-state dynamics. It can be difficult or impossible, however, to find a perfectly equivalent abstraction, particularly when the original system is stochastic. Here we develop an abstraction procedure that maps a discrete-time stochastic system to an Interval-valued Markov Chain (IMC) and a switched discrete-time stochastic system to a Boundedparameter Markov Decision Process (BMDP). We construct model checking algorithms for these models against Probabilistic Computation Tree Logic (PCTL) formulas and a synthesis procedure for BMDPs. Finally, we develop an efficient refinement algorithm that reduces the uncertainty in the abstraction. The technique is illustrated through simulation.
更多查看译文
关键词
Markov processes,Stochastic systems,Model checking,Probability distribution,Switches,Probabilistic logic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络