- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Probabilistic Constraint Nets : a formal framework...
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
Probabilistic Constraint Nets : a formal framework for the modeling and verification of probabilistic hybrid systems St-Aubin, Robert Jr.
Abstract
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 V-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.
Item Metadata
Title |
Probabilistic Constraint Nets : a formal framework for the modeling and verification of probabilistic hybrid systems
|
Creator | |
Publisher |
University of British Columbia
|
Date Issued |
2005
|
Description |
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 V-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.
|
Genre | |
Type | |
Language |
eng
|
Date Available |
2009-12-23
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.
|
DOI |
10.14288/1.0051506
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Graduation Date |
2005-11
|
Campus | |
Scholarly Level |
Graduate
|
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.