Title: Theory / Unimportant / CS / Fundamental / Model Checking / Temporal logic of Reactive and Concurrent Systems / Temporal logic

Definition: \((\sigma,j-1)\models\phi\) and \(j>0\)
Page: 193
Chapter: 3
Variables: \(AP\) a set of atomic propositionsLet \(p,q\) a PTL formula,
\(\sigma\) an interpretation
\(j\in\mathbb N\)
Notation: [$](\sigma,j)\models\bigominus\phi[/$]

Name: \(p\) since \(q\)
Page: 194
Chapter: 3
Variables: \(AP\) a set of atomic propositions
\(p,q\) a PTL formula,
Notation: \(p\mathcal Sq\)

Name: A valid property of \(P\)
Definition: A property which is true of all computations generated by \(P\)
Page: 180
Chapter: 3
Variables: \(P\) a program

Name: A program which implements the specification \(p\)
Definition: A program whose every computations satisfy \(p\)
Page: 180
Chapter: 3
Variables: \(p\) a specification
Name2: A program which satisfies \(p\)

Name: once \(p\)
Page: 193
Chapter: 3
Variables: \(AP\) a set of atomic propositions
\(p\) a PTL formula,
Notation: \(p\)
Name2: always in the past \(p\)

Name: \(\phi\) back to \(\psi\)
Definition: \(\phi\mathcal S\psi\lor\boxminus\phi\)
Page: 194
Chapter: 3
Variables: \(AP\) a set of atomic propositions
\(\phi,\psi\) a PTL formula,
Notation: \(\phi\mathcal B\psi\)

Definition: \((\sigma,k)\models p\) for all \(0\le k\le j\)
Page: 193
Chapter: 3
Variables: \(AP\) a set of atomic propositionsLet \(p\) a PTL formula,
\(\sigma\) an interpretation
\(j\in\mathbb N\)
Notation: \((\sigma,j)\models\boxminus p\)

Definition: \((\sigma,j)\models p\mathcal Sq\) or \((\sigma,j)\models\boxminus p\)
Page: 194
Chapter: 3
Variables: \(AP\) a set of atomic propositionsLet \(p,q\) a PTL formula,
\(\sigma\) an interpretation
\(j\in\mathbb N\)
Notation: \((\sigma,j)\models p\mathcal Bq\)

Definition: \((\sigma,k)\models p\) for some \(0\le k\le j\)
Page: 193
Chapter: 3
Variables: \(AP\) a set of atomic propositions\(p\) a PTL formula,
\(\sigma\) an interpretation
\(j\in\mathbb N\)
Notation: \((\sigma,j)\models\diamond p\) (with a minus in diamond)

Definition: There exists \(0\le k\le j\) such that \((\sigma,k)\models q\) and \((\sigma,i)\models p\) for each \(k<i\le j\).
Page: 194
Chapter: 3
Variables: \(AP\) a set of atomic propositions
\(p,q\) a PTL formula,
\(\sigma\) an interpretation
\(j\in\mathbb N\)
Notation: \((\sigma,j)\models p\mathcal Sq\)

Name: Previous \(p\)
Page: 193, 174 A tool for deciding the satisfiability of continuous-time metric temporal logic
Chapter: 3
Variables: \(AP\) a set of atomic propositions
Let \(p,q\) a PTL formula
Notation: [$]\bigominus p[/$]
Notation2: \(\mathbf Yp\)

Name: has always been \(p\)
Definition: \(p\)
Page: 193, 27
Chapter: 3, 2
Section: 3, 1 Cheking timed and hybrid properties: theory and applications
Variables: \(AP\) a set of atomic propositions
\(p\) a PTL formula,
Notation: \(\boxminus p\)
Name2: always in the past \(p\)
Name3: Historically \(p\)

Definition: \(\neg\ominus T\)
Page: 195
Chapter: 3
Notation: first

Name: A past formula
Page: 198
Chapter: 3
Notation: A formula without future operators

Name: A future formula
Page: 198
Chapter: 3
Notation: A formula without past operators

Name: Weak previous
Definition: \(\neg\ominus\neg\)
Page: 198
Chapter: 3
Notation: \(\tilde{\ominus}\)
Intuition: either yesterday it holds. Or it is the first time

Name: The immediate operators
Definition: \(\tilde{\ominus}\), \(\ominus\) and \(\circ\)
Page: 199
Chapter: 3

Name: The nonimmediate operators
Definition: The operators which are not immediate.
Page: 199
Chapter: 3

Definition: \(\circ\triangle\)
Page: 200
Chapter: 3
Variables: \(\triangle\) being a future operator
Notation: \(\hat\triangle\)

Definition: \(\ominus\triangle\)
Page: 200
Chapter: 3
Variables: \(\triangle\) being a past operator
Notation: \(\hat\triangle\)