Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |


N. Bertrand, P. Fournier. Parameterized verification of many identical probabilistic timed processes. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS'13, LIPIcs, Volume 24, Pages 501-513, IIT Guwahati, India, December 2013.

Download [help]

Download paper: Adobe portable document (pdf) pdf

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic


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 an error 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


Nathalie Bertrand http://www.irisa.fr/prive/nbertran/

BibTex Reference

   Author = {Bertrand, N. and Fournier, P.},
   Title = {Parameterized verification of many identical probabilistic timed processes},
   BookTitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS'13},
   Volume = {24},
   Pages = {501--513},
   Series = {LIPIcs},
   Address = {IIT Guwahati, India},
   Month = {December},
   Year = {2013}

EndNote Reference [help]

Get EndNote Reference (.ref)