Package eu.iv4xr.framework.extensions.ltl

Class LTL2Buchi

java.lang.Object
eu.iv4xr.framework.extensions.ltl.LTL2Buchi
public class LTL2Buchi extends Object
For translating an LTL formula to a Buchi automaton. For now, we exclude the following patterns:
  1. The translator does not handle conjunctions "phi ∧ psi";
  2. also does not handle left-recursive until and weak-until. E.g. "(p U q) U r" cannot be handled.
Before translating, the input LTL formula is first normalized using the following rewrites to push negation inside:
  1. "not X phi" to "X not phi"
  2. "not(phi ∧ psi)" to "(not phi) || (not psi)"
  3. "not(phi || psi)" to "(not phi) ∧ (not psi)"
  4. "not(phi U psi) to "(phi ∧ not psi) W (not phi ∧ not psi)"
  5. "not(phi W psi) to "(phi ∧ not psi) U (not phi ∧ not psi)"
After the normalization, a Buchi automaton is constructed recursively. The key recursions are these:
  1. X phi where phi is non-atom LTL formula. Let B is the Buchi of phi, with S1 as the initial state. Create a new initial state S0, and add (S0,true,S1) as a new transition.
  2. p U psi, where p is a state-predicate (atom). Let B is the Buchi of psi. Let S1 be the initial state of B, Create a new initial state S0, with (S0,p,S0) as a transition. For each out-going transitions of S1: (S1,q,T), add a new transition (S0,q,T).
  3. phi U psi, where phi is not a state-predicate: unimplemented.
  4. p W psi, where p is a state-predicate (atom). Let B is the Buchi of psi. Let S1 be the initial state of B, Create a new initial state S0, with (S0,p,S0) as a transition. We also add S0 as an omega-accepting state. For each out-going transition of S1: (S1,q,T), add a new transition (S0,q,T).
  5. phi W psi, where phi is not a state-predicate: unimplemented.
  6. phi || psi. Let B and C be the Buchis of phi and psi, respectively, and S1 and S2 their initial states. We make S1 as the initial state of the combined Buchi. We remove S2, and change every transition that goes from or to S2 to go from/to S1.
  7. phi ∧ psi. Not implemented. TODO.
Author:
Wish

  • Constructor Details

    • LTL2Buchi

      public LTL2Buchi()

  • Method Details

    • arg

      public static <State> LTL<State> arg​(LTL<State> phi)

    • argL

      public static <State> LTL<State> argL​(LTL<State> phi)

    • argR

      public static <State> LTL<State> argR​(LTL<State> phi)

    • isAtom

      public static <State> boolean isAtom​(LTL<State> phi)

    • isNotAtom

      public static <State> boolean isNotAtom​(LTL<State> phi)

    • isNow

      public static <State> Predicate<State> isNow​(LTL<State> phi)
      To recognize and destruct "now p". Returns p.

    • isNotNow

      public static <State> LTL.Now<State> isNotNow​(LTL<State> phi)
      To recognize and destruct "not(now p)". Returns now p.

    • isNotPhi

      public static <State> LTL<State> isNotPhi​(LTL<State> phi)
      To recognize and destruct "not(phi)" pattern, where phi is non-atomic. This returns phi.

    • isNotNext

      public static <State> LTL.Next<State> isNotNext​(LTL<State> psi)
      Recognize "not(next(psi))". Return "next psi".

    • isNotNot

      public static <State> LTL.Not<State> isNotNot​(LTL<State> psi)
      Recognize "not(not(phi))". Return "not phi".

    • isNotAnd

      public static <State> LTL.And<State> isNotAnd​(LTL<State> psi)
      Recognize "not(p ∧ ... ∧ q)" . Returns "p ∧ ... ∧ q".

    • isNotOr

      public static <State> LTL.Or<State> isNotOr​(LTL<State> psi)
      Recognize "not(p || ... || q)" . Returns "p || ... || q".

    • isNotUntil

      public static <State> LTL.Until<State> isNotUntil​(LTL<State> psi)
      Recognize "not(p U q)" . Returns "p U q".

    • isNotWeakUntil

      public static <State> LTL.WeakUntil<State> isNotWeakUntil​(LTL<State> psi)
      Recognize "not(p W q)" . Returns "p W q".

    • pushNegations

      public static <State> LTL<State> pushNegations​(LTL<State> f)
      Normalize an LTL formula by rewriting it, so that negations are recursively pushed as far as possible inside.

    • getBuchi

      public static Buchi getBuchi​(LTL<IExplorableState> phi)
      Translate the given LTL formula to a Buchi automaton.

    • atomName

      static String atomName​(LTL ltl)

    • atomPred

      static <State> Predicate<State> atomPred​(LTL<State> ltl)

    • andRewrite

      public static <State> LTL<State> andRewrite​(LTL<State> f)
      Normalize an LTL formula by rewriting conjunctions. It follows the following rewrite rules:
      • p ∧ q = (\s -> p(s) ∧ q(s))
      • f ∧ (g || h) = (f ∧ g) || (f ∧ h)
      • p ∧ (f U g) = (p ∧ g) || (p ∧ f ∧ X(f U g))
      • p ∧ (f W g) = (p ∧ g) || (p ∧ f ∧ X(f W g))
      • Xf ∧ Xg = X(f ∧ g)
      • (*) Xf ∧ (g U h) = (Xf ∧ h) || (g ∧ X(f ∧ (g U h))
      • (*) Xf ∧ (g W h) = (Xf ∧ h) || (g ∧ X(f ∧ (g W h)))
      • (a U b) ∧ (f U g) = (a ∧ f U (b ∧ (f U g))) || (a ∧ f U (g ∧ (a U b)))
      • (a U b) ∧ (f W g) = (a ∧ f U (b ∧ (f W g))) || (a ∧ f U (g ∧ (a U b))) ... notice that two U in the middle. They are correct.
      • (a W b) ∧ (f W g) = (a ∧ f W (b ∧ (f W g))) || (a ∧ f W (g ∧ (a U b)))
      IMPORTANT: the rewrites in (*) unroll the U/W into a X-formula. This assumes that the input sequence is long enough. For example if the sequence is only one length, the resulting formula is NOT equivalent.
      Parameters:
      f - An LTL formula. It should not contain any negation. Apply pushNegations(LTL) firsrt to normalize an LTL by pushing all negations inside until they all disappear inside atoms.
      Returns:

    • isIrreducibleConj

      public static <State> boolean isIrreducibleConj​(LTL.And<State> phi)
      Check if the cunjunction is irreducible. It is irreducible if it is of the form p ∧ Xphi. Such a form cannot be further rewritten.