Hi all, A quick (?) question. When I put the following LTL formula into SPOT online: G (G (p => Gp ) => Gp) => (FG p => Gp) SPOT says it is equivalent to 1. Therefore I assume it’s a theorem of LTL. My question: Is there anyway to see the series of rewrites of the formula to show how it gets form the original formula to “true”? Thanks, Scott
Dear Scott, On Sun, Jun 30, 2019 at 11:41 AM Scott M. Staley <smstaley@comcast.net> wrote:
A quick (?) question. When I put the following LTL formula into SPOT online: G (G (p => Gp ) => Gp) => (FG p => Gp) SPOT says it is equivalent to 1. Therefore I assume it’s a theorem of LTL.
From that formula, automata-based tests can establish that "GF!p | F(F!p & G(!p | Gp))" implies "!Gp" (its actually equivalent, but implication is enough), therefore the entire formula is necessarily
If you turn on "expert mode" on the "rewrite" tab of this page, you can play with a few options and discover that the formula is not reduced to 1 unless you tick "reduction based on automata-based containements". Without this option the formula is just rewritten to Gp | GF!p | F(F!p & G(!p | Gp)). true. The list of rules implemented is given in https://spot.lrde.epita.fr/tl.pdf, and this one is the first of the implication-based simplifications (Section 5.4.3)
My question: Is there anyway to see the series of rewrites of the formula to show how it gets form the original formula to “true”?
Not easily. If you compile the source of Spot yourelf, you can to modify the rewriting code to trace its execution for debugging https://gitlab.lrde.epita.fr/spot/spot/blob/ad2f5524/spot/tl/simplify.cc#L22 but that won't really detail each steps as the code sometimes performs multiple rewritings at once. Best regards, Alexandre Duret-Lutz
participants (2)
-
Alexandre Duret-Lutz -
Scott M. Staley