On the numerical verification of probabilistic rewriting systems

ABSTRACT

We present in this paper a technique for the formal verification of probabilistic systems described in PMAUDE, a probabilistic extension of the rewriting system Maude. Our methodology is based on a numerical verification using the probabilistic symbolic model checking tool PRISM. In particular, we show how we can construct an abstract system from the runs of a model that preserve all the probabilistic properties of the latter. Then we deduce the probabilistic matrix that will be used for the verification in PRISM.

REFERENCES

• 1: G. Agha, J. Meseguer, and K. Sen. PMAUDE: Rewrite-based specification language for probabilistic object systems. In QAPL'05, Edinburgh, Scotland, April 2005.
• 2: Adnan Aziz , Kumud Sanwal , Vigyan Singhal , Robert Brayton, Model-checking continuous-time Markov chains, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.162-170, July 2000 [doi>10.1145/343369.343402]
• 3: Andrea Bianco , Luca de Alfaro, Model Checking of Probabalistic and Nondeterministic Systems, Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science, p.499-513, December 18-20, 1995
• 4: N. Kumar, K. Sen, J. Meseguer, and G. Agha. Probabilistic rewrite theories: Unifying models, logics and tools. Technical Report UIUCDCS-R-2003-2347, Department of computer science, University of Illinois at Urbana-Champaign, 2003.
• 5: Marta Kwiatkowska , Gethin Norman , David Parker, PRISM 2.0: A Tool for Probabilistic Model Checking, Proceedings of the The Quantitative Evaluation of Systems, First International Conference on (QEST'04), p.322-323, September 27-30, 2004 [doi>10.1109/QEST.2004.35]
• 6: Narciso Martí-Oliet , José Meseguer, Rewriting logic: roadmap and bibliography, Theoretical Computer Science, v.285 n.2, p.121-154, 28 August 2002 [doi>10.1016/S0304-3975(01)00357-7]
• 7: José Meseguer, A logical theory of concurrent objects and its realization in the Maude language, Research directions in concurrent object-oriented programming, MIT Press, Cambridge, MA, 1993
• 8: Koushik Sen , Mahesh Viswanathan , Gul Agha, VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems, Proceedings of the Second International Conference on the Quantitative Evaluation of Systems (QEST'05) on The Quantitative Evaluation of Systems, p.251, September 19-22, 2005 [doi>10.1109/QEST.2005.42]