From 993035107cdd516e113515870437dff341ffbd68 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 19 Oct 2010 08:57:55 +0000 Subject: [PATCH] PTA notes. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2171 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES-PTAS.txt | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 prism/NOTES-PTAS.txt diff --git a/prism/NOTES-PTAS.txt b/prism/NOTES-PTAS.txt new file mode 100644 index 00000000..861cb86f --- /dev/null +++ b/prism/NOTES-PTAS.txt @@ -0,0 +1,28 @@ +Brief notes on support for PTAs in PRISM +---------------------------------------- + +* The PRISM Language + +In short, there is a new datatype "clock", which can be used in guards and reset (to zero) just like a normal PRISM variable. The only other addition is an "invariant" keyword, used to specify clock invariants for each PRISM module. + +There are a set of PRISM PTA examples in the directory examples/pta. + +* Properties + +Properties are specified in PCTL, i.e. essentially we allow unbounded or time-bounded reachability properties. See the .pctl files include with the examples for some sample properties. + +* Running PRISM + +Temporarily, PTA support is only available through the command-line version of PRISM. See the formats09.sh script in the examples/pta directory for details of how to run the examples. Currently, there are two different engines for verifying PTAs: (1) "abstraction-refinement", as described in [KNP09c]; and (2) "digital clocks", as described in [KNPS06]. The default is (1). The digital clocks engine can be enabled using the switch "-ptamethod digital". Note, though, that this does not yet support time-bounded reachability properties. + +----------------- + +[KNP09c] +M. Kwiatkowska, G. Norman, and D. Parker. +Stochastic games for verification of probabilistic timed automata. +In Proc. FORMATS’09, volume 5813 of LNCS, pages 212–227. Springer, 2009. + +[KNPS06] +M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston. +Performance analysis of probabilistic timed automata using digital clocks. +Formal Methods in System Design, 29:33–78, 2006.