Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / A tool for deciding the satisfiability of continuous-time metric temporal logic
Tags: fromMath

Name: falsy values
Definition: false
Page: 11
Chapter: 2
Context: JS ?
Definition2: null
Conjdef: All of
Definition3: undefined
Definition4: empty string
Definition5: 0
Definition6: NaN

Name: An homeomorphism
Definition: between the collection of open (closed) sets.
Page: 072, 4
Chapter: 2, 0 clasicall topology
Section: 3, 1
Variables: \(M,N\) metric spaces
\(f:M\to N\).
Context: Topology
Index: 12
Kind: Cor
Definition2: morphism whose inverse is a morphism
Conjdef: A bijection, equivalently

Name: An unambiguous union in \(M\)
Definition: \(P,Q\subseteq M\) such that \(\underline{P\cup Q}=\underline P+\underline Q\)
Page: 382, 228
Chapter: 1, 1
Section: 1, 4.1
Variables: \(\mathbb K\) a semiring
\(M\) a monoid
Context: Characteristic series in [$]\mathbb K\llangle M\rrangle[/$]
Index: 1
Kind: Prop
Definition2: \(P\) is disjoint from \(Q\)
Conjdef: An union of the form \(P\cup Q\), with
Name2: A disjoint union

Name: Simple operators
Definition: Arithmetic operator + * - / %
Page: 21
Chapter: 2
Section: 4
Context: C
Definition2: bitwise operator ! ^ & |
Conjdef: all of
Definition3: ?
Definition4: < >
Definition5: =
Definition6: .

Name: A temporal system
Definition: a set of variables \(V\)
Page: 174
Section: 2
Definition2: \(D\) a specific domain of interpretation for the variables
Conjdef: containing
Definition3: \(\mathcal R\) a finite family of relations on \(D\)
Denoted by: \(\mathcal D\)
DefType: A tuple

Name: Constraint LTL
Definition: LTL extended with a constraint system \(\mathcal D=(D,\mathcal R)\), and atomic formula from \(\mathcal R\)
Page: 174
Section: 2
Abbreviation: CLTL

Name: CLTL over clocks
Definition: CLTL where the domain \(D\) for variables is \(\mathbb R_+\)
Page: 174
Section: 2
Abbreviation: CLTLoc

Name: A temporal term
Definition: A real constant
Page: 174
Section: 2
Definition2: A clock variable
Conjdef: Either
Denoted by: \(\alpha\)

Name: A constraint
Definition: A formula of the form \(\alpha\sim\beta\) with \(\alpha,\beta\) temporal terms and \(\sim\) being \(<\) or =
Page: 174
Section: 2
Context: CLTLoc

Definition: A clock which is never reset
Page: 174
Section: 2
Context: TCTLoc
Notation: Now
Intuition: Allow to easily check the time between two letters

Name: The set of clock constraint on \(x\)
Definition: \(x=0\), \(x<c\), \(c<x\) and \(x=c\) for \(c\in\mathbb N^+\), \(0<x\)
Page: 177
Variables: \(V\) a set of clock
\(\phi\) a CLTLoc formula
\(x,y\in V\)
Notation: \(ac(x)\)

Name: The set of clock constraint on \(x\) and \(y\)
Definition: \(x+c\sim y\), \(y\sim x+c\), \(y+d\sim x\), \(x\sim y+d\) for \(c,d\in\mathbb N\), \(c<c(y)\), \(d<c(x)\)
Page: 177
Variables: \(V\) a set of clock
\(\phi\) a CLTLoc formula
\(x,y\in V\)
Notation: \(ac(x,y)\)

Definition: The maximal constant to which \(x\) is compared in \(\phi\)
Page: 177
Variables: \(V\) a set of clock
\(\phi\) a CLTLoc formula
\(x,y\in V\)
Notation: \(c(x)\)

Definition: \(\bigcup_{x,y\in V}ac(x)\cup ac(x,y)\)
Page: 177
Variables: \(V\) a set of clock
\(\phi\) a CLTLoc formula
Notation: \(ac(\phi)\)

Definition: The set of clock regions of \(\phi\)
Page: 177
Variables: \(V\) a set of clock
\(\phi\) a CLTLoc formula
Notation: \(\mathcal R_\phi\)

Definition: Subset of MITL with interval resricted to be \((0,1)\)
Page: 186
Notation: QTL