You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
28 lines
1.6 KiB
28 lines
1.6 KiB
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.
|