Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / Real-time logic, complexity and expresiveness
Tags: fromAlgorithm hasNotNewEffectReturnsMeaning hasSeenConjDef

Name: \(\mathcal L^2\)
Definition: Second-order language with:
-uninterpreted unary predicate symbols,
-binary predicate symbol \(\le\),
-quantification over individual variables
-quantification over unary predicate symbols
Page: 3
Chapter: 1
Section: 2.1

Name: \(\mathcal L\)
Definition: First-order language with:
-uninterpreted unary predicate symbols,
-binary predicate symbol \(\le\),
-quantification over individual variables
Page: 3
Chapter: 1
Section: 2.1

Definition: Second-order theory of the natural numbers, with successor and monadic predicates.
Page: 3
Chapter: 1
Section: 2.1
Notation: S1S

Page: 3
Implementation: \(\forall p.(p(x)\land\forall z.(p(z)\to p(z+1))\to p(y))\)
Section: 2.1
Chapter: 1
Effect: \(x<y\) using \(+1\)

Definition: \(\mathcal L_T\) with quantification over unary predicate symbols
Page: 4
Chapter: 1
Section: 2.2
Notation: \(\mathcal L_T^2\)

Definition: Uninterpreted unary predicate symbols,
Page: 5
Chapter: 1
Section: 2.2
Notation: \(\mathcal L_T\)
Definition2: \(\le\) over state sort,
Conjdef: Two sorted logic, with state sort and time sort
Definition3: constant symbol 0,
Definition4: +1
Definition5: binary predicate symbols \(\le\), \(\cong_2,\cong_3,\dots\)
Definition6: \(f\) from state sort into time sort
Definition7: quantification over variables of both sort

Definition: The set of times \(i\) such that \(f^I(i)=f^I(i-1)+\delta\)
Page: 41
Section: 2.3
Variables: \(\psi\in\mathcal L_2^T\),
\(I\) an interpretation for \(\psi\)
Notation: \(Tdiff^J_\delta\)
Assuming: \(\delta<d(\psi)\)

Name: Response formula
Definition: \(\forall i.(p(i)\implies \exists j\ge i.q(j))\)
Page: 39
Section: 2.1
Notation: \(\phi_{R}\)
Definition2: \(\big(\{p,q\}+\{q\}+\{\}+(\{p\};true^*;(\{p,q\}+\{q\}))\big)^\omega\)

Definition: The lcm of the constants \(c\) such that \(\cong_c\) occurs in \(\phi\)
Page: 6
Section: 2.3
Variables: \(\phi\in\mathcal L^2_T\)
Notation: \(c(\phi)\)

Definition: The set of times \(i\) such that \(f^I(i)\ge f^I(i-1)+c(\psi)\)
Page: 5
Section: 2.3
Variables: \(\psi\in\mathcal L_2^T\),
\(I\) an interpretation for \(\psi\)
Notation: \(Tdiff^J_{\ge c(\psi)}\)

Definition: The set of times \(i\) such that \(f^I(i)\cong t\mod d(\psi)\)
Page: 6
Section: 2.3
Variables: \(\psi\in\mathcal L_2^T\),
\(I\) an interpretation for \(\psi\)
Notation: \(Tcong^I_{d(\psi),t}\)
Assuming: \(\delta<d(\psi)\)

Name: An extended time sequence
Definition: agrees with \(I\) on \(p_i\),
Page: 42
Section: 2.3
Variables: \(\phi\in\mathcal L^2_T\)
Let \(p_1,\dots,p_n\) the predicate symbols,
\(I\) an interpretation for \(\phi\)
Definition2: aggrees with \(Tdiff_{\delta}\) and \(Tcong_{d(\phi),t}\) according to their intended meaning
Conjdef: The interpretation which
Denoted by: \(J\)

Smaller0: \(I\) and \(J\) have the same underlying state sequence
Greater0: \(I\in\mathcal M_T(\phi)\) iff \(J\in\mathcal M_T(\phi)\)
Page: 42
Section: 2.3
Variables: \(\phi\in\mathcal L^2_T\)
\(p_1,\dots,p_n\) the predicate symbols,
\(I,J\) interpretations for \(\phi\)
Index: 1
Kind: Lem

Name: An untimed model of \(\phi\)
Definition: The extended time sequence of some model of \(\phi\)
Page: 43
Section: 2.3
Variables: \(\phi\in\mathcal L^2_T\)

Definition: The set of untimed model of \(\phi\)
Page: 43, 46
Section: 2.3
Variables: \(\phi\in\mathcal L^2_T\)
Notation: \(\mathcal M ^*_T(\phi)\)
Index: , 2
Kind: ,cor
Typ: Regular \(2^{\{p_i\mid i\}\times (\{Tdiff_i\mid i\}\cup\{Tdiff_{\ge(\phi)}\})\times\{Tcong_{d(\phi),i}\}}\)

Page: 43
Implementation: -Replacing each \(\exists x.\psi(x)\) by \(\bigvee_{\delta=0}^\Delta\psi(\delta)\lor\exists i_x\bigvee_{\delta=0}^\Delta\psi(f(i_x)+\delta)\)
-Replacing each \(f(i)\le f(j)+c\) by \(\bigvee_{d=0}^c\psi_d(i,j)\) where \(\psi_0(i,j)=\forall x.(i<k\le j\implies Tdiff_0(k))\) and \(\psi_d(i,j)=\bigvee_{e=0}^d\exists k.i<k\le j\land\psi_0(i,k)\land Tdiff_e(k)\land\psi_{d-e}(k+1,j)\), and similarly for other in(equality)
-Replacing \(f(i)\equiv_dc\) by \(\bigvee_{k=1}^{d(\phi)/d} Tcong_{d(\phi),k}(i)\)
-Adding axioms for \(Tdiff_i\),\(Tcong_{d(\phi),i}\), and for realting \(Tcong\) and \(Tdiff\)
Section: 2.3
Effect: An equivalent \(\mathcal L^2\)-formula defining the extended time sequences of \(\phi\)
Variables: \(\phi\in\mathcal L^2_T\)

Question: \(\bigcirc_I\phi\)'s semantic in TPTL is
Answer: \(x.\bigcirc y.(y\in x+I\land\phi)\)
Page: 67
Section: 4.1
Variables: \(\phi\in\mathrm{MTL}\)
Extra: todo: jump from earlier

Question: [$]\bigominus_I\phi[/$]'s semantic in TPTL is
Answer: [$]x.\bigominus y.(y\in x-I\land\phi)[/$]
Page: 67
Section: 4.1
Variables: \(\phi\in\mathrm{MTL}\)

Question: \(\phi_1\mathcal U_I\phi_2\)'s semantic in TPTL is
Answer: \(x.(\phi_1\mathcal U y.(y\in x+I\land\phi_2)\)
Page: 67
Section: 4.1
Variables: \(\phi_i\in\mathrm{MTL}\)

Question: \(\phi_1\mathcal S_I\phi_2\)'s semantic in TPTL is
Answer: \(x.(\phi_1\mathcal S y.(y\in x-I\land\phi_2)\)
Page: 67
Section: 4.1
Variables: \(\phi_i\in\mathrm{MTL}\)

Question: \(Sub(\psi_1\to\psi_2)\)
Answer: equals \(\{\psi_1,\psi_2\}\)
Page: 69
Section: 4.2
Variables: \(P\) a set of propositions,
\(\phi_i\in\mathrm{MTL_P}\)

Question: \(Sub(\psi_1\mathcal U_I\psi_2)\)
Answer: equals \(\{\psi_1,\psi_2\}\cup\{\bigcirc(\psi_1\mathcal U_{I-\delta}\psi_2)\mid \delta\ge 0\}\)
Page: 69
Section: 4.2
Variables: \(P\) a set of propositions,
\(\phi_i\in\mathrm{MTL_P}\),
\(I\) an interval

Question: \(Sub(\psi_1\mathcal S_I\psi_2)\)
Answer: equals [$]\{\psi_1,\psi_2\}\cup\{\bigominus(\psi_1\mathcal S_{I-\delta}\psi_2)\mid \delta\ge 0\}[/$]
Page: 69
Section: 4.2
Variables: \(P\) a set of propositions,
\(\phi_i\in\mathrm{MTL_P}\),
\(I\) an interval

Question: \(Sub(\bigcirc S_I\psi)\)
Answer: equals \(\{\psi\}\)
Page: 69
Section: 4.2
Variables: \(P\) a set of propositions,
\(\phi_i\in\mathrm{MTL_P}\),
\(I\) an interval

Question: [$]Sub(\bigominus S_I\psi)[/$]
Answer: equals \(\{\psi\}\)
Page: 69
Section: 4.2
Variables: \(P\) a set of propositions,
\(\phi_i\in\mathrm{MTL_P}\),
\(I\) an interval

Name: The closure of \(\phi\)
Definition: containing \(\phi\)
Page: 69
Section: 4.2
Variables: \(P\) a set of propositions,
\(\phi\in\mathrm{MTL_P}\),
Definition2: closed under the \(Sub\) function
Conjdef: The least set
Abbreviation: \(closure(\phi)\)

Name: Bounded-response formula
Definition: \(\forall i.(p(i)\implies\exists j\ge i.q(j)\land f(j)\le f(i)+1)\)
Page: 40
Section: 2.2
Notation: \(\phi_{BR}\)