PRISM for co-safe LTL

[Andrew Wells]

Hi,

I'm trying to understand the inner workings of PRISM, especially in cases where the specification is given in co-safe LTL. From what I understand, the co-safe LTL formula is converted to a DFA either with an external tool (LBT, Spin, SPOT or Rabinizer) or internally via a powerset construction of the WDBA and then to a DFA by considering the set of states that must reach an accepting state.

This DFA (and all deterministic automata in PRISM) is represented by a list of edges. The automata has apList (I think a list of strings that are state labels) as well as symbols for the transitions. Is there a correspondence between the labels of the automata states (DA.java:53) and the labels in labelDDs (LTLModelChecker.java:271)?

Is my understanding correct so far?

Are there resources for understanding the source code of PRISM?

Thanks,

Andrew Wells

[Joachim Klein]

Hi Andrew,

> I'm trying to understand the inner workings of PRISM, especially in
> cases where the specification is given in co-safe LTL. From what I
> understand, the co-safe LTL formula is converted to a DFA either with an
> external tool (LBT, Spin, SPOT or Rabinizer) or internally via a
> powerset construction of the WDBA and then to a DFA by considering the
> set of states that must reach an accepting state.

There are two cases: (1) for a P=?[...] style path formula with an LTL
path and (2) for a R=?[...] expected accumulated reward formula where
the inner formula is a (syntactically) co-safe LTL formula.

For (1), we construct a deterministic omega-automaton (mostly
deterministic Rabin automata), either via the internal jltl2dstar
implementation or via an external tool, as you mentioned.

For (2), we can't use a general deterministic omega-automaton, but a
essentially a DFA in a special form (this has to do with the fact that
the language is used to exactly determine how long accumulation should
happen). Here, we have an implementation in LTL2WDBA, which does a
transformation from LTL to NBA to a special form of a DBA and then to a
DFA. If you're interested, you can read a bit of detail on that in
http://dx.doi.org/10.1007/s10009-017-0456-3

For syntactically safe co-safe LTL formulas, one can use the method of
(2) also for the case (1), but this is currently still disabled, as we'd
like to do a bit of performance testing beforehand. If you want to play
around a it, you can change the flag at

https://github.com/prismmodelchecker/prism/blob/023d49fc77e483eadd987bacce2e0859aed96f45/prism/src/automata/LTL2DA.java#L131

> This DFA (and all deterministic automata in PRISM) is represented by a
> list of edges. The automata has apList (I think a list of strings that
> are state labels) as well as symbols for the transitions. Is there a
> correspondence between the labels of the automata states (DA.java:53)
> and the labels in labelDDs (LTLModelChecker.java:271)?

Yep, the DAs are encoded as a list of edges, which are labeled with
elements of the powerset of the atomic propositions. The names of the
atomic propositions are stored in apList, each edge is then labled with
a bitset where a true bit at index i corresponds to the atomic
proposition apList[i] being active.

This covers the DA encoding, but to construct the product between the
model and the DA, we also need to know which atomic propositions are
true in each model state (so that we can choose the correct edge in the
DA). That information is stored in the labelDDs list. During the
LTL->automaton construction, maximal state formulas are replaced by
labels of the form L0, L1, ... and labelsDD stores which states
correspond to L0, L1, ...

In general, if you want to understand how the model checking parts work,
it's often easier to have a look at the implementation in the explicit
package, as there all the manipulations are carried out using Java data
structures etc. In the symbolic part of PRISM, the algorithms make use
of the symbolic MTBDD based algorithms which are similar but can be a
bit more opaque at first.

For a bit of background on the underlying algorithms, I've had good
experience with the slides at
http://www.prismmodelchecker.org/lectures/pmc/
and the
http://www.prismmodelchecker.org/bibitem.php?key=KNP07a
http://www.prismmodelchecker.org/bibitem.php?key=FKNP11
tutorial papers.

The "Principles of Model Checking" book by Christel Baier and
Joost-Pieter Katoen might also be useful.

Otherwise, feel free to ask.

Cheers,
Joachim Klein