Symbolic Engine with LTL

[Andrew Wells]

I'm curious how PRISM uses the symbolic engine to verify LTL properties of an MDP. As I understand it, the property is translated to a NBA then a DRA, which is represented explicitly. Is this correct? How does it take the product of a symbolic MDP with an explicitly represented Deterministic Rabin Automata?

Thanks,

Andrew Wells

[Joachim Klein]

Hi Andrew,

Yes, you are right, in the standard approach we translate the LTL
formula into an NBA and then an explicit DRA. If you are interested in
the code, have a look at the automata, jltl2ba and jltl2dstar packages
in the source code (e.g.
https://github.com/prismmodelchecker/prism/tree/master/prism/src/jltl2ba)

For the symbolic approach, we convert the DRA into its symbolic
representation and perform the product construction with the MDP.
Basically, we form the product state space of the MDP and the automaton
and then synchronize the transitions of the automaton (which are
labelled with the atomic propositions of the formula) with the
corresponding states in the MDP that satisfy/don't satisfy the atomic
propositions. For the general construction, you can have a look at the
slides here:
http://www.prismmodelchecker.org/lectures/pmc/18-ltl%20model%20checking.pdf

For the actual code that does the product, see
https://github.com/prismmodelchecker/prism/blob/46d33944d05134879afdfc803a3c2e642bb241aa/prism/src/prism/LTLModelChecker.java#L749
and
https://github.com/prismmodelchecker/prism/blob/46d33944d05134879afdfc803a3c2e642bb241aa/prism/src/prism/LTLModelChecker.java#L951


If you need more help, please feel free to ask.

Cheers,
Joachim Klein