This function replaces positive/negative occurrences of strong operators in weak operators except for the limit operators GF and FG which are even introduced by this function. Hence, except for the limit operators the remaining formulas of ElimStrongInWeak(+,phi) are in TL-FG and those of ElimStrongInWeak(-,phi) are in TL-GF. Starting the function with sign=false will convert the given formula to TL-GF except for the contained limit formulas of the form GF phi and FG phi.

Generate a map that explains the used state variables

LTL2DetOmega translates a given LTL formula phi to an equivalent deterministic omega-automaton by first translating the formula to an equivalent TL-Streett formula and then by translating its TL-FG and TL-GF subformulas to equivalent Det-FG and Det-GF automata, respectively.

This function translates a given LTL formula phi to an omega-automaton where each elementary subformula of phi is abbreviated by a new state variable of the generated omega-automaton. If option tryFG is true, the function prefers the use of FG-constraints instead of GF-constraints (see [Schn03] and VRS slides). The following results are possible:

• no GF constraints, no FG constraints, acpCond = true: This is a safety automaton that only demands the existence of a run through the automaton to accept an input trace. Determinization is possible with the subset construction.
• no GF constraints, some FG constraints, i.e., acpCond = FG(psi): This is a nondeterministic FG-automaton since the conjunction of the FG constraints were combined to a single FG constraint. Determinization is possible with the breakpoint construction.
• some GF constraints, acpCond is either true or FG(psi): This is a nondeterministic generalized Büchi-automaton if the acceptance condition is true, and otherwise a Rabin/Streett automaton.

Given a LTL formula phi, the following function LTL2OmegaCTL computes an existential omega-automaton which is equivalent to phi, and whose acceptance condition is a LeftCTL*-PE formula that has already been translated to CTL. In addition to the LeftCTL* syntax, the function also applies elimination rules to replace CTL^2 nestings of two temporal operators. If argument tryFG is true, then the function extracts the largest FG-formula and translates those subformulas that violate the LeftCTL* syntax rules to state variables and F-constraints, while otherwise GF-constraints would be used. The result is a pair (topPE,auto) where topPE is the largest top-level formula of phi that belongs to the LeftCTL* PE-fragment, and where auto is an existential nondeterministic omega-automaton, i.e., a SpecExpr ExistsAuto(qVars,initCond,transRel,fairConstr,acceptCond) where acceptCond is a CTL formula that is equivalent to an LTL formula (according to [ClDr89] one just may remove all path quantifiers).

Function LTL2Streett converts a given LTL formula phi to an equivalent TL-Streett formula, i.e., a boolean combination of TL-GF and TL-FG formulas that can therefore be translated to equivalent Det-GF and Det-FG automata, respectively. This way, we obtain a simple translation from LTL to deterministic omega-automata, i.e., either Rabin or Streett automata.

Prove the validity of a given LTL formula via emptiness checking of an equivalent omega-automaton. The function returns (isValid,pathOpt) where isValid holds if the LTL formula is valid. In this case, pathOpt is None, and otherwise, it contains a counterexample. The generated counterexample can be drawn with Witness2DotFile or can be printed as html table with PrintCounterExampleAsHtmlTable

This function makes case distinctions on limit formulas, i.e., formulas of the form GF𝜑 or FG𝜑 so that all of these formulas no longer occur under a temporal operator. The function makes use of the following equivalences: φ⟨GFβ⟩+ ⇔ GFβ ∧ φ⟨true⟩+ ∨ φ⟨false⟩+ φ⟨FGβ⟩+ ⇔ FGβ ∧ φ⟨true⟩+ ∨ φ⟨false⟩+ φ⟨GFβ⟩− ⇔ FG¬β ∧ φ⟨false⟩− ∨ φ⟨true⟩− φ⟨FGβ⟩− ⇔ GF¬β ∧ φ⟨false⟩− ∨ φ⟨true⟩−

This function searches in the given formula for a positive occurrence of a subformula eta starting with a strong temporal future operator or a negative occurrence of a subformula eta starting with a weak temporal future operator. It then constructs a context function phi such that the considered formula is phi, i.e., the found occurrences of eta can now be replaced by any other subformula. In this way, the context phi can be instantiated with different subformulas, as required for the normalization procedure of [EsRS24]. The function returns None if there is no positive/negative occurrence of subformula starting with a strong/weak temporal future operator, and Some(sgn,eta,phi) where eta is the subformula found at occurrences of signum sgn such that the context function phi:SpecExpr->SpecExpr can reconstruct the given formula.

This function searches occurrences of signum sgn of the formula eta within the given formula phiLTL which is an occurrence with signum sign. It returns a function phif such that phiLTL = phif(eta).