LTLf synthesis with unobservable variables¶

In [1]:
import spot
spot.setup(show_default='.A') # Don't show acceptance conditions in twa, since we abuse twa to represent DFA

The following specification states that assuming u alternate between on and off (but we do not know its initial value), we eventually want that o=u. This is realizable, for instance by a controller that continuously assign the same value to o.

In [2]:
f = 'G((!u | X!u) & (u | Xu)) -> X[!]F(u <-> o)'
out = ['o']
unobs = [spot.formula.ap('u')]

Here is the automaton for f as an MTDFA, or as a DFA.

In [3]:
a = spot.ltlf_to_mtdfa(f); display(a); display(a.as_twa(True))
mtdfa S0 G((!u | X!u) & (u | Xu)) -> X[!]F(o <-> u) I->S0 B40 u S0->B40 S1 (u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) B42 u S1->B42 S2 (!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) B44 u S2->B44 B43 o B44->B43 B1 1 B44->B1 B41 o B42->B41 B42->B1 B38 (u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) B40->B38 B39 (!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) B40->B39 B43->B1 B43->B38 B41->B1 B41->B39
0 G((!u | X!u) & (u | Xu)) -> X[!]F(o <-> u) I->0 1 (u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) 0->1 !u 2 (!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) 0->2 u 1->2 !o & u 3 1 1->3 o | !u 2->1 o & !u 2->3 !o | u 3->3 1

In order to consider u as unobservable, we quantify it away.

In [4]:
qf = spot.formula.forall(unobs, f)
display(qf)
$\forall u: (\mathsf{G} ((\lnot u \lor \mathsf{X} \lnot u) \land (u \lor \mathsf{X} u)) \rightarrow \mathsf{X^{[!]}}\mathsf{F} (o \leftrightarrow u))$

Here is the game generated for synthesis. By comparing the labels of the states in this game and the previous one, we can see that u was quantified universally by replacing all u-labeled nodes by the conjunction of their children.

In [5]:
spot.ltlf_to_mtdfa_for_synthesis(qf, out, 
                                 approach="state_refine")  # slight simplifications, but no solving
Out[5]:
mtdfa S0 G((!u | X!u) & (u | Xu)) -> X[!]F(o <-> u) I->S0 B38 ((u & G((!u | X!u) & (u | Xu))) -> F(o <-> u)) & ((!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u)) S0->B38 S1 ((u & G((!u | X!u) & (u | Xu))) -> F(o <-> u)) & ((!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u)) B56 o S1->B56 S2 (!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) B28 o S2->B28 S3 (u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) B27 o S3->B27 B1 1 B28->B1 B0 0 B28->B0 B27->B1 B27->B0 B39 (!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) B56->B39 B55 (u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) B56->B55

Now, the solved version, and its corresponding Mealy machine:

In [6]:
strat = spot.ltlf_to_mtdfa_for_synthesis(qf, out)
display(strat)
display(spot.mtdfa_strategy_to_mealy(strat))
mtdfa S0 G((!u | X!u) & (u | Xu)) -> X[!]F(o <-> u) I->S0 B38 ((u & G((!u | X!u) & (u | Xu))) -> F(o <-> u)) & ((!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u)) S0->B38 S1 ((u & G((!u | X!u) & (u | Xu))) -> F(o <-> u)) & ((!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u)) B57 o S1->B57 S2 (!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) B28 o S2->B28 B1 1 B28->B1 B0 0 B28->B0 B57->B0 B39 (!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) B57->B39
0 G((!u | X!u) & (u | Xu)) -> X[!]F(o <-> u) I->0 1 ((u & G((!u | X!u) & (u | Xu))) -> F(o <-> u)) & ((!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u)) 0->1 1 / 1 2 (!u & G((!u | X!u) & (u | Xu))) -> F(o <-> u) 1->2 1 / !o 3 1 2->3 1 / !o 3->3 1 / 1

Note that the above example has no observable input variables, so we do not have to order input and output variables to decide between Moore and Mealy semantics. (See the ltlf2dfa notebook for how to do that.)

LTL synthesis with unobserved variables¶

Universal quantification is not straightfoward for ω-automata, so instead we translate the complemented formula, perform existential quantification, and determinize the result to complement it as a DPA.

This currently only supports Mealy semantics.

In [7]:
from spot.jupyter import display_inline
import buddy
spot.setup(show_default='.a') # Print acceptance conditions again.
In [8]:
def synt_w_unobs(f, out, unobs):
    quant_nba_neg = spot.translate(spot.formula.exists(unobs, spot.formula_Not(f)))
    display_inline("negated NBA after ∃-quantification:", quant_nba_neg)
    dpa_neg = spot.tgba_determinize(quant_nba_neg)
    display_inline("negated DPA:", dpa_neg)
    dpa = spot.dualize(dpa_neg)
    display_inline("DPA:", dpa)
    b = buddy.bddtrue
    for o in out:
        b &= buddy.bdd_ithvar(dpa.register_ap(o))
    dpa.set_synthesis_outputs(b)
    game = spot.split_2step(dpa)
    res = spot.solve_game(game)
    spot.highlight_strategy(game)
    display_inline("game:", game)
    display("REALIZABLE" if res else "UNREALIZABLE")
    if res:
        mealy = spot.solved_game_to_mealy(game)
        mealy = spot.unsplit_mealy(mealy)
        display_inline("Mealy controller:", mealy)
        spot.simplify_mealy_here(mealy, 2, False)
        display_inline("simplified Mealy controller:", mealy)
In [9]:
synt_w_unobs('G((!u | X!u) & (u | Xu)) -> X[!]F(u <-> o)', out = ['o'], unobs = unobs)
negated NBA after ∃-quantification:
t [all] 0 0 I->0 1 1 0->1 1 2 2 0->2 1 1->2 o 2->1 !o
negated DPA:
Fin( ⓿ ) & Inf( ❶ ) [Rabin 1] 0 0 I->0 1 1 0->1 1 2 2 1->2 !o ⓿ 3 3 1->3 o ❶ 2->3 o ❶ 3->2 !o ❶
DPA:
Inf( ⓿ ) | Fin( ❶ ) [gen. Streett 1] 0 0 I->0 1 1 0->1 1 2 2 1->2 !o ⓿ 3 3 1->3 o ❶ 2->3 o ❶ 4 4 2->4 !o 3->2 !o ❶ 3->4 o 4->4 1
game:
Inf( ⓿ ) | Fin( ❶ ) [gen. Streett 1] 0 0 I->0 5 5 0->5 1 1 1 5->1 1 6 6 1->6 1 ❶ 2 2 6->2 !o ⓿ 3 3 6->3 o ❶ 7 7 2->7 1 7->3 o ❶ 4 4 7->4 !o 8 8 3->8 1 8->2 !o ❶ 8->4 o 9 9 4->9 1 9->4 1 
'REALIZABLE'
Mealy controller:
0 0 I->0 1 1 0->1 1 / 1 2 2 1->2 1 / !o 3 3 2->3 1 / !o 3->3 1 / 1
simplified Mealy controller:
0 0 I->0 1 1 0->1 1 / 1 1->1 1 / !o

Let's change this a an unrealizable specification.

In [10]:
synt_w_unobs('G(u <-> X!u) & XF(u <-> o)', out = ['o'], unobs = unobs)
negated NBA after ∃-quantification:
t [all] 0 0 I->0 0->0 1
negated DPA:
t [all] 0 0 I->0 0->0 1
DPA:
f [none] 0 0 I->0 0->0 1
game:
f [none] 0 0 I->0 1 1 0->1 1 1->0 1 
'UNREALIZABLE'

There is also a shortcut to convert LTL into a Game, with a few extra simplifaction along the way. That is actually what is used in ltlsynt. This ltl_to_game() function takes an optional list of unobservable variables to quantify universally, and will take care of doing the negation/∃-quantification/complementation. The only downside is that you currently have to configure it to use DET_SPLIT or SPLIT_DET instead of more efficient approaches like LAR or ACD. (This should be fixed eventually.)

In [11]:
si = spot.synthesis_info()
si.s = spot.synthesis_info.algo_DET_SPLIT
spot.ltl_to_game('G(u <-> X!u) -> XF(u <-> o)', ['o'], si, ['u'])
Out[11]:
Fin( ⓿ ) [co-Büchi] 0 0 I->0 5 5 0->5 1 ⓿ 1 1 5->1 1 ⓿ 6 6 1->6 1 ⓿ 2 2 6->2 !o ⓿ 3 3 6->3 o ⓿ 7 7 2->7 1 7->3 o ⓿ 4 4 7->4 !o 8 8 3->8 1 8->2 !o ⓿ 8->4 o 9 9 4->9 1 9->4 1

Whith that function, our synthesis function can be simplified to this:

In [12]:
def synt_w_unobs2(f, out, unobs):
    si = spot.synthesis_info()
    si.s = spot.synthesis_info.algo_DET_SPLIT
    game = spot.ltl_to_game(f, out, si, unobs)
    res = spot.solve_game(game)
    spot.highlight_strategy(game)
    display_inline("game:", game)
    display("REALIZABLE" if res else "UNREALIZABLE")
    if res:
        mealy = spot.solved_game_to_mealy(game)
        mealy = spot.unsplit_mealy(mealy)
        display_inline("Mealy controller:", mealy)
        spot.simplify_mealy_here(mealy, 2, False)
        display_inline("simplified Mealy controller:", mealy)
In [13]:
synt_w_unobs2('G(u <-> X!u) -> XF(u <-> o)', out = ['o'], unobs = ['u'])
game:
Fin( ⓿ ) [co-Büchi] 0 0 I->0 5 5 0->5 1 ⓿ 1 1 5->1 1 ⓿ 6 6 1->6 1 ⓿ 2 2 6->2 !o ⓿ 3 3 6->3 o ⓿ 7 7 2->7 1 7->3 o ⓿ 4 4 7->4 !o 8 8 3->8 1 8->2 !o ⓿ 8->4 o 9 9 4->9 1 9->4 1 
'REALIZABLE'
Mealy controller:
0 0 I->0 1 1 0->1 1 / 1 2 2 1->2 1 / !o 3 3 2->3 1 / !o 3->3 1 / 1
simplified Mealy controller:
0 0 I->0 1 1 0->1 1 / 1 1->1 1 / !o
In [ ]: