Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / Verification and synthesis of MITL through alternating timed automata - Estévenart
Tags: AlphabetLocationInitialFinalTran autDone defToAut hasSeenConjDef toBinaryRelation
On every note of this deck, unless a note says otherwise:
Chapter: 2

Definition: The set of all intervals whose ends are in \(S\)
Page: 11
Section: 1
Variables: \(S\subseteq \mathbb R\)
Notation: \(\mathcal I(S)\)
Kind: Def

Definition: \(i\in P\) holds for each \(i\in I\)
Page: 11
Section: 1
Variables: \(P\subseteq \mathbb R\) a property
\(I\in\mathcal I(\mathbb R)\)
Notation: \(P(I)\)
Index: 3
Kind: Def

Name: Adjacent interval
Definition: A pair of interval of the form \(\langle_i a_i,b_i\rangle_i\), with \(b_1=a_2\) and \(\bigcup \langle_i a_i,b_i\rangle_i=\langle_1 a_1,b_2\rangle_2\)
Page: 11^2
Section: 1
Index: 4
Kind: Def

Definition: \(\{i-t\in \mathbb R\mid i\in I\land i\ge t\}\)
Page: 11
Section: 1
Variables: \(I\) an interval,
\(t\in\mathbb R^+\)
Notation: \(I-t\)
Index: 3
Kind: Def

Definition: \(\{i+t\in \mathbb R\mid i\in I\}\)
Page: 11
Section: 1
Variables: \(I\) an interval,
\(t\in\mathbb R^+\)
Notation: \(I+t\)
Index: 3
Kind: Def

Definition: \(P(i,j)\) holds for each \(i\in I,j\in J\)
Page: 12
Section: 1
Variables: \(I,J\) intervals,
\(P\) a binary property on \(\mathbb R\)
Notation: \(P(I,J)\)
Index: 3
Kind: Def

Name: A time sequence
Definition: A non-decreasing sequence of non-negative reals
Page: 13
Section: 1
Index: 7
Kind: Def
Denoted by: \(\overline{\tau}\)

Name: A timed word
Definition: The pair with a word and a time sequence of the same length.
Page: 13
Section: 1
Variables: \(\Sigma\) an alphabet
Index: 7
Kind: Def

Name: The set of finite timed words
Page: 13
Section: 1
Variables: \(\Sigma\) an alphabet,
Notation: \(T\Sigma^*\)
Index: 7
Kind: Def

Name: The set of infinite timed words
Page: 13
Section: 1
Variables: \(\Sigma\) an alphabet,
Notation: \(T\Sigma^\omega\)
Index: 7
Kind: Def

Name: A timed language
Definition: A set of timed words
Page: 13
Section: 1
Variables: \(\Sigma\) an alphabet,
Index: 8
Kind: Def

Name: A determinizable Büchi automaton over infinite words
Definition: A Büchi automaton equivalent to a deterministic Büchi automaton
Page: 16
Variables: \(\Sigma\) an alphabet,
Index: 20
Kind: Def

Name: A positive boolean formula over \(L\)
Definition: A positive Boolean combination of \(\top,\bot\) and element of \(L\)
Page: 20
Variables: \(L\) a set
Index: 31
Kind: Def

Name: The set of positive boolean formulas over \(L\)
Page: 20
Variables: \(L\) a set
Notation: \(B^+(L)\)
Index: 31
Kind: Def

Name: An alternating automaton
Definition: A tuple \((\Sigma,L,\ell_0,F,\delta)\), as an automaton, with \(\delta:L\times \sigma\to B^+(L)\)
Page: 21
Index: 32
Kind: Def

Name: A conjunctive transition
Definition: Intuitively, when this transition is taken, multiple automaton are created, and all runs simultaneously. They all must accept
Page: 21
Index: 32
Kind: Def
Denoted by: An arrow split.
A single tail,
one head by successor

Name: A configuration
Definition: A finite set of locations of \(A\)
Page: 21
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Index: 32
Kind: Def

Name: Its initial configuration
Definition: \(\{\ell_0\}\)
Page: 21
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Index: 32
Kind: Def

Name: An accepting configuration
Definition: A subset of \(F\)
Page: 21
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Context: alternating automaton
Index: 32
Kind: Def

Name: The set of configurations of \(\mathcal A\)
Page: 21
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Notation: \(\text{Config}(\mathcal A)\)
Index: 32
Kind: Def

Name: A model of \(\gamma\)
Definition: A subset of \(L\) such that \(\gamma\) is true when the elements of this subsets are assigned to true, and everything else to false.
Page: 21
Variables: \(L\) a set,
\(\gamma\in B^+(L)\)
Index: 35
Kind: Def
Denoted by: \(M\)

Name: A minimal model of \(\gamma\)
Definition: A model, minimal for the inclusion function
Page: 21
Variables: \(L\) a set,
\(\gamma\in B^+(L)\)
Index: 35
Kind: Def

Definition: The set of minimal models \(M\) of \(\delta(\ell,\sigma)\)
Page: 21
Variables: \((\Sigma,L,\ell_0,F,\delta)\) an alternating automaton,
\(\ell\in L\),
\(\sigma\in \sigma\)
Notation: \(\text{Succ}(\ell,\sigma)\)
Index: 36
Kind: Def

Definition: The set of configurations \(\bigcup_{\ell\in C}M_\ell\), with \(M_\ell\) an element of \(\text{Succ}(\ell,\sigma)\).
Page: 21
Variables: \((\Sigma,L,\ell_0,F,\delta)\) an alternating automaton,
\(\ell\in L\),
\(C\) a configuration
Notation: \(\text{Succ}(C,\sigma)\)
Index: 36
Kind: Def
Definition2: I.e. a union of minimal model \(M_\ell\) for each \(\ell\in C\)

Name: A run on \(\mathcal A\) on \(\overline\sigma\)
Definition: A sequence of discrete transitions in \(\mathcal T_A\), labelled by \(\overline{\sigma}\)
Page: 23
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton,
\(\overline\sigma\in\Sigma^*\)
Index: 40
Kind: Def

Name: the semantic of \(\mathcal{A}\)
Definition: The transition system \((\text{Config}(\mathcal A),\rightarrow)\) with \(\rightarrow=\bigcup_{\sigma\in\Sigma}\xrightarrow{\sigma}\)
Page: 23
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Notation: \(\mathcal{T_A}\)
Index: 39
Kind: Def

Name: The set of succesors of \(\ell\) in \(C'\)
Definition: A set \(M_\ell\) such that \(C'=\bigcup_{\overline\ell\in C}M_{\overline\ell}\) and \(M_{\overline\ell}\in\text{Succ}(\overline\ell,\sigma)\)
Page: 23
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton,
\(\sigma\in\Sigma^*\)
\(C\) a configuration,
\(C'\in\mathrm{Succ}(C,\sigma)\)
\(\ell\in L\)
Context: alternating automata
Notation: \(\text{dest}(C,C',\ell)\)
Index: 39
Kind: Def
Typ: subset of \(C'\)

Definition: \(V=\bigcup_{0\le i\le|\overline\sigma|}V_i\)
Page: 24
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton,
\(\overline\sigma\in\Sigma^\infty\),
\(\pi=(C_i)_{0\le i\le|\overline\sigma|}\) a run of \(\mathcal A\) on \(\overline\sigma\)
Notation: \(G_\pi\)
Index: 41
Kind: Def
Definition2: \(V_i=\{(l,i)\mid l\in C_i\}\) the set of vertices of depth \(i\)
Conjdef: A tuple \((V,(\ell_0,0),\rightarrow)\) with:
Definition3: \((\ell_1,i)\rightarrow (\ell_2,i+1)\) for \(\ell_2\in \text{dest}(C_{i},C_{i+1},\ell_1)\)
Typ: Rooted DAG

Name: An accepting run over \(\overline \sigma\)
Definition: A run on \(\overline\sigma\) whose last configuration is accepting
Page: 25
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton,
\(\overline\sigma\in\Sigma^*\)
Index: 43
Kind: Def

Name: A word accepted by \(\mathcal A\)
Definition: A word which admits an accepting run in \(\mathcal A\).
Page: 25
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Index: 43, 44
Kind: Def

Definition: The language of finite words accepted by \(\mathcal A\)
Page: 25
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Notation: \(L(\mathcal A)\)
Index: 43
Kind: Def

Name: Branch of \(\pi\)
Definition: A finite or infinite path in \(G_\pi\)
Page: 25
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton,
\(\overline\sigma\in\Sigma^\omega\),
\(\pi=(C_i)_{0\le i\le|\overline\sigma|}\) a run of \(\mathcal A\) on \(\overline\sigma\)
Index: 44
Kind: Def
Denoted by: \(\beta\)

Name: The set of all infinite branches of \(G_\pi\)
Page: 25
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton,
\(\overline\sigma\in\Sigma^\omega\),
\(\pi=(C_i)_{0\le i\le|\overline\sigma|}\) a run of \(\mathcal A\) on \(\overline\sigma\)
Notation: \(Bran^\omega(G_\pi)\)
Index: 44
Kind: Def

Definition: The set of locations occurring infinitely often along \(\beta\)
Page: 25
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton,
\(\overline\sigma\in\Sigma^\omega\),
\(\pi=(C_i)_{0\le i\le|\overline\sigma|}\) a run of \(\mathcal A\) on \(\overline\sigma\),
\(\beta\in Bran^\omega(G_\pi)\)
Notation: \(inf(\beta)\)
Index: 44
Kind: Def

Name: An accepting run on \(\overline\sigma\)
Definition: A run \(\pi\) such that for all \(\beta\in Bran^\omega(G_\pi),\) \(\inf(\beta)\) intersects \(F\).
Page: 25
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton,
\(\overline\sigma\in\Sigma^\omega\),
Index: 44
Kind: Def

Definition: The language of infinite words accepted by \(\mathcal A\)
Page: 25
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Notation: \(L^\omega(\mathcal A)\)
Index: 44
Kind: Def

Page: 26
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Section: 2
Transitions: Transition: \(\delta'(S,a)\) being the set of \(\bigcup_{\ell\in S}M^\ell\), with, for all \(\ell\in S\), a minimal model \(M^\ell\) of \(\delta(\ell,\sigma)\)
States: \(\Sigma\)
Initial: initial location: \(\ell_0\)
Notation: \(\mathcal {B^A}\)
Locations: Set of locations: \(2^L\)
Kind: Def
Index: 46
Typ: TA
Labels: Final location: \(2^F\)

Definition: A Büchi automaton accepting the same language
Page: 27
Section: 3
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Notation: \(\mathcal A^{BM}\)

Definition: The set of subformulas of \(\Phi\)
Page: 30
Section: 3
Variables: \(\Phi\) a formula
Notation: \(Sub(\Phi)\)
Index: 52
Kind: Def

Name: The satisfiability problem
Definition: Given a formula, does there exists a word satisfying this formula
Page: 30
Section: 4.2

Question: The LTL satisfiability problem over finite word's complexity:
Answer: PSPACE-complete
Page: 30
Chapter: 2
Section: 4.2

Question: The LTL satisfiability problem over infinite word's complexity:
Answer: PSPACE-complete
Page: 30
Chapter: 2
Section: 4.2

Name: Model checking problem
Definition: Given a formula and an automaton, verifying whether the language accepted by the automaton is included in the language defined by the formula
Page: 31
Section: 4.2

Question: The LTL problem cheking complexity:
Answer: PSPACE-complete
Page: 32
Chapter: 2
Section: 4.2

Page: 23
Definition: The relation on pairs of configurations \((C,C')\) with \(C'\in \text{Succ}(C,\sigma)\)
Chapter: 2
Variables: \(\mathcal A=(\Sigma,L,\ell_0,F,\delta)\) an alternating automaton
Notation: \(\xrightarrow{\sigma}\)
Kind: Def
Index: 39