Title: Theory / Unimportant / CS / Fundamental / Model Checking / LTL / An antichain algorithm for LTL realizability
Tags: fromImplication examplesSwitchExample1 hasSeenConjDef EquivalentButNoIntermediate addIntermediateCard closed defToAut fromAlgorithm fromMath hasNotNewEffectReturnsMeaning mathToSee mid1516974248815 oldAlgoNewName récupéré toBinaryRelation toUnary

Definition: \(2^I\)
Page: 4
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(I\) a set of input signals
Notation: \(\Sigma_I\)

Definition: \(2^O\)
Page: 4
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(O\) a set of output signals
Notation: \(\Sigma_O\)

Definition: \(I\cup O\)
Page: 4
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(I,O\) sets of input/output signals
Denoted by: \(P\)

Definition: \(2^P\)
Page: 4
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(I,O\) sets of input/output signals
Context: LTL
Notation: \(\Sigma\)

Name: The realizability game
Definition: Two players, \(I\) and \(O\)
A state: an element of \(\Sigma^*\)
Turn: at turns \(n\), \(O\) gives a subset \(o_n\subseteq O\), then \(I\) gives a subset \(i_n\subseteq I\). It creates the state \((i_n\cup o_n)\) which is appended to the state
Page: 4
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(I,O\) sets of input/output signals

Name: A strategy for \(O\)
Definition: A function \((\Sigma_O\Sigma_I)^*\to \Sigma_O\)
Page: 4
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(I/O\) sets of input/output signals
Denoted by: \(\lambda_O\)

Name: A strategy for \(I\)
Definition: A function \((\Sigma_O\Sigma_I)^*\Sigma_O\to \Sigma_I\)
Page: 4
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(I,O\) sets of input/output signals
Denoted by: \(\lambda_I\)

Name: The realizability problem
Definition: Given \(\phi\in LTL\), decide whether this formula is realizable
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2

Name: A realizable formula
Definition: A formula \(\phi\in LTL\) such that there exists a strategy \(\lambda_O\) such that for all strategies \(\lambda_I\), \(outcome(\lambda_O,\lambda_I)\models\phi\)
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Example: \(I=\{q\}\), \(O=\{p\}\),
\(\lozenge q\to (p\mathcal U q)\),
\(\lambda_I\) consists in always playing \(\{I\}\)

Smaller0: \(\phi\) is realizable
Greater0: \(\phi\) is realized by a finite-state strategy
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(\phi\in LTL\)
Smaller to greater: iff

Name: A non realizable formula
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Example: \(p\mathcal U q\) for \(I=\{q\}\), \(O=\{p\}\)

Name: An infinite word automaton
Definition: \(\Sigma\) an alphabet
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Definition2: \(Q\) the finite set of states
Conjdef: A tuple
Definition3: \(q_0\in Q\) the initial state
Definition4: \(\alpha\subseteq Q\) The set of final states
Definition5: \(\delta\subseteq Q\times\Sigma\times Q\) the transition relation

Name: the set of runs of \(A\) on \(w\)
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(A=(\Sigma,Q,q_0,\alpha,\delta)\) an infinite word automaton,
\(w\in\Sigma^\omega\)
Abbreviation: \(Runs_A(w)\)

Definition: The number of times \(q\) occurs along \(\rho\)
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(A=(\Sigma,Q,q_0,\alpha,\delta)\) an infinite word automaton,
\(\rho\) a run,
\(q\in Q\)
Notation: \(Visit(\rho,q)\)

Name: A word accepted for the Universal Co-Büchi condition
Definition: A word \(w\in\Sigma^\omega\) such that, for each run \(\rho\in Runs_A(w)\), for each final state \(q\in \alpha\), \(Visit(\rho,q){\lt}\infty\)
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(A=(\Sigma,Q,q_0,\alpha,\delta)\) an infinite word automaton,

Name: A word accepted for the Universal \(K\)-Co-Büchi condition
Definition: A word \(w\in\Sigma^\omega\) such that, for each run \(\rho\in Runs_A(w)\), for each final state \(q\in \alpha\), \(Visit(\rho,q)\le K\)
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(A=(\Sigma,Q,q_0,\alpha,\delta)\) an infinite word automaton,
\(K\in\mathbb N\)

Name: An infinite word automaton with the non-determinstic Büchi condition
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Abbreviation: A NBW

Definition: The set of words accepted by \(A\) for the non-determinsitic Büchi condition
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(A=(\Sigma,Q,q_0,\alpha,\delta)\) an infinite word automaton
Notation: \(L_b(A)\)

Definition: The set of words accepted by \(A\) for the universal Co-Büchi condition
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(A=(\Sigma,Q,q_0,\alpha,\delta)\) an infinite word automaton,
Notation: \(L_{\text{uc}}(A)\)

Definition: The set of words accepted by \(A\) for the universal \(K\)-Co-Büchi condition
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(A=(\Sigma,Q,q_0,\alpha,\delta)\) an infinite word automaton,
\(K\in\mathbb N\)
Notation: \(L_{\text{uc},K}(A)\)

Name: A Universal Co-Büchi automaton
Definition: An infinite word automaton with universal Co-Büchi condition
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Abbreviation: UCW

Name: A Universal \(K\)-Co-Büchi automaton
Definition: An infinite word automaton with universal \(K\)-Co-Büchi condition
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Abbreviation: U\(K\)CW

Smaller0: \(\overline{L_{\text{uc}}(A)}\)
Greater0: \(L_b(A)\)
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(A=(\Sigma,Q,q_0,\alpha,\delta)\) an infinite word automaton,
Smaller to greater: =

Smaller0: \({L_{\text{uc}}(A)}\)
Greater0: \(\overline{L_b(A)}\)
Page: 5
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(A=(\Sigma,Q,q_0,\alpha,\delta)\) an infinite word automaton,
Smaller to greater: =
Extra: doublon

Name: A turn based automaton
Definition: \(\Sigma_I,\Sigma_0\) the input and output alphabet,
Page: 5
Section: 2
Variables: \(I,O\) sets of input/output signals,
Definition2: \(Q_I,Q_O\) the set of input and output sets,
Conjdef: The tuple
Definition3: \(q_0\in Q_0\) the initial state
Extra: Check whether its correct deck
Definition4: \(\alpha\subseteq Q_i\cup Q_O\) the set of final states
Definition5: \(\delta_I\subseteq Q_I\times \Sigma_I\times Q_O\) and \(\delta_O\subseteq Q_O\times \Sigma_O\times Q_I\) the input and output transition relations

Definition: The acceptance condition \(\textbf{C}\) for turn-based automata
Chapter: 2
Section: 6
Variables: \(C\) an acceptance condition of \(\omega\) automaton
Notation: \(\textbf{tbC}\)

Name: A Moore machine with \(\Sigma_I,\Sigma_O\)
Definition: \((\Sigma_I,\Sigma_O, Q_M,q_0,\delta_M,g_M)\) with.
-\(Q_M\) a finite set
-\(q_0\in Q_M\),
-\(\delta_M:Q_M\times \Sigma_I\to Q_M\)
-\(g_M:Q\to\Sigma_O\)
Chapter: 2
Section: 6
Variables: \(\Sigma_I,\Sigma_O\) input and output alphabet
Denoted by: \(M\)

Name: Its transition function
Chapter: 2
Section: 6
Variables: \(\Sigma_I,\Sigma_O\) input and output alphabet,
\(M\) a Moore machine
Notation: \(\delta_M\)

Name: A word accepted by \(M\)
Definition: A word \((o_n\cup i_n)_{n\in\mathbb N}\in \Sigma^\omega_P\) such that \(\delta^*_M(i_0\dots i_n)\) is defined and \(o_n=g_M(\delta^*_M(i_0\dots i_n-1))\) for all \(n\)
Chapter: 2
Section: 6
Variables: \(\Sigma_I,\Sigma_O\) input and output alphabet,
\(M=(\Sigma_I,\Sigma_O, Q_M,q_0,\delta_M,g_M)\) a Moore machine

Smaller0: \(L(M)\subseteq L_{uc}(A)\)
Greater0: \(L(M)\subseteq L_{uc,2mn}(A)\)
Page: 7
Section: 3
Variables: \(\Sigma_I,\Sigma_O\) input and output alphabet,
\(M\) a Moore machine with \(n\) states
\(A\) a \(\textbf{tbUCW}\) with \(m\) states
Index: 1
Kind: Lem
Smaller to greater: iff

Smaller0: \(A\) is realizable
Greater0: \(2^{2n+2}+1\)
Page: 7
Section: 3
Variables: \(\Sigma_I,\Sigma_O\) input and output alphabet,
Let \(A\) a \(\mathbf{tbUCW}\) with \(n\) states
Smaller to greater: iff
Prefix Greater: there exists a non-empty Moore machine with at most
Extra: Check whether its correct deck
Suffix Greater: states that realizes \(A\)

Definition: The language accepted by \(B\) under the acceptance condition \(c\).
Page: 17
Section: A.2
Variables: \(B\) an atomaton,
\(c:Q_B\to\mathbb N\) an acceptance condition,
Notation: \(L_{par,c}(B)\)
Extra: Check whether its correct deck

Definition: The set of words accepted by \(B\) according to the parity condition
Page: 17
Chapter: An Antichain Algorithm for LTL Realizability
Variables: \(B\) an automaton,
\(c\) a parity condition
Notation: \(L_{par,c}(B)\)

Definition: \((\Sigma_O\Sigma_I)^\omega\to(\Sigma_O\cup\Sigma_I)^\omega\) sending \((o_ni_n)_{n\in\mathbb N}\) to \((o_n\cup i_n)_{n\in\mathbb N}\)
Page: 17
Chapter: An Antichain Algorithm for LTL Realizability
Variables: \(O,I\) alphabets
Context: Two player game on AP
Notation: \(m\)

Definition: \(\mathcal F=\{-1,\dots,K+1\}^F\), the set of mappings from \(F\) to an integer between \(-1\) and \(K+1\)
Page: 8
Section: 3
Variables: \(A=(\Sigma,Q,q_0,\alpha,\Delta)\) a U\(K\)CW
Notation: \(det(A,K)\)
Index: 1
Kind: Prop
Definition2: \(F_0\) sending initial state to \(0\) if it is final, to \(1\) otherwise. Sending every other states to \(-1\).
Conjdef: A tuple with
Definition3: \(\alpha'\) the set of maps whose range contains \(K+1\)
Intuition: Its equivalent deterministic co-büchi automaton
Definition4: \(\mathbf{succ}(F,\sigma)\) the function sending \(q\)
to the maximal number of accepting states met during a run from \(q_0\) to \(q\) reading \(w\). Formally, \(\max\{\min(K+1,F(p)+(q\in \alpha))\mid q\in\Delta(p,\sigma),F(p)\ne-1\}\)

Name: Its equivalent deterministic co-büchi automaton
Definition: \(\text{det}(A,K)\) (with its \(\mathcal F_O,\mathcal F_I,F_0\))
Page: 8
Section: 3
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW
Notation: \(G(A,K)\)
Definition2: \(T=\{(F,F')\mid \exists\sigma\in\Sigma_O\cup\Sigma_I,F'=\text{succ}(F,\sigma)\}\)
Conjdef: The pair with
Definition4: \(\textbf{safe}=\mathcal F\setminus\alpha'\) the maps whose range does not contain \(K+1\)

Name: A safety game
Definition: A game with a safety winning condition
Page: 8
Section: 3

Smaller0: \(A\) is realizable
Greater0: player \(O\) has a winning strategy in the game \(G(A,2n(n^{2n+2}+1))\)
Page: 8
Section: 3
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW
Index: 2
Kind: theo
Smaller to greater: iff
Name: Reduction to safety game

Definition: \(2^{\mathcal F_O}\to2^{\mathcal F_I}\),
Sends a set \(S\) to the class of sets \(F\in safe\cap\mathcal F_I\) whose every \(T\)-successor belong to \(S\)
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
Notation: \(Pre_I\)

Definition: \(2^{\mathcal F_I}\to2^{\mathcal F_O}\),
Sends a set \(S\) to the class of sets \(F\in safe\cap\mathcal F_I\) which admits a \(T\)-successor (in \(S\)?)
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
Notation: \(Pre_O\)
Extra: \(S\) does not seems to be used in the definition !

Definition: \(\textbf{Pre}_O\circ\textbf{Pre}_I\)
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
Name: The controllable predecessor function
Monotonic: Monotonic
Abbreviation: \(\textbf{CPre}\)

Definition: The greatest fixpoint of \(\textbf{CPre}\)
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
Notation: \(\textbf{CPre}^*\)

Smaller0: \(s\in\textbf{CPre}^*\)
Greater0: \(O\) has a winning strategy from \(s\)
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
\(s\) a state in \(G(A,K)\)
Smaller to greater: iff

Smaller0: \(F_0\in\textbf{CPre}^*\)
Greater0: the specification of \(A\) is realizable
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
Smaller to greater: iff

Page: 9
Implementation: Computing \(S_0=\mathcal F\), \(S_i=\mathbf{Cpre}S_{i-1}\cap S_{i-1}\) and return the first fixed point.
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
Name: \(\mathbf{CPre}^*\)
Extra: effect

Page: 9
Definition: for each \(q\in Q_i\), \(F(q)\le F'(q)\)
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
\(i\in\{I,O\}\)
\(F,F'\in\mathcal F_i\)
Notation: \(F\preceq F'\)

Smaller0: \(F\preceq F'\)
Greater0: \(O\) can win from \(F'\) implies \(O\) can win from \(F\)
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
\(i\in\{I,O\}\)
\(F,F'\in\mathcal F_i\)
Index: 3
Kind: Theo
Context: tbU\(K\)CW,

Name: A closed subset of \(\mathcal F\) for \(\preceq\)
Definition: A set closed under taking \(\preceq\)-smaller elements.
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,

Name: The class of closed sets
Page: 9
Section: 4
Index: , 3
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
Kind: , Lem
Extra: union/intersections are finite, since the class is finite
Under: union
Under2: intersection
Under3: \(\mathbf{Pre}_{i}\)
Under4: \(\mathbf{CPre}\)

Name: The closure of \(S\)
Definition: The set of \(F\in\mathcal F\) which have a \(\prec\)-majorant in \(S\).
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
\(S\subseteq\mathcal F\)
Notation: \(\downarrow S\)

Smaller0: \(S=\downarrow\lceil S\rceil\)
Greater0: \(S\) is closed
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
\(S\subseteq\mathcal F\)
Smaller to greater: iff
Intermediate: \(S=\downarrow S\)

Name: An antichain
Definition: A set \(S\subseteq\mathcal F\) whose elements are \(\preceq\) incomparable
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,

Definition: The set of \(\preceq\)-maximal elements of \(S\)
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbU\(K\)CW,
\(S\subseteq\mathcal F\)
Notation: \(\lceil S\rceil\)
Definition2: The set of \(F\in S\) such that there exists no \(F'\in S\) with \(F\prec F'\)
Typ: Antichain

Smaller0: \(S\subseteq\mathcal F_I\)
Greater0: \(\mathrm{CPre}(S)\) is closed
Page: 9
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbUCW,
\(K=2n(n^{2n+2}+1)\)
\(G(A,K)=(\mathcal F_O,\mathcal F_I,F_0,T,\mathrm{safe})\)
\(S\subseteq\mathcal F\)
Index: 3
Kind: Lem
Smaller1: \(S\) is closed
Greater1: \(\mathrm{Pre}_O(S)\) is closed

Definition: \(q\mapsto \min(F_1(q),F_2(q))\)
Page: 10
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbUCW,
\(K=2n(n^{2n+2}+1)\)
\(G(A,K)=(\mathcal F_O,\mathcal F_I,F_0,T,\mathrm{safe})\)
\(L_1,L_2\subseteq\mathcal F\) antichains,
Notation: \(L_1\sqcap L_2\)
Index: 2 (iv)
Kind: Prop

Definition: [$]\defFun Q{\mathcal F}q{\min\{\max(-1,F(q')-(q'\in \alpha))\mid(q,\sigma,q')\in\delta\}}[/$]
Page: 10
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbUCW,
\(K=2n(n^{2n+2}+1)\)
\(G(A,K)=(\mathcal F_O,\mathcal F_I,F_0,T,\mathrm{safe})\)
\(\sigma\in\Sigma_I\cup\Sigma_O\),
\(F\in\mathcal F\)
Notation: \(\Omega(F,\sigma)\)
Kind: Prop

Definition: The set of \(F\in\mathcal F\) such that \(\mathrm{succ}(F,\sigma)\in S\)
Page: 10
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbUCW,
\(K=2n(n^{2n+2}+1)\)
\(G(A,K)=(\mathcal F_O,\mathcal F_I,F_0,T,\mathrm{safe})\)
\(\sigma\in\Sigma_I\cup\Sigma_O\),
\(S\subseteq\mathcal F\)
Notation: \(\mathrm{Pre}(S,\sigma)\)
Kind: Lem

Name: The set of independent sets of \(G\)
Definition: The set of \(W\subseteq V\) such that no elements of \(E\) is a subset of \(W\).
Page: 10
Section: 4
Variables: \(A=(\Sigma_O,\Sigma_I,Q_O,Q_I,q_0,\alpha,\Delta_O,\Delta_I)\) a tbUCW,
\(K=2n(n^{2n+2}+1)\)
\(G(A,K)=(\mathcal F_O,\mathcal F_I,F_0,T,\mathrm{safe})\)
Notation: \(\mathrm{IND}(G)\)

Name: The outcomes of these strategies
Definition: The infinite word \((o_n,i_n)_{n\in\mathbb N}\) such that \(o_n=\lambda_i(o_0i_0\dots o_{n-1}i_{n-1})\) and \(i_n=\lambda_i(o_0i_0\dots o_{n-1}i_{n-1}o_n)\)
Page: 4
Chapter: An Antichain Algorithm for LTL Realizability
Section: 2
Variables: \(I,O\) sets of input/output signals,
\(\lambda_I,\lambda_O\) stategies
Abbreviation: \(outcome(\lambda_O,\lambda_I)\)