Advertisement

Quantified reduced views of state graphs using Markovian and timed observational equivalence

  • K. Drira
  • Y. Atamna
  • G. Juanole
Chapter
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)

Abstract

This paper defines a new equivalence relation over the states of graphs labeled with probabilities and time feature. The Markovian aggregation technique and the observational transition relation compatibility are used. A computation algorithm is provided using the technique of sequence equivalences of Milner. The reduced quantified view of a state graph is defined as the quotient graph associated with the so-called Markovian-observational equivalence.

Keywords

Observational equivalence Markovian aggregation Probabilistic equivalence relation quotient graph 

References

  1. [Atamna, 1994]
    Atamna, Y. (1994). Réseaux de Petri Temporisés Stochastiques Classiques et Bien Formés: Définition, Analyse et Application aux Systèmes Distribués Temps Réel. PhD thesis, Université Paul Sabatier, Toulouse I II.Google Scholar
  2. [Atamna, 1995]
    Atamna, Y. and Juanole, G. (1995). Methodology for obtaining abstract views of state graphs labeled with probabilities and times. an example of application to a. communication protocol. In MASCOTS, the 3rd International Workshop on Modelling Analysis and Simulation of Computer and Telecommunication Systems IEEE-CS Press, Durham, North Carolina, USA.Google Scholar
  3. [Christoff, 1991]
    Christoff, L. and Christoff, I. (1991). Eficient algorithms for verification of equivalences for probabilistic processes. In Larsen, K. and Skou, A., editors, Proc. 3rd International Workshop CAV’91, number 575 in Lecture Notes in Computer Science. Springer-Verlag.Google Scholar
  4. [Courtois, 1986]
    Courtois, P. J. and Semal, P. (1986). Computable Bounds on conditional steady—state probabilities in large Markov chain and Queueing models. IEEE Journal Selected Areas in Communication, SAC,. 4 (6): 926–937.CrossRefGoogle Scholar
  5. [Drira, 1993]
    Drira, K. and Azéma, P. (1993). Verifying communication protocols via testing-projection. In M. Nivat, C. Rattray, T. R. and Scollo, G., editors, Proceedings of the Third International Conference on Algebraic Methodology and Software Technology, University of Twente, The Netherlands, 21–25 June 1993, Workshops in Computing, pages 255–264, London. Springer-Verlag.Google Scholar
  6. [Hansson, 1990]
    Hansson, H. and Jonsson, B. (1990). A Calculus for Communicating Systems with Time and Probabilities. In Proc. Real-time systems symposium, pages 278–287, Lake Buena Vista, Florida. IEEE Computer Society Press.Google Scholar
  7. [Hennessy, 1985]
    Hennessy, M. and Milner, R. (1985). Algebraic Laws for Nondeterminism and Concurrency. Journal of the Association for Computing Machinery 32(1):137–161.MathSciNetCrossRefzbMATHGoogle Scholar
  8. [Howard, 1971]
    Howard, R. A. (1971). Dynamic Probabilistic Systems, Volume 2: Semi-Markov and Decision Processes. Wiley, J and Sons, INC.Google Scholar
  9. [Juanole, 1991]
    Juanole, G. and Atamna, Y. (1991). Dealing with Arbitrary time Distributions with the Stochastic Timed Petri Net model - Applications to Queueing systems. In Fourth International Workshop on Petri Nets and Performance Models IEEE-CS Press, Melbourne, Australia.Google Scholar
  10. [Kemeny, 1960]
    Kemeny, J. G. and Snell, J. L. (1960). Finite Markov Chains. Nostrand, V and Princeton, N. J.zbMATHGoogle Scholar
  11. [Larsen, 1991]
    Larsen, K. and Skou, A. (1991). Bisimulation through Probalistic Testing. Information and Computation, 94: 1–28.MathSciNetzbMATHGoogle Scholar
  12. [Milner, 1980]
    Milner, R. (1980). A Calculus of Communicating Systems. In Lecture Notes in Computer Science, volume 92. Springer-Verlag, Berl in Heidelberg.Google Scholar
  13. [Park, 1981]
    Park, D. (1981). Concurrency and automata on infinite sequences. In Lecture Notes in Computer Science, volume 104. Springer-Verlag, Berl in Heidelberg.Google Scholar
  14. [Simon, 1984]
    Simon, S. and Shankar, A. (1984). Protocol verification via projection. IEEE Transactions on Software Engineering, 10 (4): 325–342.zbMATHGoogle Scholar
  15. [Van Glabbeek, 1990]
    van Glabbeek, R. (1990). The linear Time-Branching Time Spectrum. In CONCUR ’80, Theories of Concurrency: Unification and Extension, volume 458, Amsterdam, The Netherlands. Lecture Notes in Computer Science, Springer-Verlag.Google Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • K. Drira
    • 1
  • Y. Atamna
    • 2
  • G. Juanole
    • 1
  1. 1.LAAS-CNRS 7, ay. du Colonel RocheToulouse CedexFrance
  2. 2.Dep. of Elec. and Comp. EngWest Virginia UnivMorgantown, WVUSA

Personalised recommendations