Many control systems have large, infinite state space that can not be easily abstracted. One method to analyse and verify these systems is reachability analysis. It is frequently used for air traffic control and power plants. Because of lack of complete information about the environment or unpredicted changes, the stochastic approach is a viable alternative. In this paper, different ways of introducing rechability under uncertainty are presented. A new concept of stochastic bisimulation is introduced and its connection with the reachability analysis is established. The work is mainly motivated by safety critical situations in air traffic control (like collision detection and avoidance) and formal tools are based on stochastic analysis.
The different versions of the original document can be found in:
Published on 01/01/2008
Volume 2008, 2008
DOI: 10.1109/cdc.2005.1582906
Licence: CC BY-NC-SA license
Are you one of the authors of this document?