Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / Logics for Real Time: Decidability and Complexity
Tags: complexity computer_to_instruction

Name: Temporal logic
Context: Model checking
Abbreviation: TL

Name: monadic predicate logic of order
Page: 4
Abbreviation: MLO

Name: The continuous canonical model
Definition: \(\langle R^+,<\rangle\)
Page: 4
Context: Real time logic

Name: The discrete canonical model
Definition: \(\langle N,<\rangle\)
Page: 4
Context: Timed logic

Name: Temporal logic with modality names \(O_1^{(k_1)},\dots,O_n^{k_n}\) with \(O_i\) of arity \(k_i\) and monadic predicate variable \(X_1,\dots,\)
Definition: \(\phi::= X\mid\neg\phi\mid\phi\land\phi\mid O^{(k)}(\phi_1,\dots,\phi_k)\)
Page: 4
Notation: \(TL(O_1^{(k_1)},\dots,O_n^{k_n})\)
Example: until is a binary modality

Name: A truth table for \(O^{(k)}\) in \(L\)
Definition: A formula \(\overline O(t_0,X_1,\dots, X_k)\) such that \(O_M(P_1,\dots,P_k)\) is the set of \(\tau\) such that \(M\models_{MLO}\overline O[\tau,P_1,\dots,P_k]\) for every structure \(M\)
Page: 4
Variables: \(L\) a predicate logic
\(O^{(k)}\) a modality
Example: \(\exists t>t_0 X(t)\)
Example2: \(\exists t_1(t_0<t_1\land Y(t_1)\land \forall t(t_0<t<t_1\to X(t)))\)
Applied to: eventually \(X\)
Applied to2: \(X\) until \(Y\)

Name: A temporal logic expressively complete for \(L\) over \(C\)
Definition: for every formula \(\psi(t_0,X_1,\dots, X_n)\in L\) with a single free first-order variable \(t_0\), there is \(\phi\in TL'\) which is equivalent to \(\psi\) over \(C\)
Page: 4
Variables: \(L\) a fragment of FO logic
\(C\) a class of structures
Definition2: for every formula \(\phi\in TL'\) there exists \(\psi(t_0,X_1,\dots, X_n)\in L\) with a single free first-order variable \(t_0\), which is equivalent to \(\psi\) over \(C\)
Example: \(TL(until,since)\)
Conjdef: both
Example3: \(TL(until,since,until_s,since_s)\) with Stavi's modalities
DefType: A temporal logic \(TL'\)
Applied to: MLO over continuous canonical model
Applied to3: MLO over arbitrary linear order model

Name: MLO^+
Definition: MLO with the +1 function
Page: 8
Chapter: 3
Section: 1
Variables: \(L\) a fragment of FO logic
\(C\) a class of structures

Name: The standard canonical model for MLO^+
Definition: \(\langle R^+,<,+1)\)
Page: 8
Chapter: 3
Section: 1
Variables: \(L\) a fragment of FO logic
\(C\) a class of structures

Page: 8
Section: 1
Chapter: 3
Time complexity: Undecidable
Variables: \(L\) a fragment of FO logic
\(C\) a class of structures
Effect: Satisfiability of MSO^+

Name: Quantitative temporal logic with modalities \(\Gamma\)
Definition: \(QTL(\Gamma)\) and the modalites \(\diamond_1 X\) and \(\overleftarrow\diamond_1 X\)
Page: 8
Chapter: 3
Section: 1
Variables: \(L\) a fragment of FO logic
\(C\) a class of structures
Abbreviation: \(QTL(\Gamma)\)

Name: Quantitative temporal logic
Definition: \(QTL(until,since)\)
Page: 8
Chapter: 3
Section: 1
Variables: \(L\) a fragment of FO logic
\(C\) a class of structures
Abbreviation: \(QTL\)

Definition: \(\exists t(t_0<t<t_0+1\land\phi(t))\)
Page: 8
Chapter: 3
Section: 1
Variables: \(\phi\) a MSO^+ formula
\(t_0\) a term of this logic
Notation: \((\exists t)_{>t_0}^{t_0+1}\phi\)

Definition: \(\exists t(t<t_0<t+1\land\phi(t))\)
Page: 8
Chapter: 3
Section: 1
Variables: \(\phi\) a MSO^+ formula
\(t_0\) a term of this logic
Notation: \((\exists t)_{>t_0}^{t_0-1}\phi\)

Name: Quantitative Monadic Logic of Order
Definition: Fragment of MLO^+ such that if \(\phi(t)\) is a formula of this fragment with \(t\) its only first-order free variable, then \((\exists)_{>t_0}^{t_0+1}\phi\) and \((\exists)_{>t_0-1}^{t_0}\phi\) also belong to this fragment
Page: 8
Chapter: 3
Section: 1
Variables: \(t_0\in\mathbb R^+\)
\(\phi\) a MSO^+ formula
Abbreviation: QMLO

Definition: \(\exists t_1[t_0<t_1\land X(t_1)\land \forall t(t_0<t<t_1\to \neg X(t))]\)
Page: 8
Chapter: 3
Section: 1
Variables: \(t_0\) a term
Notation: \(First(t_0,X)\)

Definition: The time during which \(X\) was true, or 0 if it's not true now
Page: 11
Chapter: 3
Section: 2
Variables: \(X\) monadic predicate
Notation: \(\Gamma(X)\)

Definition: \(First(t_0,X)\land(\exists t)_{>t_0}^{<t_0+n}X(t)\)
Page: 11
Chapter: 3
Section: 2
Variables: \(X\) monadic predicate
\(n\in\mathbb N\)
Notation: \(d_{<n}(X)\)
Extra: First means that there exists a first-moment after \(t_0\) when \(X\) holds.
Intuition: The first time \(X(t)\) exists and occurs after \(t_0\) is in distance smaller than \(n\)

Definition: \(\forall t(Y(t)\iff (\forall t_1)_{>t-1}^{<t}X(t_1)\)
Page: 12
Chapter: 5
Variables: \(X,Y\) monadic predicates
Notation: \(Timer(X,Y)\)
Index: 1
Kind: Def

Definition: \(\bigwedge_iTimer(X_i,Y_i)\)
Page: 12
Chapter: 5
Variables: \(X,Y\) monadic predicates
Notation: \(Timer_n(X_1,\dots,X_n,Y_1,\dots,Y_n)\)
Index: 1
Kind: Def
Definition2: \(Always((Y\iff{\overleftarrow\square_1}X))\)
Intuition: \(Y\) measures if \(X\) persisted for the duration of the last unit of time

Name: A simple timer formula
Definition: A formula of the form \(Timer(X,Y)\)
Page: 12
Chapter: 5
Variables: \(X,Y\) monadic predicates
Index: 1
Kind: Def

Name: \(Y\) is a timer for \(X\)
Definition: \(Timer(X,Y)\) holds
Page: 12
Chapter: 5
Variables: \(X,Y\) monadic predicates
Index: 1
Kind: Def

Name: A \(L\) formula in timer normal form
Definition: A formula of the form \(\exists\overline W(Timer_n(X_1,\dots,X_n,Y_1,\dots,Y_n)\land\phi)\) with \(\overline W\) a list of monadic variables and \(\phi\in L\)
Page: 12
Chapter: 5
Variables: \(L\) a logic
Index: 2
Kind: Def

Smaller0: \(Always(Y\iff\diamond_1X)\)
Greater0: the next occurence of \(X\)
Page: 12
Chapter: 5
Variables: \(X,Y\) monadic variables
\(t\in\mathbb R\)
Index: 3
Kind: Rem
Prefix Greater: \(Y\) holds until
Smaller1: \(Y\) holds at \(t\)

Smaller0: \(Always(Y\iff\diamond_1X)\)
Greater0: in the unit of time before \(t\)
Page: 12
Chapter: 5
Variables: \(X,Y\) monadic variables
\(t\in\mathbb R\)
Index: 3
Kind: Rem
Prefix Greater: \(Y\) holds
Smaller1: \(X\) holds at \(t\)

Smaller0: \(Always(Y\iff\diamond_1X)\)
Greater0: not at \(t\)
Page: 12
Chapter: 5
Variables: \(X,Y\) monadic variables
\(t\in\mathbb R\)
Index: 3
Kind: Rem
Prefix Greater: \(Y\) holds
Smaller1: \(X\) does not holds during \([t,t+1]\)

Question: How to rewrite \(\diamond_1X\) using past modalities and a timer for \(X\)
Answer: \(\exists Y\) such that the conjunction of the following holds
Page: 12
Chapter: 5
Variables: \(X\) monadic variable
Answer2: \(Always(Y\to until X)\)
Index: 3
Kind: Rem
Answer3: \(Always(X\to\overleftarrow\square_1Y)\)
Answer4: \(Always(\overleftarrow\diamond_1\neg X)\to\overleftarrow\diamond_{\le1}\neg Y\)
Answer5: \(Y\)
Extra: Check answer 4, it was initially written as Always(\overleftarrow\diamond_1\neg X)\to\overleftarrow_{\le1}\neg Y\)

Question: How to state that \(Y\) is a timer, without metric
Answer: \(Y\) is True at 0
Page: 14
Section: 6
Context: Real time logic
Answer2: \(Y\) has finite variability
Answer3: \(Y\) is a closed set

Question: How to state that \(Y\) is a potential timer for \(X\), without metric
Answer: If at a positive time \(t\), \(Y\) holds, then \(X\) was True for a while just before \(t\)
Page: 14
Section: 6
Context: real time logic
Answer2: if \(X\) is true forever, at some point \(Y\) is true forever
Answer3: if \(Y\) is true at \(b\) and \(X\) is true in \([b,c)\) then \(Y_i\) is true at \(c\)

Question: How to state that \(Y\) and \(Y'\), timers for \(X\) and \(X'\), are compatible (without metric)?
Answer: if at \(b\), \(Y\) is true and \(Y'\) is false, then there is an interval \((c,b)\) on which \(X\) is true and containing a point where \(X'\) is false
Page: 14
Section: 6
Context: real time logic
Answer2: if \(Y\) and \(Y'\) becomes true at the same point \(b\), then for every previous point \(c\), if \(X\) is true on the interval \((c,b)\) then so is \(X'\)

Name: A generalized truth table for \(O^{(k)}\)
Definition: a formula \(\overline O(Y,X_1,\dots,X_n)\) such that for every structure \(M\) and subsets \(P_1,\dots,P_k,Q\) of the universe, \(O_M(P1,\dots,P_k)=Q\) iff \(M\models_{MLO}\overline O[Q,P_1,\dots,P_k]\)
Page: 18
Section: 9
Variables: \(O^{(k)}\) a modality
Example: \(\forall t(Y(t)\iff\psi(t,X_1,\dots,X_k))\) for \(\psi\) a truth table of \(O\)

Smaller0: every \(O_i\) has a generalized truth table in second-order timer normal form
Greater0: the satisfiability of \(TL(O_1,\dots,O_n)\) for finite variability is decidable
Page: 18
Section: 9
Variables: \(O_1,\dots,O_n\) modalities

Smaller0: every \(O_i\) has a generalized truth table in first-order timer normal form
Greater0: the satisfiability of \(TL(O_1,\dots,O_n)\) is decidable
Page: 18
Section: 9
Variables: \(O_1,\dots,O_n\) modalities

Name: Q2MLO
Definition: if \(\phi(t0,t)\) is a formula of this set, with \(t_0,t\) the only first-order free variables, \(m<n\in\mathbb N\) then \((\exists t)_{\prec t_0+n}^{\succ t_0+m}\phi\) also belong to this set, with \(\prec,\succ\) beeing strong or weak comparison
Page: 19
Chapter: 9
DefType: Extension of first order MLO