View - Edit - Print - Search

Configuring PRISM /

Automata Generation

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:

The -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 in-file out-file", where 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 ltl2dstar and ltl2ba executables are located in the current directory or on the PATH).

PRISM is known to work with these HOA-enabled tools:

• ltl2dstar
• ltl3dra
• Rabinizer 3

and contains ready-made scripts for calling them in the etc/scripts/hoa directory of the distribution:

• hoa-ltl2dstar-with-ltl2ba-for-prism
  (ltl2dstar using ltl2ba as the LTL-to-NBA tool)
• hoa-ltl2dstar-with-ltl2tgba-for-prism
  (ltl2dstar using Spot's ltl2tgba as the LTL-to-NBA tool
• hoa-ltl2dstar-with-ltl3ba-for-prism
  (ltl2dstar using LTL3BA as the LTL-to-NBA tool
• hoa-ltl3dra-dra-for-prism
  (ltl3dra, generating Rabin automata)
• hoa-ltl3dra-tdgra-for-prism
  (ltl3dra, generating transition-based generalized Rabin automata)
• hoa-rabinizer3-dgra-for-prism
  (Rabinizer 3, generating generalized Rabin automata)
• hoa-rabinizer3-dra-for-prism
  (Rabinizer 3, generating Rabin automata)
• hoa-rabinizer3-tdgra-for-prism
  (Rabinizer 3, generating transition-based generalized Rabin automata)
• hoa-rabinizer3-tdra-for-prism
  (Rabinizer 3, generating transition-based Rabin automata)

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.

The -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 HOA format (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.