When PRISM performs verification of LTL formulas, it does so by converting the formula into a deterministic omega automaton (such as a Rabin automaton) and then analysing a larger product model, constructed from the model being verified and the omega automaton. For this reason, the size of the omega automaton has an important effect on the efficiency of verification.
By default PRISM uses a port of the ltl2dstar library to construct these automata. But it also allows the use of external LTL-to-automata converters producing deterministic automata through support for the Hanoi Omega Automaton (HOA) format. From the command line, an example of this is:
-ltl2datool switch specifies the location of the program to be executed to perform the LTL-to-automaton conversion. This will be called by PRISM as "
exec is the executable,
in-file is the name of a file containing the LTL formula to be converted and
out-file is the name of a file where the resulting automaton should be written, in HOA format. Typically, the executable will be a script. Here is a simple example (called as
hoa-ltl2dstar-for-prism in the above example), which calls an external copy of
ltl2dstar in the required fashion (assuming that the
ltl2ba executables are located in the current directory or on the PATH).
PRISM is known to work with these HOA-enabled tools:
and contains ready-made scripts for calling them in the
etc/scripts/hoa directory of the distribution:
ltl2baas the LTL-to-NBA tool)
ltl2tgbaas the LTL-to-NBA tool
There are also scripts for the upcoming Rabinizer 3.1.
See the files themselves for details of any configuration required and for a reminder of the PRISM command-line arguments required.
-ltl2dasyntax switch is used to specify the textual format for passing the LTL formula to the external converter (i.e., in the file
out-file). The options are:
lbt- LBT format
spin- SPIN format
spot- Spot format
rabinizer- Rabinizer format
From the GUI, configuring the external LTL converter is done with the two options "Use external LTL->DA tool" and "LTL syntax for external LTL->DA tool".
Another related option is "All path formulas via automata" (command-line switch
-pathviaautomata), which forces construction of an automata
when computing the probability of a path formula, even if it is not needed. This is primarily intended for debugging/testing, not regular use.
As mentioned above, PRISM's external LTL-to-automaton interfacing works using the
(and, in particular, using the
jhoafparser HOA parser.
Currently, PRISM can handle automata in HOA format that are
deterministic and complete, with state-based acceptance.
Automata with transition-based acceptance are converted to state-based acceptance by PRISM.
For DTMC and CTMC model checking, generic acceptance conditions are supported, i.e.,
anything that can be specified as an
Acceptance: header in HOA format.
For MDP model checking, currently Rabin and generalized Rabin acceptance
specified via the
acc-name: header are supported. See the HOA format specification for details.