Formal Verification and Synthesis for Discrete-Time Stochastic Systems

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 Bounded-parameter 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.