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.
Chapter PDF
Similar content being viewed by others
Keywords
References
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.
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.
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.
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.
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.
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.
Hennessy, M. and Milner, R. (1985). Algebraic Laws for Nondeterminism and Concurrency. Journal of the Association for Computing Machinery 32(1):137–161.
Howard, R. A. (1971). Dynamic Probabilistic Systems, Volume 2: Semi-Markov and Decision Processes. Wiley, J and Sons, INC.
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.
Kemeny, J. G. and Snell, J. L. (1960). Finite Markov Chains. Nostrand, V and Princeton, N. J.
Larsen, K. and Skou, A. (1991). Bisimulation through Probalistic Testing. Information and Computation, 94: 1–28.
Milner, R. (1980). A Calculus of Communicating Systems. In Lecture Notes in Computer Science, volume 92. Springer-Verlag, Berl in Heidelberg.
Park, D. (1981). Concurrency and automata on infinite sequences. In Lecture Notes in Computer Science, volume 104. Springer-Verlag, Berl in Heidelberg.
Simon, S. and Shankar, A. (1984). Protocol verification via projection. IEEE Transactions on Software Engineering, 10 (4): 325–342.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Drira, K., Atamna, Y., Juanole, G. (1996). Quantified reduced views of state graphs using Markovian and timed observational equivalence. In: Dembiński, P., Średniawa, M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34892-6_16
Download citation
DOI: https://doi.org/10.1007/978-0-387-34892-6_16
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2925-1
Online ISBN: 978-0-387-34892-6
eBook Packages: Springer Book Archive