Question about LTL POR Provisos

[sjudson]

Reading Partial Order Reduction for PINS and looking at the code for pins2lts-seq.c in particular, I am trying to understand how LTSmin determines whether to use the safety or liveness variant of a given proviso.

I gather that the bit output by a por_proviso() call and added to the transition information by the next_all callback is used to indicate to the POR layer whether the conditions of Definition 36 in that document are met for a specific transition, but cannot seem to find where it is indicated to that POR layer whether to then use a 'there exists' or a 'for all' condition on those bits during state exploration.

Given that the liveness provisos imply the safety provisos, I was wondering whether this is done by just always using the liveness provisos, unless a safety property is provided through the inv_detect interface? Or is there some switch I cannot find where the LTL formula is exposed to the POR interface for safety vs. liveness detection which then dictates which proviso variant is used?

[alaarman]

In the multi-core tool the proviso is decided here: https://github.com/utwente-fmt/ltsmin/blob/87823366b1d58a25ff84534acd36e9fcd98b8438/src/pins2lts-mc/parallel/options.c#L89C10-L89C10

[alaarman]

In the sequential tool there is this switch statement: https://github.com/utwente-fmt/ltsmin/blob/87823366b1d58a25ff84534acd36e9fcd98b8438/src/pins2lts-seq/pins2lts-seq.c#L1575

[sjudson]

@alaarman

Thank you very much for your response. So just to confirm my understanding of how pins2lts-seq works:

-- If the user knows the formula is some safety formula {phi}, they can invoke with the --strategy=bfs or --strategy=dfs and --inv={phi}, in which case the safety proviso will be used.

-- If the user wants to use any other formula, or does not know the safety vs. liveness character of {phi}, they can invoke with --strategy=scc and --ltl {some ltl formula file}, in which case the liveness proviso will be used?

[alaarman]

Ah right. That is correct!

I believe the pins2lts-mc tool also has functionality to analyze LTL properties and refine the proviso if possible (eg when for weak LTL).

[sjudson]

Great, thank you for the clarification.