Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / From MITL to Timed Automata
Tags: CorrectType

Name: A sequential function with bounded acausality
Definition: A sequential function \(f:A^\omega\to B^\omega\) such that there exists a constant \(c\) such that for every \(u\in A^*,v_1,v_2\in B^*\), with [$]\abs{u}+c=\abs{v_1}=\abs{v_2}[/$], \(f(u\alpha_1)=v_1\beta_1\) and \(f(u\alpha_2)=v_2\beta_2\) implies \(v_1=v_2\)
Page: 35
Chapter: 2
Section: 3.2
Variables: \(A,B\) alphabets
Example: \(\circ^d\)
Intuition: The \(n\)-th output is determined by the past, and a bounded future

Name: An interpretation of \(\phi\)
Typ: \(\mathbb N\to\mathbb B^n\)
Page: 2
Variables: \(\phi\) an LTL formula with \(n\) propositional variables
Denoted by: \(\xi\)

Name: The characteristic function of \(\phi\)
Definition: The function mapping sequences over \(\mathbb B^n\) into Boolean sequences such that the \(i\)-th element is 1 iff \((\xi,i)\models \phi\)
Page: 2
Variables: \(\phi\) an LTL formula with \(n\) propositional variables,
Denoted by: \(\Xi^\phi\)

Name: The temporal tester of \(\phi\)
Definition: An automaton which accepts sequences which satisfy \(\phi\)
Page: 3
Section: 2
Variables: \(\phi\) an LTL formula

Smaller0: \(\xi[t]=\xi[t+1]=p\bar q\)
Greater0: \(\Xi^{p\mathcal Uq}(\xi)[t]=\Xi^{p\mathcal Uq}(\xi)[t+1]\)
Page: 5
Section: 2
Variables: \(p,q\) propositional variables,
\(\xi\) an interpretation over \(\{p,q\}\),
\(t\in\mathbb N\)
Index: 1
Kind: Lem