TemporalLogic Module
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 GF-constraints which however are harder to check than others. They cannot always be avoided, but the translators presented here may try to use F-constraints whenever possible which then usually generates a cascade of F-constraints, 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 CF-constraints is controlled with option tryConstrF of the translators. In addition to the use of GF or F-constraints, 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 GF-constraints. In case F-constraints should be used LTL2OmegaCTL incorporates them to the CTL formula.
Functions and values
| Function or value | Description |
|
compute equivalent DetF-automaton for a cascaded liveness constraint cf; the result is an existential nondeterministic omega-automaton, i.e., a SpecExpr ExistsAuto(qVars,initCond,transRel,fairConstr,acceptCond).
|
|
compute equivalent DetFG-automaton for a cascaded liveness constraint cf; the result is an existential nondeterministic omega-automaton, i.e., a SpecExpr ExistsAuto(qVars,initCond,transRel,fairConstr,acceptCond).
|
|
compute equivalent NDetF-automaton for a cascaded liveness constraint cf; the result is an existential nondeterministic omega-automaton, i.e., a SpecExpr ExistsAuto(qVars,initCond,transRel,fairConstr,acceptCond).
|
|
compute equivalent NDetFG-automaton for a cascaded liveness constraint cf; the result is an existential nondeterministic omega-automaton, i.e., a SpecExpr ExistsAuto(qVars,initCond,transRel,fairConstr,acceptCond).
|
|
|
|
|
|
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 tryConstrF is true, the translator tries to generate an acceptance condition of cascaded F-constraints in addition to the GF-fairness constraints according to [Schn03]. The following results are then possible (where tryConstrF=true can lead to the cases with cascaded F-constraints):
|
|
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 tryConstrF 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).
|
|
|
|
PE2NDetFG phiPE computes for a LeftCTL* PE-formula 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]].
|
|
|