Verification and synthesis for stochastic systems with temporal logic specifications

Stochastic systems;Model checking;Finite-state abstractions;Temporal logic;Interval-valued markov chain

Dutreix, Maxence Dominique Henri ; Coogan, Samuel Electrical and Computer Engineering Zhang, Fumin Zhao, Ye Wardi, Yorai Vamvoudakis, Kyriakos ; Coogan, Samuel

University:Georgia Institute of Technology

Department:Electrical and Computer Engineering

关键词: Stochastic systems;    Model checking;    Finite-state abstractions;    Temporal logic;    Interval-valued markov chain;   

Others  :  https://smartech.gatech.edu/bitstream/1853/62820/1/DUTREIX-DISSERTATION-2020.pdf

美国|英语

来源: SMARTech Repository

【 摘 要 】

The objective of this thesis is to first provide a formal framework for the verification of discrete-time, continuous-space stochastic systems with complex temporal specifications. Secondly, the approach developed for verification is extended to the synthesis of controllers that aim to maximize or minimize the probability of occurrence of temporal behaviors in stochastic systems. As these problems are generally undecidable or intractable to solve, approximation methods are employed in the form of finite-state abstractions arising from a partition of the original system’s domain for which analysis is greatly simplified. The abstractions of choice in this work are Interval-valued Markov Chains (IMC) which, unlike conventional discrete-time Markov Chains, allow for a non-deterministic range of probabilities of transition between states instead of a fixed probability. Techniques for constructing IMC abstractions for two classes of systems are presented. Due to their inherent structure that facilitates estimations of reachable sets, mixed monotone systems with additive disturbances are shown to be efficiently amenable to IMC abstractions. Then, an abstraction procedure for polynomial systems that uses stochastic barrier functions computed via Sum-of-Squares programming is derived. Next, an algorithm for computing satisfaction bounds in IMCs with respect to so-called omega-regular properties is detailed. As probabilistic specifications require finding the set of initial states whose probability of fulfilling some behavior is below or above a certain threshold, this method may yield a set of states whose satisfaction status is undecided. An iterative specification-guided partition refinement method is proposed to reduce conservatism in the abstraction until a precision threshold is met. Finally, similar interval-based finite abstractions are utilized to synthesize control policies for omega-regular objectives in systems with both a finite number of modes and a continuous set of available inputs. A notion of optimality for these policies is introduced and a partition refinement scheme is presented to reach a desired level of optimality.