Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / On the decidability and complexity of Metric Temporal Logic over finite words
Tags: hasSeenConjDef examplesSwitchExample1 récupéré

Name: A flow step
Definition: A transition in \(Q\times\mathbb R_{\ge0}\times Q\)
Page: 4
Section: 2.1
Variables: \((\Sigma,S,s_0,F,X,\Delta)\) a timed automaton
Context: Timed automata

Name: An edge-step
Definition: A transition in \(Q\times\Sigma\times Q\)
Page: 4
Section: 2.1
Variables: \((\Sigma,S,s_0,F,X,\Delta)\) a timed automaton

Name: The set of flow-step
Page: 4
Section: 2.1
Variables: \((\Sigma,S,s_0,F,X,\Delta)\) a timed automaton
Notation: todo

Name: The set of edge-step
Page: 4
Section: 2.1
Variables: \((\Sigma,S,s_0,F,X,\Delta)\) a timed automaton
Notation: \(\rightarrow\)

Definition: containing \(\top\), \(\bot\),
Page: 5
Section: 3
Variables: \(S\) a finite set of locations,
\(x\) a distinguised clock variable
Context: alternating timed automata
Notation: \(\Phi(S)\)
Definition2: elements of \(S\),
Conjdef: The set of formulas
Definition3: \(x\bowtie k\) for \(\bowtie\) being an inequality,
Definition4: closed under conjunction, disjonction,
Definition5: closed under adding \(x\) as a prefix.

Name: A timed alternating automaton
Definition: \(\delta:S\times\Sigma\to\Phi(S)\)
Page: 5
Section: 3
Variables: \(S\) a finite set of locations,
\(x\) a distinguised clock variable
Context: alternating timed automata
Index: 1
Kind: Def
Definition2: and the remaining as usual timed automaton
Conjdef: A 5-tuple, \((\Sigma,S,s_0,F,\delta)\)

Question: Language accepted by timed alternating automaton, but not by non-deterministic timed automaton ?
Answer: \((a^\omega,\tau)\) such that \(\tau_i-\tau_j\) is never equal to 1.
Page: 5
Section: 3
Index: 2
Kind: Ex

Question: Timed alternating automaton accepting \((a^\omega,\tau)\) such that \(\tau_i-\tau_j\) is never equal to 1.
Answer: \((\{s_0,s_1\},\{a\},s_0,\{s_0,s_1\},\delta)\) such that \(\delta(s_0,a)=s_0\land x.s_1\) and \(\delta(s_1,a)=s_1\land x\ne 1\).
Page: 5
Section: 3
Index: 2
Kind: Ex

Name: A state
Definition: An element of \(S\) and a clock valuation
Page: 6
Section: 3
Variables: \((\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,
Denoted by: \((s,v)\)

Name: The set of state
Definition: \(S\times\mathbb R_{\ge0}\)
Page: 6
Section: 3
Variables: \((\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,
Notation: \(Q\)

Definition: \((s,v)\in M\)
Page: 6
Section: 3
Variables: \((\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,
\(v\) a clock valuation
\(M\subseteq Q\)
\(s\in S\)
Notation: \(M\models_vs\)
Definition2: If \(\phi=x\bowtie k\), then \(v(x)\bowtie k\) for bowtie le ge =...

Definition: \(\nu(x)\bowtie k\)
Page: 6
Section: 3
Variables: \((\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,
\(v\) a clock valuation
\(M\subseteq Q\)
\(\bowtie\in\{\le,<,>,\ge\}\),
\(k\in\mathbb N\)
Notation: \(M\models_vx\bowtie k\)

Definition: \(M\models_0\phi\)
Page: 6
Section: 3
Variables: \((\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,
\(v\) a clock valuation
\(M\subseteq Q\)
\(\phi\) a MTL formula
Notation: \(M\models_vx.\phi\)

Smaller0: \(N\subseteq M\)
Greater0: (\(N\models_v\phi\) implies \(M\models_v\phi\))
Page: 6
Section: 3
Variables: \((\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,
\(v\) a clock valuation
\(N,M\subseteq Q\)
\(\phi\in\Phi(S)\)

Name: A configuration of \(\mathcal A\)
Typ: A finite set of states.
Page: 6
Section: 3
Variables: \(\mathcal A=(\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,

Name: The set of configurations
Page: 6
Section: 3
Variables: \(\mathcal A=(\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,
Notation: \(\wp(Q)\)

Name: The initial configuration
Definition: \(\{(s_0,0)\}\)
Page: 6
Section: 3
Variables: \(\mathcal A=(\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,

Name: The minimal model of \(\phi\) with respect to \(v\)
Definition: The element \(M\) of \(\wp(Q)\), minimal under inclusion, such that \(M\models_v(\phi)\)
Page: 6
Section: 3
Variables: \(\mathcal A=(\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,
\(x\) a distinguished variable
\(\phi\in\Phi(S)\),
\(v\) a clock valuation

Name: An accepting configuration
Definition: A configuration whose every states are accepting
Page: 6
Section: 3
Variables: \(\mathcal A=(\Sigma,S,s_0,F,\delta)\) a timed alternating automaton,
Example: The empty configuration