Title:  Verification and Synthesis for Stochastic Systems with Temporal Logic Specifications

Committee: 

Dr. Coogan, Advisor      

Dr. F. Zhang, Chair

Dr. Zhao

Abstract:

The objective of the proposed research is to design a scalable verification and synthesis tool for discrete-time, continuous-state stochastic systems subject to complex temporal logic specifications. In a stochastic framework, the verification problem amounts to finding the probability that a system exhibits a behavior of interest when initialized to some initial state; the synthesis problem requires designing a control policy that either maximizes or minimizes the probability that some specification is met. Our approach relies on finite-state abstractions of the underlying dynamics in the form of Interval-valued Markov Chains for systems without inputs and Bounded-parameter Markov Decision Processes for controlled systems, and we focus our attention on the expressive class of omega-regular specifications. The first goal of this work is to present classes of systems for which the aforementioned finite-state abstractions can be efficiently constructed given a partition of the continuous domain. Then, a computationally efficient automaton-based algorithm for verifying Interval-valued Markov Chains abstractions against omega-regular specifications has to be implemented, as well as a controller synthesis scheme for Bounded-parameter Markov Decision Processes with a finite or infinite set of inputs. Furthermore, as the optimality of the verification and synthesis algorithms with regard to the abstracted system depend heavily on the quality of the continuous domain partition, we aim to develop a specification-guided partition refinement procedure which targets regions of the state-space most likely to decrease the uncertainty in the abstraction until a precision threshold is reached. Lastly, this method should exploit all information obtained from coarser partitions to reduce computation times when re-performing verification or synthesis in the refined partitions and achieve enhanced scalability.