Advertisement

Continuous Time and/or Continuous Distributions

  • Joseph Assouramou
  • Josée Desharnais
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6342)

Abstract

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. 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 use an example of an aircraft to highlight the differences between the two models and we define a generalization of both that can model all the features of our aircraft example.

Keywords

Hybrid System Continuous Time Continuous Distribution Hybrid Process Concurrent System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Journal Theoretical Computer Science 138 (1995)Google Scholar
  2. 2.
    Blute, R., Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. In: Proc. of the Twelfth IEEE Symposium on Logic in Computer Science, Warsaw, Poland (1997)Google Scholar
  3. 3.
    Bouchard-Cote, A., Ferns, N., Panangaden, P., Precup, D.: An approximation algorithm for labelled Markov processes: towards realistic approximation. In: QEST 2005: Proc. of the Second International Conference on the Quantitative Evaluation of Systems, p. 54. IEEE Computer Society, Washington (2005)Google Scholar
  4. 4.
    van Breugel, F., Sharma, B., Worrell, J.: Approximating a Behavioural Pseudometric Without Discount for Probabilistic Systems. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 123–137. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Cattani, S., Segala, R., Kwiatkowska, M., Norman, G.: Stochastic transition systems for continuous state spaces and non-determinism. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 125–139. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    D’Argenio, P.R., Wolovick, N., Terraf, P.S., Celayes, P.: Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization. In: International Conference on Quantitative Evaluation of Systems, pp. 11–20 (2009)Google Scholar
  7. 7.
    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Approximating Continuous Markov Processes. In: Proc. of the 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, Californie, USA, pp. 95–106 (2000)Google Scholar
  8. 8.
    Desharnais, J., Laviolette, F., Zhioua, S.: Testing Probabilistic Equivalence through Reinforcement Learning. In: Proc. of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science, pp. 664–677 (2006)Google Scholar
  9. 9.
    Fränzle, M., Hermanns, H., Teige, T.: Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 172–186. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    Henzinger, T.A., Ho, P.-H., Wong-toi, H.: Algorithmic Analysis of Nonlinear Hybrid Systems. Journal IEEE Trans. on Automatic Control 43, 225–238 (1996)zbMATHGoogle Scholar
  11. 11.
    Hassapis, G., Kotini, I.: Verification of rectangular hybrid automata models. Journal The Journal of Systems and Software 79(10) (2006)Google Scholar
  12. 12.
    Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: An Approach to the Description and Analysis of Hybrid Systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 149–178. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  13. 13.
    Richard, N.: Labelled Markov Processes. Master thesis, Département d’informatique et de génie logiciel, Université Laval (2003)Google Scholar
  14. 14.
    Sproston, J.: Analyzing Subclasses of Probabilistic Hybrid Automata. In: Proc. of the 2nd International Workshop on Probabilistic Methods in Verification, Eindhoven. University of Birmingham, Technical Report, CS-99-8 (1999)Google Scholar
  15. 15.
    Sproston, J.: Model Checking of Probabilistic Timed and Hybrid Systems. Ph.D. thesis, University of Birmingham, Faculty of Science (2000)Google Scholar
  16. 16.
    Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M.: Safety verification for probabilistic hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. LNCS, vol. 6174, pp. 196–211. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Joseph Assouramou
    • 1
  • Josée Desharnais
    • 1
  1. 1.Department of Computer Science and Software EngineeringUniversité LavalQuébecCanada

Personalised recommendations