Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / A really temporal logic
Tags: hasSeenConjDef

Name: A state
Definition: A subset of \(P\)
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,

Name: A state
Definition: A subset of \(P\)
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,
Context: TPTL

Name: A timed state
Definition: The pair with a state and a natural number
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,

Name: A term of TPTL
Definition: \(c\) with \(c\in\mathbb N\)
Page: 184
Section: 2.2
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Index: 2
Kind: Def
Definition2: \(c+x\) with \(c\in\mathbb N\), \(x\in V\)
Conjdef: Either

Name: The set of TPTL formulas
Definition: containing elements of \(P\)
Page: 184
Section: 2.2
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Index: 2
Kind: Def
Definition2: containing Timing constraints
Conjdef: The least set
Definition3: containing \(false\)
Definition4: closed under implications
Definition5: closed under next
Definition6: closed under until
Definition7: closed under time quantification.

Name: The timing constraints
Definition: \(\pi_1\le\pi_2\) for \(\pi_i\) some terms
Page: 184
Section: 2.2.1
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Context: TPTL
Definition2: \(\pi_1\equiv_d\pi_2\) for \(\pi_i\) some terms and \(d\in\mathbb N\)
Conjdef: Either

Name: A formula which contains no absolute time references
Definition: A formula such that each term contains a variable.
Page: 184
Section: 2.2.1
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables

Name: Freze quantifiers
Page: 184
Section: 2.2.3
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
\(\phi\) a TPTL formula with a free variable \(x\)
Notation: \(x.\phi(x)\)

Definition: \(\rho\models_{\mathcal E[x:=\tau_0]}\phi\)
Page: 184
Section: 2.2.3
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Let \(\rho=(\sigma,\tau)\) a timed state sequence,
\(\tau_0\in\mathbb R_{\ge0}\)
\(\mathcal E:V\to T\) an interpretation for the variables
Notation: \(\rho\models _{\mathcal E}x.\phi\)

Definition: The discrete time domain
Page: 183
Section: 2.1
Context: times automata
Notation: \(\mathbf{T}\)

Name: An interpretation for the variables
Typ: \(V\to\mathrm{T}\)
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,
\(V\) a set of variables
Denoted by: \(\mathscr{E}\)
Name2: An environment for the variables

Question: \(\rho\models_{\mathscr{E}}p\)
Answer: \(p\in\sigma_0\)
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Let \(\rho=(\sigma,\tau)\) a timed state sequence,
\(\mathscr{E}:V\to\mathrm{T}\),
\(p\in P\)
Index: 3
Kind: Def

Question: \(\rho\models_{\mathscr{E}}\pi_1\le\pi_2\)
Answer: \(\mathscr{E}(\pi_1)\le\mathscr{E}(\pi_2)\)
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Let \(\rho=(\sigma,\tau)\) a timed state sequence,
\(\mathscr{E}:V\to\mathrm{T}\),
\(\pi_1,\pi_2\) terms
Index: 3
Kind: Def

Question: \(\rho\models_{\mathscr{E}}\pi_1\equiv_d\pi_2\)
Answer: \(\mathscr{E}(\pi_1)\equiv_d\mathscr{E}(\pi_2)\)
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Let \(\rho=(\sigma,\tau)\) a timed state sequence,
\(\mathscr{E}:V\to\mathrm{T}\),
\(\pi_1,\pi_2\) terms
Index: 3
Kind: Def

Question: \(\rho\models_{\mathscr{E}}false\)
Answer: is impossible
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Let \(\rho=(\sigma,\tau)\) a timed state sequence,
\(\mathscr{E}:V\to\mathrm{T}\),
Index: 3
Kind: Def

Question: \(\rho\models_{\mathscr{E}}\phi_1\mathcal U\phi_2\)
Answer: \(\rho^i\models_{\mathscr{E}}\phi_2\) for some \(i\ge0\) and \(\rho^j\models_{\mathscr{E}}\phi_1\) for all \(0\le j<i\)
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Let \(\rho=(\sigma,\tau)\) a timed state sequence,
\(\mathscr{E}:V\to\mathrm{T}\),
\(\phi_1,\phi_2\in\text{TPTL}\)
Index: 3
Kind: Def

Question: \(\rho\models_{\mathscr{E}}x.\phi\)
Answer: \(\rho\models_{\mathscr{E}[x=\tau_0]}\phi\)
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Let \(\rho=(\sigma,\tau)\) a timed state sequence,
\(\mathscr{E}:V\to\mathrm{T}\),
\(\phi\in\text{TPTL}\)
Index: 3
Kind: Def

Question: \(\rho\models_{\mathscr{E}}\bigcirc\phi\)
Answer: \(\rho^i\models_{\mathscr{E}}\phi\) for some \(i\ge 0\)
Page: 183
Section: 2.1
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Let \(\rho=(\sigma,\tau)\) a timed state sequence,
\(\mathscr{E}:V\to\mathrm{T}\),
\(\phi\in\text{TPTL}\)
Index: 3
Kind: Def

Name: \(\rho\) is a model of \(\phi\)
Definition: \((\rho,\mathscr{E})\) satisfies \(\phi\) for any environment \(\mathscr{E}\)
Page: 185
Section: 2.1
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Let \(\rho=(\sigma,\tau)\) a timed state sequence,
\(\phi\in\text{TPTL}\) closed
Notation: \(\rho\models\phi\)
Index: 3
Kind: Def

Question: \(x.\phi\) is equivalent to the first order formula
Answer: \(\forall x.(x=now\to\phi)\) and \(\exists x.(x=now\land\phi)\)
Page: 186
Section: 2.3
Variables: \(P\) a set of propositional symbol,
\(V\) the set of variables
Let \(\rho=(\sigma,\tau)\) a timed state sequence,
\(\phi\in\text{TPTL}\) closed,
\(x\) a time variable
Index: 3
Kind: Def

Name: Timed Propositional Temporal Logic
Page: 183
Section: 2
Abbreviation: TPTL