How does logic.past work?

thisiscam commented 4 years ago

Hi, I was studying about past LTL operators, and ran into this repo. Could someone explain how the translate routine omega.logic.past works? Specifically, I wonder what is the returned tuple value and what does "initial condition" mean?

johnyf commented 4 years ago

About past LTL, please refer to the literature cited in the docstring of the module omega.logic.past:

https://github.com/tulip-control/omega/blob/v0.3.1/omega/logic/past.py#L4-L27

A usage example of this module is the function openpromela.logic.map_to_future:

https://github.com/johnyf/openpromela/blob/8a74b37b2b481cb9b1914fd9b2b4b38bb8162a73/openpromela/logic.py#L2272 (requires a previous version of omega https://github.com/tulip-control/omega/blob/v0.0.7/omega/logic/past.py)

of the package openpromela, which is described in a paper and a technical report.

The function omega.logic.past.translate

https://github.com/tulip-control/omega/blob/v0.3.1/omega/logic/past.py#L245

takes a formula that may contain past LTL operators and returns a translated formula with operators of future LTL, together with additional variables that work as memory for representing the past LTL operators, and formulas about these additional variables. These additional variables and formulas are called temporal testers.

The past operators are listed in the documentation

https://github.com/tulip-control/omega/blob/v0.3.1/doc/doc.md#temporal-logic-syntax

'-X' expr # weak previous
'--X' expr # strong previous
'-[]' expr # historically (dual of [])
'-<>' expr # once (dual of <>)
expr 'S' expr # since

For example, assuming that u is a variable, translating the operator "weak previous":

>>> from omega.logic import past

>>> past.translate('-X u')

({'u_prev1': {'type': 'bool', 'dom': None, 'owner': 'sys'}},
 'u_prev1',
 'u_prev1',
 '((X u_prev1) <=> u)',
 [])

The function omega.logic.past.translate returns a tuple with 5 items:

dvars, r, init, trans, win

dvars: dictionary of variable declarations. These are the additional memory variables added to represent the past LTL operators. In the example, u_prev1 is the additional variable, and is Boolean-valued.
r: translated formula in future LTL. In the example, -X u has been translated to u_prev1.
init: the initial condition applicable to the additional variable. Weak previous is TRUE at the initial state, so the initial condition is u_prev1. This initial condition together with the transition formula and the liveness formula describe the temporal tester.
trans: transition formula applicable to the additional variable. In the example, ((X u_prev1) <=> u). The operator X means "next" and can also be written using a prime u_prev1' <=> u. This formula requires that the next value of the memory variable u_prev1 be equal to the current value of the variable u. In other words, the variable u_prev1 remembers the previous value of variable u, and thus implements the operator "weak previous".

This formula is understood to be placed within the operator []. So what trans means is []((X u_prev1) <=> u). The operator "always" has been omitted because the returned formulas are intended to be stored in an automaton instance, in the attributes aut.init, aut.action, and aut.win. The automaton represents a formula with initial condition, []action formulas, and []<>win formulas for each item in win.

The automaton class is omega.symbolic.temporal.Automaton:

https://github.com/tulip-control/omega/blob/v0.3.1/omega/symbolic/temporal.py#L36
win: recurrence formula, to be placed within []<>. The example of translating the operator "until" (below) includes a liveness formula (see also d7e8d1e7f833e0f0bfdf84d2109288995cadaac1).

Translating the operator "strong previous":

>>> past.translate('--X u')

({'u_prev1': {'type': 'bool', 'dom': None, 'owner': 'sys'}},
 'u_prev1',
 '(~ u_prev1)',
 '((X u_prev1) <=> u)',
 [])

Compared to the operator "weak previous", the operator "strong previous" is represented by a variable with initial value FALSE, as described by (~ u_prev1). The reason is that:

The operator "strong previous" (--X) is TRUE if there exists a previous state and the argument is TRUE in the previous state.
The operator "weak previous" (-X) is TRUE if there does not exist a previous state or there exists a previous state and the argument is TRUE in the previous state.

Translating the operator "historically":

>>> past.translate('-[] u')

({'_aux0': {'type': 'bool', 'dom': None, 'owner': 'sys'}},
 '(~ _aux0)',
 '(_aux0 <=> ( ~ u ))',
 '((X _aux0) <=> (    (X ( ~ u )) \\/ ((X True) /\\ _aux0)))',
 [])

The translation of the formula -[] u is ~ _aux0. The auxiliary variable _aux0 starts equal to ~ u (negated u) and becomes TRUE if ~ u becomes TRUE. After becoming TRUE, variable _aux0 remains TRUE. So variable _aux0 remembers whether u has become FALSE, and ~ _aux0 is TRUE if u has been uninterruptedly TRUE in the past.

Translating the operator "once":

>>> past.translate('-<> u')

({'_aux0': {'type': 'bool', 'dom': None, 'owner': 'sys'}},
 '_aux0',
 '(_aux0 <=> u)',
 '((X _aux0) <=> (    (X u) \\/ ((X True) /\\ _aux0)))',
 [])

The translation of the formula -<> u is _aux0. The auxiliary variable _aux0 starts equal to u and becomes TRUE if u becomes TRUE. After becoming TRUE, variable _aux0 remains TRUE. So variable _aux0 remembers whether u has become TRUE, and _aux0 is TRUE if u has been TRUE at least once in the past.

Translating the operator "since":

>>> past.translate('a S b')

({'_aux0': {'type': 'bool', 'dom': None, 'owner': 'sys'}},
 '_aux0',
 '(_aux0 <=> b)',
 '((X _aux0) <=> (    (X b) \\/ ((X a) /\\ _aux0)))',
 [])

The translation of the formula a S b is _aux0. The variable _aux0 becomes TRUE when b becomes TRUE. Afterwards, _aux0 remains TRUE as long as a is TRUE, until b become TRUE again. So variable _aux0 remembers if a has been uninterruptedly TRUE since the last state when b was TRUE.

The operator "until" can also be translated (for a closed system):

>>> past.translate('a U b', until=True)

({'_aux0': {'type': 'bool', 'dom': None, 'owner': 'sys'}},
 '_aux0',
 'True',
 '(_aux0 <=> (    (b) \\/ ((a) /\\ (X _aux0))))',
 ['((b) \\/ ~ _aux0)'])

An example with more than one temporal operator of past LTL:

>>> past.translate('-[] (a S b)')

({'_aux0': {'type': 'bool', 'dom': None, 'owner': 'sys'},
  '_aux1': {'type': 'bool', 'dom': None, 'owner': 'sys'}},
 '(~ _aux1)',
 '((_aux0 <=> b)) /\\ ((_aux1 <=> ( ~ _aux0 )))',
 '(((X _aux0) <=> (    (X b) \\/ ((X a) /\\ _aux0)))) /\\ (((X _aux1) <=> (    (X ( ~ _aux0 )) \\/ ((X True) /\\ _aux1))))',
 [])

thisiscam commented 4 years ago

@johnyf Thanks for the detailed reply!

I think I understand now. Just to confirm, is the following correct:

>>> past.translate('a S b')

({'_aux0': {'type': 'bool', 'dom': None, 'owner': 'sys'}},
 '_aux0',
 '(_aux0 <=> b)',
 '((X _aux0) <=> (    (X b) \\/ ((X a) /\\ _aux0)))',
 [])

This is really saying that a S b is equivalent to _aux0, given that (_aux0 <=> b) /\\ []((X _aux0) <=> ( (X b) \\/ ((X a) /\\ _aux0))) (initial condition conjuncted with "always transition relation".

In other words, I think another way to say this is that a S b is equivalent to

exists _aux0, (_aux0 <=> b) /\\ []((X _aux0) <=> (    (X b) \\/ ((X a) /\\ _aux0)))

(where I existentially quantified _aux0 to project it out)

johnyf commented 4 years ago

This is correct provided that the translated formula a S b occur within the scope of the temporal existential quantifier.

Stutter-invariant temporal existential quantification in the temporal logic of actions, TLA+ is denoted by \EE. Please refer to this book about TLA+ and this paper about TLA.

If we denote stutter-sensitive temporal existential quantification in raw TLA+ by \ee, then the translation of the formula a S b could be written as follows (in TLA+ prime ' denotes the operator "next"):

\ee _aux0:  /\ _aux0
            /\ (_aux0 <=> b)
            /\ []((_aux0') <=> ((b') \/ ((a') /\ _aux0)))

The translation of past temporal operators is based on Section 5 of this paper. Quantified propositional temporal logic (QPTL) is described in this paper.

Another example would be translating the formula [](a S b).

>>> past.translate('[] (a S b)')

({'_aux0': {'type': 'bool', 'dom': None, 'owner': 'sys'}},
 '( [] _aux0 )',
 '(_aux0 <=> b)',
 '((X _aux0) <=> (    (X b) \\/ ((X a) /\\ _aux0)))',
 [])

The translated formula in raw TLA+ would be (== in TLA+ denotes a definition)

TranslatedFormula ==
    \ee _aux0:
        /\ [] _aux0
        /\ _aux0 <=> b
        /\ [](_aux0' <=> (b' \/ (a' /\ _aux0)))

The formula [](a S b) is equivalent to the translated formula, i.e.,

OriginalFormula == [](a S b)

THEOREM
    OriginalFormula <=> TranslatedFormula

The TLA+ proof language is described in this document.

The variable _aux0 could be considered a history-determined variable in raw TLA+. History-determined variables in TLA are discussed in Section 2.4 of this paper.

Realizability of properties with quantified history-determined variables is preserved when "unhiding" the history-determined variables by removing the temporal quantifier, as discussed in Section 9.7 on pages 154--157 of this dissertation (Table 3.2 on page 18 lists temporal and rigid quantifiers).

So GR(1) synthesis can be used when past temporal operators occur, after applying the translation of the past temporal operators and the addition of the auxiliary, history-determined variables.

The preservation of realizability when unhiding history-determined variables is described in detail in the module HistoryIsRealizable in the supplemental material, in particular the theorem RealizingHistory.

A definition of stutter-sensitive temporal quantification is included on page 4 of the module TemporalLogic in the supplemental material.

tulip-control / omega

How does logic.past work? #11