Verification of Infinite-State Systems with Probabilistic Behaviour

Parosh Aziz Abdulla1, Asso Raouf Majeed2, & Sallah Hama Amin3

1 Deparment of Information Technology, Uppsala University, Sweden, 2 College of Engineering, University of Sulaimani, 3 College of Science, University of Sulaimani

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

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 alogorithm.

Keywords : Markov chains, quantitative analysis, lossy channel systems

References

1- 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.

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

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

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

5- 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.

6- Iyer P. and Narasimha M. Probabilistic lossy channel systems. Io TAPSOFT'97, 1997,volume l2l4 of Lecture Notes in Computer Science, pages 667-681.

7- 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.

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

9-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.

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

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

View Full Article