License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2013.501
URN: urn:nbn:de:0030-drops-43964
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4396/
Go to the corresponding LIPIcs Volume Portal

Bertrand, Nathalie ; Fournier, Paulin

Parameterized Verification of Many Identical Probabilistic Timed Processes

pdf-format:
38.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{bertrand_et_al:LIPIcs:2013:4396,
  author =	{Nathalie Bertrand and Paulin Fournier},
  title =	{{Parameterized Verification of Many Identical Probabilistic Timed Processes}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{501--513},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Anil Seth and Nisheeth K. Vishnoi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4396},
  URN =		{urn:nbn:de:0030-drops-43964},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.501},
  annote =	{Keywords: model checking, Markov decision processes, parameterized verification}
}

Keywords: model checking, Markov decision processes, parameterized verification
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)
Issue Date: 2013
Date of publication: 10.12.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI