Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / The regular real-time languages
Tags: complexity computer_to_instruction

Name: A positively decidable formalism
Definition: constructively closed under \(\land\) and \(\lor\)
Page: 2
Chapter: 1
Definition2: such that its satisfiability is decidable
Conjdef: both
DefType: A formalism

Name: A fully decidable formalism
Definition: A positively decidable formalism also constructively closed under negation
Page: 2
Chapter: 1

Name: The history clock for \(p\)
Definition: The clock stating the time elapsed since the last time \(p\) was true
Page: 5
Chapter: 2
Section: 1
Variables: \(p\) a proposition
Notation: \(x_p\)

Name: The prophecy clock for \(p\)
Definition: The clock stating the time remaining since the next time \(p\) become true
Page: 5
Chapter: 2
Section: 1
Variables: \(p\) a proposition
Notation: \(y_p\)

Name: A floating automaton
Definition: \(Q\) a finite set of locations
Page: 5
Chapter: 2
Section: 1
Definition2: \(Q_0\subseteq Q\) the set of starting locations
Conjdef: The tuple
Definition3: \(\delta,\delta'\subseteq Q\times Q\) the set of forward and backward transition relations
Definition4: \(P\) a finite set of propositional symbols
Definition5: \(\lambda:Q\to\mathrm{BoolComb}(P)\) the labelling function from locations to propositions
Definition6: \(Q_F,Q_F'\subseteq\) the set of forward and backward accepting locations

Name: 2way Event-clock automata
Definition: \(Q\) a finite set of locations
Page: 5
Chapter: 2
Section: 1
Definition2: \(Q_0\subseteq Q\) the set of starting locations
Conjdef: The tuple
Definition3: \(\delta,\delta'\subseteq Q\times Q\) the set of forward and backward transition relations
Abbreviation: 2ECA
Definition4: \(P\) a finite set of propositional symbols
Definition5: \(\lambda:Q\to\mathrm{BoolComb}(P\cup\mathrm{Constr}(\mathbb C))\) the labelling function from locations to propositions and timing constraints
Definition6: \(Q_F,Q_F'\subseteq\) the set of forward and backward accepting locations
Definition7: \(\mathbb C\) a finite set of clocks (prophecy and history)

Name: A singular state for forward run
Definition: A state \(q\in Q\) such that \((q,q)\not\in\delta\)
Page: 5
Chapter: 2
Section: 1
Variables: \(A=(Q,Q_0,\delta,\delta',P,\lambda,Q_F,Q'_f)\) a floating automaton

Name: A singular state for backward run
Definition: A state \(q\in Q\) such that \((q,q)\not\in\delta'\)
Page: 5
Chapter: 2
Section: 1
Variables: \(A=(Q,Q_0,\delta,\delta',P,\lambda,Q_F,Q'_f)\) a floating automaton

Name: A backward run for \((\tau,t)\)
Definition: for each \(i<n\), \((q_i,q_{i-1})\in\delta'\)
Page: 5
Chapter: 2
Section: 1
Variables: \(A=(Q,Q_0,\delta,\delta',P,\lambda,Q_F,Q'_f)\) a floating automaton
\(\tau\) a timed state sequence
\(t\in\mathbb R^+\)
Definition2: \(q_0\in Q_0\)
Definition3: \(q_n\in Q_f'\)
Definition4: if \(q_i\) is singular for backward relation, then \(I_i\) is a singleton
Definition5: for each \(t'\in I_i\), \(\tau(t')\models \lambda(\rho(t'))\)
DefType: A finite sequence \(\rho=(\overline q,\overline I)\) of length \(n\)

Name: A forward run for \((\tau,t)\)
Definition: for each \(i\in\mathbb N\), \((q_i,q_{i+1})\in\delta\)
Page: 5
Chapter: 2
Section: 1
Variables: \(A=(Q,Q_0,\delta,\delta',P,\lambda,Q_F,Q'_f)\) a floating automaton
\(\tau\) a timed state sequence
\(t\in\mathbb R^+\)
Definition2: \(q_0\in Q_0\)
Conjdef: such that
Definition3: the sequence \((q_i)\) is infinitly often in \(Q_f\)
Definition4: if \(q_i\) is singular for forward relation, then \(I_i\) is a singleton
Definition5: for each \(t'\in I_i\), \(\tau(t')\models \lambda(\rho(t'))\)
DefType: A sequence \(\rho(\overline q,\overline I)\)

Name: \(A\) accepts \(\tau\) at time \(t\)
Definition: there exists accepting forward and backward runs starting at the same initial location
Page: 5
Chapter: 2
Section: 1
Variables: \(A=(Q,Q_0,\delta,\delta',P,\lambda,Q_F,Q'_f)\) a floating automaton
\(\tau\) a timed state sequence
\(t\in\mathbb R^+\)

Name: The set of level-\(i\) clock constraint
Definition: if \(i=0\), the empty set
Page: 5
Chapter: 2
Section: 1
Variables: \(i\in\mathbb N\)
\(P\) a set of propositions
Notation: \(\Gamma_i\)
Definition2: if \(i>0\), then the set of \(x_B\sim c\) or \(y_B\sim c\) with \(\sim\) being \(\le,<,=,>,\ge\), and \(B\) a recursive event-clock automaton of level less than \(i\) whose propositions are contained in \(P\)

Question: The expressivity of level-\(i\) event-clock automata is
Answer: strictly increasing with \(i\)
Page: 7
Chapter: 2
Section: 1

Question: The set of languages defined by event-clock automata is
Answer: closed under Boolean operation
Page: 7
Chapter: 2
Section: 1
Kind: Theo

Page: 7
Section: 1
Chapter: 2
Name: Emptiness problem for recursive event-clock automata
Kind: Theo
Space complexity: PSPACE-complete

Name: Formulas of first-order real-time sequential calculus
Definition: \(p(t)\) for \(t\) a first-order variable over \(\mathbb R^+\), \(p\) a monadic predicate
Page: 7
Chapter: 2
Kind: Theo
Definition2: \(t_1\sim t_2\) for \(t_1,t_2\) first-order variables over \(\mathbb R^+\) and \(\sim\) being \(\le,<,=,>\) or \(\ge\)
Conjdef: The set of formulas
Definition3: \((\exists t)\Phi\) with \(t\) a first-order variable
Definition4: \((\mathrm{Min}t_1)(t_1>t_2\land\Psi(t_1))\sim(t_2+c)\) and \((\mathrm{Max}t_1)(t_1<t_2\land\Psi(t_1))\sim(t_2+c)\) with \(\Psi\) a formula in the same language whose only free variable is \(t_1\)
Definition5: closed under Boolean operations

Name: Formulas of second-order real-time sequential calculus
Definition: constructed similarly to formulas of first-order real-time sequential calculus
Page: 7
Chapter: 2
Kind: Theo
Definition2: with quantifications over monadic predicates
Conjdef: The set of formulas

Name: Second-order real-time sequential calculus
Page: 7
Chapter: 2
Notation: \(\mathbf{MinMaxML}_2\)
Kind: Theo

Name: First-order real-time sequential calculus
Page: 7
Chapter: 2
Notation: \(\mathbf{MinMaxML}_1\)
Kind: Theo

Name: A closed formula of \(\mathbf{MinMaxML}_2\)
Definition: A formula of \(\mathbf{MinMaxML}_2\) without free variables
Page: 7
Chapter: 2
Kind: Theo

Name: A \(\omega\)-regular real-time language
Definition: defined by a \(\mathbf{MinMaxML}_2\)-formula
Page: 8
Chapter: 2
Definition2: accepted by a recursive event-clock automaton
Conjdef: equivalently
DefType: A language

Page: 8
Implementation: Transform the formula into a recursive event-clock automaton. Test whether it accepts a word
Section: 2
Name: Satisfiability of \(\mathbf{MinMaxML}_2\)
Time complexity: Non-elementary

Definition: \(\neg\phi\mathcal S_I\phi\)
Page: 9, 10
Variables: \(\phi\) a MTL formula
\(I=\mid a,b\mid\) an interval
Notation: \(\triangleleft_I\phi\)
Definition2: \(\square_{[0,a\mid}\neg\phi\land\lozenge_{[0,b\mid}\phi\) (using past operators)

Definition: \(\neg\phi\mathcal U_I\phi\)
Page: 9
Variables: \(\phi\) a MTL formula
\(I=\mid a,b\mid\) an interval
Notation: \(\triangleright_I\phi\)
Definition2: \(\square_{[0,a\mid}\neg\phi\land\lozenge_{[0,b\mid}\phi\)

Page: 9
Section: 1
Chapter: 3
Name: Satisfiability of MITL
Variables: \(\phi\) a MTL formula
\(I\) an interval
Space complexity: EXSPACE-complete

Page: 9
Section: 1
Chapter: 3
Name: Satisfiability of MITL_0,∞
Variables: \(\phi\) a MTL formula
\(I\) an interval
Space complexity: PSPACE-complete

Name: A counter-free \(\omega\)-regular real-time language
Definition: defined by a MITL formula
Page: 10
Chapter: 3
Section: 2
Definition2: Defined by a MITL_0,∞-formula
Conjdef: equivalenty
Definition3: Defined by a EventClockTL-formula
Definition4: Defined by a MinMaxML_1-formula
DefType: A language

Question: How to rewrite \(\phi_1\mathcal U_{\mid c,\infty}\phi\) in MITL_0-formula
Answer: \(\square_{(0,c\mid}(\phi_1\land(\phi_1\mathcal U_{(0,\infty)}\phi_2))\)
Page: 11
Chapter: 3
Section: 2
Variables: \(\phi_1,\phi_2\) MITL_0 formula,
\(c>0\)
Context: Signals

Name: An event clock
Definition: A prophecy clock or a history clock
Page: 1

Definition: \(\bot\mathcal U\phi\)
Page: 9
Chapter: 3
Section: 1
Variables: \(\phi\) a MITL formula
Context: Real-time languages
Notation: \(\mathcal J\phi\)

Definition: \(\bot\mathcal S\phi\)
Page: 9
Chapter: 3
Section: 1
Variables: \(\phi\) a MITL formula
Context: Real-time languages
Notation: \(\mathcal B\phi\)

Question: How to rewrite \(\lozenge_{\mid a,a+1\mid}\phi_1\) is MITL_0
Answer: By induction on \(a\)
Page: 12
Chapter: 3
Section: 2
Variables: \(\phi_1\) a MITL_0 formula
\(0<a\)
Answer2: \(\lozenge_{\mid a-1,a\mid}\triangleright_{1}\mathcal J\phi_1\) assuming \(\phi\) starts to hold at least \(1\) units apart from the previous one, and is left-open
Answer3: \(\lozenge_{\mid a-1,a\mid}\triangleright_{1}\phi_1\)
assuming \(\phi\) starts to hold at least \(1\) units apart from the previous one, and is left-closed
Answer4: \(\square_{\mid a-1,a\mid}\lozenge{(0,1)\mid}\phi_1\)

Question: How to rewrite \(\lozenge_{\mid a,b\mid}\phi_1\) is MITL_0
Answer: \(\bigvee_{c=a}^{b-a}\lozenge_{\mid a,a+1\mid}\phi_1\), with \(\mid\)'s potentially changed to ensure that the union of the small intertals equal the big interval
Page: 12
Chapter: 3
Section: 2
Variables: \(\phi_1\) a MITL_0 formula
\(0<a<b\)