TemporalLogic Module
The functions of this module provide translations from temporal logics to symbolically encoded omega automata, i.e., essentially alternating 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 be avoided in general, but the translators presented here try to use F-constraints or FG-constraints whenever possible so that automata with safety, liveness, co-Büchi and Büchi conditions (see Averest.Core.Specifications.AcceptanceType) are obtained. The main functions are as follows:
- LTL2Omega translates LTL formulas to omega-automata
- LTL2DetOmega translates LTL formulas to deterministic omega-automata
- LTL2OmegaCTL translates LTL formulas to omega-automata with CTL acceptance
- LTL2Streett translates LTL formulas to TL-Streett formulas
Functions and values
Function or value | Description |
|
|
|
|
|
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.
|
|
|
|
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:
|
Full Usage:
LTL2OmegaCTL tryFG phi
Parameters:
bool
phi : SpecExpr
Returns: AutomatonSymb * SpecExpr
|
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
|
|