Skip to Main content Skip to Navigation
Conference papers

Probabilistic Regular Graphs

Abstract : Deterministic graph grammars generate regular graphs, that form a structural extension of configuration graphs of pushdown systems. In this paper, we study a probabilistic extension of regular graphs obtained by labelling the terminal arcs of the graph grammars by probabilities. Stochastic properties of these graphs are expressed using PCTL, a probabilistic extension of computation tree logic. We present here an algorithm to perform approximate verification of PCTL formulae. Moreover, we prove that the exact model-checking problem for PCTL on probabilistic regular graphs is undecidable, unless restricting to qualitative properties. Our results generalise those of [EKM06], on probabilistic pushdown automata, using similar methods combined with graph grammars techniques.
Document type :
Conference papers
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : Christophe Morvan Connect in order to contact the contributor
Submitted on : Monday, October 11, 2010 - 5:04:26 PM
Last modification on : Friday, February 4, 2022 - 3:17:43 AM
Long-term archiving on: : Thursday, October 25, 2012 - 4:51:17 PM


Files produced by the author(s)


  • HAL Id : inria-00525388, version 1



Nathalie Bertrand, Christophe Morvan. Probabilistic Regular Graphs. Infinity (International Workshop on Verification of Infinite-State Systems), 2010, Singapour, Singapore. pp.77-90. ⟨inria-00525388⟩



Record views


Files downloads