16 views

Skip to first unread message

Jun 12, 2019, 9:55:46 PM6/12/19

to PRISM model checker developers

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

Jun 14, 2019, 2:23:52 PM6/14/19

to Andrew Wells, PRISM model checker developers

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

> 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.

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)?

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu