Probabilistic regular graphs
Nathalie Bertrand (INRIA Rennes Bretagne Atlantique), Christophe, Morvan (Universit\'e Paris-Est, INRIA Rennes Bretagne Atlantique)

TL;DR
This paper introduces probabilistic regular graphs generated by graph grammars with probabilistic labeling, and presents an algorithm for approximate PCTL verification, highlighting the undecidability of exact model-checking in general.
Contribution
It extends deterministic regular graphs to probabilistic cases and develops an approximate verification algorithm for PCTL properties, generalizing previous work on probabilistic pushdown automata.
Findings
Approximate verification algorithm for PCTL on probabilistic regular graphs.
Exact model-checking for PCTL is undecidable in general.
Results extend previous work on probabilistic pushdown automata.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
