Modeling And Analysis Of Stochastic Switched Systems

Stochastic switched system incorporates discrete states, continuous dynamics and ran-domness. This kind of system is widely used in a variety of industrial processes such asthe automotive industry, navigation systems, aircraft control systems, air trafc control, fi-nance market model, and many other fields. However, the languages to describe the discreteswitching logic and the stochastic dynamic processes are diferent, and this diference makesthe design and analysis hard.This thesis studies such a kind of stochastic system, in which the continuous dynamicprocesses are described using a set of Ito stochastic diferential equations and the control logicis based on Markov jump. The thesis focuses on the modeling and analysis of the stochasticswitched system. First, this thesis proposes a new Petri net model, namely StochasticDiferential Petri Net. Using the new Petri net, this thesis represents the stochastic switchedsystem based on the E-M discrete format. Then, the PRISM model checker is used tocheck the newly-defined model. In order to model check the Petri net model, this thesisconstructs the corresponding Markov chain to the reachability states of the SDPN, andprove the equivalence of the Markov chain from the reachability graph and that from thestate space partition, based on the equivalence, the SDPN model is model checked by PRISM.A temperature control system has been used to demonstrate the correctness and efectivenessof our method.The contributions of the work are located in the following aspects:Model with randomness. The Petri net language enables us to model the switching logicand stochastic subsystems in a single formalism.Verification of a system with infinite states. For a system whose states involve infiniteor uncountable components, this thesis obtain an equivalent finite state representation onwhich finite state model checking methods can be applied.