Processus de Markov étiquetés et systèmes hybrides probabilistes
|Abstract:||We compare two models of processes involving uncountable space. Labelled Markov processes are probabilistic transition systems that can have uncountably many states, but still make discrete time steps. The probability measures on the state space may have uncountable support and a tool has been developed for verification of such systems. Hybrid processes are a combination of a continuous space process that evolves continuously with time and of a discrete component, such as a controller. Existing extensions of Hybrid processes with probability restrict the probabilistic behavior to the discrete component. We have also shown, in a paper, how to compute for probabilistic hybrid systems, the clock approximation and linear phase-portrait approximation that have been proposed for non probabilistic processes by Henzinger et al. The techniques permit, under some conditions, to define a rectangular probabilistic process from a non rectangular one, hence allowing the model-checking of any class of systems. To highlight the differences between Labelled Markov processes and probabilistic hybrid systems, we use two examples, the ones of a boat and an aircraft, and|
|Document Type:||Mémoire de maîtrise|
|Open Access Date:||18 April 2018|
|Collection:||Thèses et mémoires|
All documents in CorpusUL are protected by Copyright Act of Canada.