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.
36 lines
3.0 KiB
36 lines
3.0 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 an integer value) just like a normal PRISM variable. The only other addition is an "invariant" keyword, used to specify clock invariants for each PRISM module. The invariant should appear between the variable declarations and the guarded commands.
|
|
|
|
In guards or invariants, references to clocks must be conjunctions of simple clock constraints (i.e. x~c or x~y where x and y are clocks, c is an integer-valued expression and ~ is one of <, <=, >=, >, =). In fact, when using the digital clocks method (see below), this is relaxed and boolean combinations of clock constraints are allowed.
|
|
|
|
There are also some additional restrictions for PTA models. Modules cannot read the local variables of other modules and global variables are not permitted. The model must also have a single initial state (i.e. the init...endinit construct is not permitted). Again, when using digital clocks, the latter constraint does not apply.
|
|
|
|
Model checking requires several assumptions: we require PTAs to be well-formed and non-zeno (see e.g. [KNP09c] for details). Currently, PRISM does not check automatically that these assumptions are satisfied.
|
|
|
|
PRISM does check for timelocks, i.e. states in which it possible to get to a point where no transitions are available and time cannot elapse due to invariant conditions.
|
|
|
|
There are a set of PRISM PTA examples in the directory examples/pta. See the formats09.sh script in this directory for details of how to run the examples.
|
|
|
|
* Properties
|
|
|
|
Properties are specified in PCTL, with no nested P operators, i.e. essentially we allow unbounded or time-bounded reachability properties: properties of the form Pmin=?[F a], Pmax=?[F a], Pmin=?[F<=T a] or Pmax=?[F<=T a], where a is a Boolean-valued expression, not including any clock variables. See the .pctl files included with the examples for some sample properties. For digital clocks, a few less restrictions are in place, e.g. until formulae are allowed, as are clock variables in expressions, as are arithmetic expressions such as 1-Pmin=?[F a].
|
|
|
|
* Running PRISM
|
|
|
|
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. Also, the simulator does not yet support PTAs.
|
|
|
|
-----------------
|
|
|
|
[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.
|