Abstract
In this paper, we present a sound integration mechanism for Markov processes that are abstractions of stochastic hybrid systems (SHS). In a previous work, we have defined a very general model of SHS and we proved that the realization of an SHS is a Markov process. Moreover, we have developed a verification strategy for the reachability analysis problem. We develop further this line of research by making verification modularly. To achieve this, the state space is decomposed into regions that might share a common border. An abstraction can be constructed on each region and the abstraction method can vary from one region to another. We show how these abstractions can be integrated to provide an abstraction for the entire system. We illustrate this technique for the reachability analysis problem.
Original language | Undefined |
---|---|
Title of host publication | MED '07. Mediterranean Conference on Control & Automation |
Place of Publication | Los Alamitos |
Publisher | IEEE |
Pages | 1-6 |
Number of pages | 6 |
ISBN (Print) | 1-4244-1282-X |
DOIs | |
Publication status | Published - 21 Jan 2008 |
Event | 15th Mediterranean Conference on Control & Automation, MED 2007 - Athens, Greece Duration: 27 Jun 2007 → 29 Jun 2007 Conference number: 15 |
Publication series
Name | |
---|---|
Publisher | IEEE Computer Society Press |
Conference
Conference | 15th Mediterranean Conference on Control & Automation, MED 2007 |
---|---|
Abbreviated title | MED |
Country/Territory | Greece |
City | Athens |
Period | 27/06/07 → 29/06/07 |
Keywords
- EWI-15278
- topological superposition
- stochastic hybrid system
- METIS-263810
- IR-65456
- Markov Processes
- reachability analysis