Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
Spot
Spot
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 117
    • Issues 117
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 1
    • Merge Requests 1
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Spot
  • SpotSpot
  • Issues
  • #11

Closed
Open
Opened Dec 19, 2014 by Alexandre Duret-Lutz@adlOwner

more LTL simplifications for GF formulas

(GF(a)&GF(b)) | (GF(c)&GF(d)) is equivalent to (GF(a|c) & GF(a|d) & GF(b|c) & GF (b|d)).

It's a bigger formula, but it can be translated into a one-state automaton.

Jan Strejcek:

ADL: we like to simplify GFa | GFb as GF(a|b) because GF(a|b) is easily translated as a deterministic automaton. In the same way, (GFa & GFb) | (GFc & GFd), which is currently translated as a non-deterministic automaton, could be rewritten as GF(a|c) & GF(a|d) & GF(b|c) & GF(b|d) which will be translated as a deterministic automaton. Can this kind of rewriting be generalized?

I think I can provide a (partial) answer. The only non-obvious rule we have to add is the following:

for pure eventually formulae m1,m2 (roughly speaking, the formulae starting with F), the following equivalence holds: G m1 | G m2 <=> G (m1|m2)

With this rule and the standard rules

G f1 & G f2 <=> G (f1&f2)
distributivity: (A&B) | (C&D) <=> (A|C) & (A|D) & (B|C) & (B|D)
                or simply A | (C&D) <=> (A|C) & (A|D) applied twice
F f1 | F f2 <=> F (f1|f2)

one can transform (GFa & GFb) | (GFc & GFd) into G( F(a|c) & F(a|d) & F(b|c) & F(b|d)), which is enough to get determinstic automaton. A more interesting question may be "How to detect the situation when such rules should be applied". This especially applies to the distributivity as all other rules simply replace two modalities with one, which has usually positive effect on the translation and therefore the rules should be applied by default. I can imagine that distributivity will be applied only with --deter option and only to propagate disjunction downwards the syntactic tree (as disjunction is often a source of nondeterminism).

Jan:

ADL: It isn't as straightforward as it seems. For instance adding only the G(e1)|G(e2) = G(e1|e2) without distribution can be a serious regression:

G(Fa & Fb) | G(Fc & Fd): 3 states G((Fa & Fb) | (Fc & Fd)): 15 states G(F(a | c) & F(a | d) & F(b | c) & F(b | d)): 1 state

I think for this to work we have to guarantee that all pure eventualities will be rewritten as F(something).

I guess that you want to say that each pure eventuality formula can be rewritten into a conjunction of F(something) formulae. I'm afraid this doesn't hold. For example, GFa R Fb is a pure eventuality formula equivalent to GFa | GFb... Hmm, but there is no problem in this particular case. I have to think about it with a fresh mind.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: spot/spot#11