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