Parameterized Verification of Many Identical Probabilistic Timed Processes

Authors Nathalie Bertrand, Paulin Fournier

Thumbnail PDF


  • Filesize: 0.5 MB
  • 13 pages

Document Identifiers

Author Details

Nathalie Bertrand
Paulin Fournier

Cite AsGet BibTex

Nathalie Bertrand and Paulin Fournier. Parameterized Verification of Many Identical Probabilistic Timed Processes. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 501-513, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Parameterized verification aims at validating a system's model irrespective of the value of a parameter. We introduce a model for networks of identical probabilistic timed processes, where the number of processes is a parameter. Each process is a probabilistic single-clock timed automaton and communicates with the others by broadcasting. The number of processes either is constant (static case), or evolves over time through random disappearances and creations (dynamic case). An example of relevant parameterized verification problem for these systems is whether, independently of the number of processes, a configuration where one process is in a target state is reached almost-surely under all scheduling policies. On the one hand, most parameterized verification problems turn out to be undecidable in the static case (even for untimed processes). On the other hand, we prove their decidability in the dynamic case.
  • model checking
  • Markov decision processes
  • parameterized verification


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads