Question about time-bounded operators

[Anastasia Mavridou]

Hello, 

We tried to analyze the following PCTL* with PRISM:

P>=1[(G (regular_condition => (P>=0.5[((G[0,5] (! post_condition)) & (F[0,6] post_condition))])))]

However, PRISM returned the error: "Error: Time-bounded operators not supported in LTL”, which appears to stem from the subformula:

P>=0.5[((G[0,5] (! post_condition)) & (F[0,6] post_condition))]

Interestingly, if we remove the conjunction of bounded operators, the error does not occur. For example, the following formula is parsed successfully:

P>=1[(G (regular_condition => (P>=0.5[((F[0,6] post_condition))])))]

Our understanding is that the original formula is valid PCTL*. Thus, it seems like this is a limitation of PRISM(?) Have you encountered this problem before? If so, how do you typically handle such cases?

One approach we tried was unfolding the time-bounded operators—for instance, expressing G[0,n] as a nested sequence of next-state operators. This allowed PRISM to parse the formula successfully:

E.g., G[0,n] =(!$post_condition$ & (X !$post_condition$ & (X !$post_condition$ & … (X $post_condition$)))).

However, we are unsure whether we could use this for non discrete-time semantics.

We would greatly appreciate any insights or alternative solutions you might have.

Best regards,
Anastasia

[Dave Parker]

Hi Anastasia,

No, we don't support time bounds (like [0,5]) on temporal operators
within LTL formulas, I'm afraid. The same applies to PCTL*.

Strictly speaking, you could add these without changing the expressivity
of the logic - because, as you say, you could encode them by unrolling
and using next operators. But, either way, these are quite likely to
blow up the automata generated for the LTL formulas, so we (and the
LTL-to-automaton converters we use) don't support them.

The situation is different for PCTL, where the model checking does not
need any automata and the bounded operators are easy to check.

For your particular example, I think G[0,5]!p & F[0,6]p would just be
equivalent to !p U[6,6] p, which would avoid the need for LTL. But that
won't necessarily be possible for other formulas I guess.

Best wishes,

Dave

> Hello,
>
> We tried to analyze the following PCTL* with PRISM:
>
> P>=1[(G (regular_condition => (P>=0.5[((G[0,5] (! post_condition)) &
> (F[0,6] post_condition))])))]
>

> However, PRISM returned the error: "/Error: Time-bounded operators not
> supported in LTL/”, which appears to stem from the subformula:

>
> P>=0.5[((G[0,5] (! post_condition)) & (F[0,6] post_condition))]
>
> Interestingly, if we remove the conjunction of bounded operators, the
> error does not occur. For example, the following formula is parsed
> successfully:
>
> P>=1[(G (regular_condition => (P>=0.5[((F[0,6] post_condition))])))]
>
> Our understanding is that the original formula is valid PCTL*. Thus, it
> seems like this is a limitation of PRISM(?) Have you encountered this
> problem before? If so, how do you typically handle such cases?
>
> One approach we tried was unfolding the time-bounded operators—for
> instance, expressing G[0,n] as a nested sequence of next-state
> operators. This allowed PRISM to parse the formula successfully:
>
> E.g., G[0,n] =(!$post_condition$ & (X !$post_condition$ & (X !
> $post_condition$ & … (X $post_condition$)))).
>
> However, we are unsure whether we could use this for non discrete-time
> semantics.
>
> We would greatly appreciate any insights or alternative solutions you
> might have.
>
> Best regards,
> Anastasia
>

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion, visit https://groups.google.com/d/msgid/
> prismmodelchecker/5f446686-9577-4e39-
> abe6-3b47547bf8aan%40googlegroups.com <https://groups.google.com/d/
> msgid/prismmodelchecker/5f446686-9577-4e39-
> abe6-3b47547bf8aan%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Anastasia Mavridou]

Thank you, Dave. This is very helpful.

All the best,

Anastasia