The functions of this module provide translations from temporal logics to symbolically encoded omega automata. In general, these translations replace an elementary subformula (one that starts with a temporal operator) by a new state variable of the automaton and according state transitions and contraints so that the new state variable becomes equivalent to the elementary subformula it abbreviates. To this end, one usually makes use of GFconstraints which however are harder to check than others. They cannot always be avoided, but the translators presented here may try to use Fconstraints whenever possible which then usually generates a cascade of Fconstraints, i.e. formulas of the following form where phi is propositional: CF ::= F phi  F(phi&CF)  X CF  CF & CF. The use of F or CFconstraints is controlled with option tryConstrF of the translators. In addition to the use of GF or Fconstraints, the translators differ also in the acceptance condition they finally produce: LTL2Omega will just have these constraints while LTL2OmegaCTL will rather use a CTL formula (equivalent to an LeftCTL*LTL formula) with potential GFconstraints. In case Fconstraints should be used LTL2OmegaCTL incorporates them to the CTL formula.
Function or value  Description 

compute equivalent DetFautomaton for a cascaded liveness constraint cf; the result is an existential nondeterministic omegaautomaton, i.e., a SpecExpr ExistsAuto(qVars,initCond,transRel,fairConstr,acceptCond).


compute equivalent DetFGautomaton for a cascaded liveness constraint cf; the result is an existential nondeterministic omegaautomaton, i.e., a SpecExpr ExistsAuto(qVars,initCond,transRel,fairConstr,acceptCond).


compute equivalent NDetFautomaton for a cascaded liveness constraint cf; the result is an existential nondeterministic omegaautomaton, i.e., a SpecExpr ExistsAuto(qVars,initCond,transRel,fairConstr,acceptCond).


compute equivalent NDetFGautomaton for a cascaded liveness constraint cf; the result is an existential nondeterministic omegaautomaton, i.e., a SpecExpr ExistsAuto(qVars,initCond,transRel,fairConstr,acceptCond).






This function translates a given LTL formula phi to an omegaautomaton where each elementary subformula of phi is abbreviated by a new state variable of the generated omegaautomaton. If option tryConstrF is true, the translator tries to generate an acceptance condition of cascaded Fconstraints in addition to the GFfairness constraints according to [Schn03]. The following results are then possible (where tryConstrF=true can lead to the cases with cascaded Fconstraints):


Given a LTL formula phi, the following function LTL2OmegaCTL computes an existential omegaautomaton 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 tryConstrF is true, then the function extracts the largest FGformula and translates those subformulas that violate the LeftCTL* syntax rules to state variables and Fconstraints, while otherwise GFconstraints would be used. The result is a pair (topPE,auto) where topPE is the largest toplevel formula of phi that belongs to the LeftCTL* PEfragment, and where auto is an existential nondeterministic omegaautomaton, 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).




PE2NDetFG phiPE computes for a LeftCTL* PEformula an equivalent NDetFG automaton. Note that the FG operators cannot be replaced by an F operator (in contrast to the automata generated from cascaded liveness conditions). A counterexample is [a WU [b SB b]].


