Verification of Infinite-State Systems with Probabilistic Behaviour

Volume 9 , Issue 1 , September 2007 , Pages 81-91

Authors

Parosh Aziz Abdulla 1 ; Asso Raouf Majeed 2 ; Sallah Hama Amin 3

1 Dept. of Information Technology, Uppsala University, Sweden'

2 Dept of Electrical engineering, College of Engineering, Sulaimani University, Kurdistan Region iraq.

3 Dept. of Computer Science, College of Science, Sulaimani University, Kurdistan Region Iraq.

DOI logo 10.17656/jzs.10151

Keywords

Abstract

We present a method for perforrnin g qwantitative onalysis of probabilistic sysierrs with infinite state
spaces: given an initial state srrrr, a ilt F'of final states, and a ritional 0 >0, compute a rational p such that
tr,.prouluullityofreachinge*oms;,xisbetweenandpr$'wepresentanalgorithmworkinginbreadth
firsimanner to perform qfantitative'analysis of infinite state Markov chains, and provide sufficient
conditions for termination of our algorithm'

Statistics
  • Article view421
  • Downloads0
  • Published at1 September 2007

  • RIS
  • BibTeX
  • EndNote
  • Mendeley
  • APA (7th edition)
  • MLA (9th edition)
  • Chicago
  • Harvard
  • IEEE
  • Vancouver