| Summary: | Dans ce mémoire, nous comparons deux modèles de processus probabilistes évoluant
dans un environnement continu. Les processus de Markov étiquetés sont des systèmes de
transitions pour lesquels l’ensemble des états est non-dénombrable, mais qui évoluent de
manière discrète dans le temps. Les mesures de probabilité définies sur l’ensemble des
états peuvent avoir un support infini. Les processus hybrides sont une combinaison d’un
processus à espace d’états continu qui évolue de manière continue dans le temps et une
composante discrète qui intervient pour contrôler l’évolution. Les extensions probabilistes
des processus hybrides présentes dans la littérature restreignent le comportement
probabiliste à la composante discrète. Nous utilisons deux exemples de systèmes, un
avion et un bateau, pour faire ressortir les divergences entre les deux modèles ainsi que
leurs limitations, et nous définissons une généralisation qui peut modéliser fidèlement
ces exemples. Nous avons également pu montrer, dans un article publié dans un atelier
international, comment utiliser, dans le contexte probabiliste, la «substitution d’horloge»
et l’«approximation par portrait» qui sont des techniques proposées par Henzinger
et al. pour les processus non probabilistes. Ces techniques permettent, sous certaines
conditions, de définir un processus probabiliste rectangulaire à partir d’un qui est non
rectangulaire, rendant ainsi possible la vérification formelle de toute classe de système
hybride probabiliste. === 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
|
|---|
