@TECHREPORT{atr49,
  author = {Arnd Hartmanns},
  title = {A {Modest} Checker for Probabilistic Timed Automata},
  institution = {Sonderforschungsbereiche (SFB)/ Transregio (TR) 14 AVACS},
  year = {2009},
  type = {Reports of SFB/TR 14 AVACS},
  number = {49},
  month = {April},
  note = {ISSN: 1860-9821, http://www.avacs.org.},
  abstract = {The formalism of probabilistic timed automata (PTA) combines discrete
	probabilities, time and nondeterminism. We developed mcpta, a fully
	automatic model-checking tool for PTA specified in Modest, a high-level
	compositional modelling language that includes features such as exception
	handling, dynamic parallelism and recursion. It uses an integral
	semantics for time, representing clocks with bounded integer variables,
	which makes it possible to use established probabilistic model-checking
	tools for the analysis. The use of Modest allows models to be specified
	in a convenient, succinct fashion while support for certain forms
	of dynamic parallelism simplifies modularisation. In order to cope
	with large systems, mcpta optimises the models, leading to significant
	reductions in terms of state-space and model-checking times in the
	case studies we considered. In this report, we investigate the relationship
	between Modest and PTA, show how to correctly transform a large subset
	of Modest including a form of dynamic parallelism for use with the
	probabilistic model-checker PRISM, and present the tool implementation
	and its application to several case-studies, highlighting performance
	improvements due to automatic optimisation as well as elegant modelling
	techniques made possible by exploiting Modest language features.
	},
  access = {open},
  bibtex = {atr049.bib},
  editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger
	Olderog and Andreas Podelski and Reinhard Wilhelm},
  pdf = {avacs_technical_report_049.pdf},
  series = {ATR},
  subproject = {S2}
}