Verification of Infinite-State Systems with Probabilistic Behaviour

Authors

  • Parosh Aziz Abdulla Deparment of Information Technology, Uppsala University, Sweden. Author
  • Asso Raouf Majeed College of Engineering, University of Sulaimani, Kurdistan Region, Iraq. Author
  • Sallah Hama Amin College of Science, University of Sulaimani, Kurdistan Region, Iraq. Author

DOI:

https://doi.org/10.17656/jzs.10151

Keywords:

Markov chains, Quantitative analysis, Lossy channel systems

Abstract

We present a method for performing quantitative analysis of probabilistic systems with infinite state spaces. given an initial state s a set F of final states, and a rational 0>0, compute a rational p such that the probability of reaching F from s is between and p+0. We present an algorithm working in breadth first manner to perform quantitative analysis of infinitive state Markov chains, and provide sufficient conditions for termination of our algorithm.

References

- Abdulla P.A., Cerans K., Jonsson 8., and Yih-Kuen T. Algorithmic analysis of programs with well-quasi ordered domains. Information and Computation, 2000, I 60:109-127. DOI: https://doi.org/10.1006/inco.1999.2843

-Rabinovich A. Quantitative analysis of probabilistic lossy channel systems. ln Proc. ICALP'03,2403.

- Bertrand N and Snoebelen Ph. Model checking lossy channel decidable. In Proc- FOSSACSO 3, 20A3, 2620.

-Abdulla P. A" and Rabinovich A. Verification of Probabilistic communication. In Proc. FOSSACSO3, 2003 2624.

- Baier C. and Engelen B. Establishing qualitative properties for probabilistic lossy channel systems. In Katoen, editor, ARTS'gg, 1999, 1601 af Leeture Notes in Computer Science, pages 34-52. DOI: https://doi.org/10.1007/3-540-48778-6_3

- Iyer P. and Narasimha M. Probabilistic lossy channel systems. Io TAPSOFT'97, 1997,volume l2l4 of Lecture Notes in Computer Science, pages 667-681. DOI: https://doi.org/10.1007/BFb0030633

- Abdulla P. A., Iyer P, and Jonsson B. Reasoning about probabilistic lossy channel systems. In C. Palamidessi, Proc. CONCUR 2000, I l'h Int. Conf,, on Concurrency theary, 1997, 877 of Lecture Notes in Computer Science. DOI: https://doi.org/10.1007/3-540-44618-4_24

- Finkel A. and Snoebelen Ph. Weil-structured transition systems everyrvhere. April 1998, Technical LSV-98-4. Ecole Normale superieure de cachan.

-Abduila P. A., Cerans K, Jonsson B, and Yih-Kuen T. General decidability theorems for infinite-state systems. lgglrirn Proc. LICS'96 I /h IEEE Int. Symp- On Logic in Computer Science, pages 313-321.

- Kemeny J. G., Snit i. L., and Knapp A. W.. Denumerable Markov chains' D van Nostad Co. 1966

l- Karlin S. Afirst Course in Stochastic Processes. Academic Press' 1966.

Published

2006-04-27

How to Cite

Verification of Infinite-State Systems with Probabilistic Behaviour. (2006). Journal of Zankoy Sulaimani - Part A, 9(1), 81-91. https://doi.org/10.17656/jzs.10151