Probabilistic constraint nets: A formal framework for the modeling and verification of probabilistic hybrid systems.

摘要

The development of autonomous agents, such as mobile robots or software agents has generated considerable research in recent years. Robotic systems, which are usually built from a mixture of continuous (analog) and discrete (digital) components, are often referred to as hybrid dynamical systems.; The modeling and analysis of hybrid dynamical systems is becoming more and more important as such systems are now widely used to reason about complex physical systems. Ying Zhang and Alan Mackworth developed a semantic model for dynamical systems, called Constraint Nets (CN) [ZM95a]. CN introduces an abstraction and unitary framework to model hybrid systems. Furthermore, specification and verification methods were introduced for deterministic system.; Traditional approaches to real-time hybrid systems usually define behaviors purely in terms of determinism or sometimes non-determinism. The CN framework was developed to model and verify deterministic systems, with the capability to model non-determinism. However, real-time dynamical systems very often behave unpredictably and thus exhibit (structured) uncertainty. It is therefore important to be able to model and analyze real-time probabilistic systems. Hence, a formal framework to model systems with unpredictable behaviors is essential.; We extend the work previously done on Constraint Nets by developing a new framework that we call "Probabilistic Constraint Nets" (PCN). The PCN framework allows for the modeling and simulation of any dynamical system, whether it is deterministic, non-deterministic or probabilistic. We introduce formal syntax and semantics for the framework that ensure the correctness of the models. We also provide a graphical representation that simplifies the task of modeling complex systems. Moreover, we show that our framework is a generalization of many commonly used frameworks such as Markov processes and Markov Decision Processes (MDP). This allows the user to take advantage of a unified framework encompassing most popular modeling paradigms. We have also developed two specification languages (average-time timed ∀-automata and PATTL) along with verification algorithms that allow us specify some behavioural constraints on the system and enables us to proceed to on average and to probabilistic verification of these requirements.; Finally, we also provide, for a subclass of PCN models algorithms for control synthesis. Moreover, we investigate the use of stochastic and robust control for handling the control synthesis task within PCN. With such control synthesis techniques, a designer can automatically construct an optimal controller for his system, hence greatly facilitating his task.