Title: Theory / Unimportant / CS / Fundamental / Model Checking / toSort / A decision algorithm for full propositional temporal logic
Tags: hasSeenConjDef
On every note of this deck, unless a note says otherwise:
Chapter: A decision algorithm for full propositional temporal logic

Name: Propositional temporal logic
Definition: The least set containing elements of AP and True, closed under conjonction negation, Next, Until, Previous, Since
Page: 3
Section: 2.1
Variables: \(AP\) a set of atomic propositions
Abbreviation: PTL

Name: A basic formula
Definition: A proposition
Page: 3
Section: 2.1
Variables: \(AP\) a set of atomic propositions
Definition2: True
Conjdef: Either
Definition3: Previous
Definition4: Next

Name: The preconditions of \(p\land q\)
Definition: \(\{p,q\}\)
Page: 3
Section: 2.1
Variables: \(AP\) a set of atomic propositions,
\(p,q\) PTL formulas

Question: The preconditions of \(\neg(p\land q)\)
Answer: \(\{\neg p\}\) and \(\{\neg q\}\)
Page: 3
Chapter: A decision algorithm for full propositional temporal logic
Section: 2.1
Variables: \(AP\) a set of atomic propositions,
\(p,q\) PTL formulas

Name: The preconditions of \(\neg(p\mathcal U q)\)
Definition: \(\{\neg p,\neg q\}\) and \(\{\neg q,\neg\bigcirc(p\mathcal U q)\}\)
Page: 3
Section: 2.1
Variables: \(AP\) a set of atomic propositions,
\(p,q\) PTL formulas

Name: The preconditions of \((p\mathcal U q)\)
Definition: \(\{q\}\) and \(\{p,\bigcirc(p\mathcal U q)\}\)
Page: 3
Section: 2.1
Variables: \(AP\) a set of atomic propositions,
\(p,q\) PTL formulas

Name: The preconditions of \((p\mathcal S q)\)
Definition: \(\{q\}\) and \(\{p,\ominus(p\mathcal Sq)\}\)
Page: 3
Section: 2.1
Variables: \(AP\) a set of atomic propositions,
\(p,q\) PTL formulas

Name: The preconditions of \(\neg(p\mathcal S q)\)
Definition: \(\{\neg p,\neg q\}\) and \(\{\neg q,\neg\ominus(p\mathcal Sq)\}\)
Page: 3
Section: 2.1
Variables: \(AP\) a set of atomic propositions,
\(p,q\) PTL formulas

Name: The preconditions of \(p\)
Page: 3
Section: 2.1
Variables: \(AP\) a set of atomic propositions,
\(p\) a PTL formulas
Notation: \(pre_i\)
Assuming: \(p\) is not basic

Smaller0: \(\bigvee_{i=1}^2\bigwedge_{\psi\in pre_i}\psi\) holds
Greater0: \(p\) holds
Page: 3
Chapter: A decision algorithm for full propositional temporal logic
Section: 2.1
Variables: \(AP\) a set of atomic propositions,
\(p\) a PTL formulas
Smaller to greater: iff
Assuming: \(p\) is not basic

Name: The closure of \(\phi\)
Definition: containing \(first\)
Page: 4
Section: 2.2
Variables: \(AP\) a set of atomic propositions,
\(p\) a PTL formulas
Notation: \(CL(\phi)\)
Definition2: containing \(\phi\)
Conjdef: The smallest set
Definition3: closed under negation
Definition4: closed under removing \(\ominus\) and \(\bigcirc\) in front of formulas,
Definition5: closed under taking the preconditions of a formula

Definition: The subset of formulas of \(CL(\phi)\) beginning about a negation.
Page: 4
Section: 2.2
Variables: \(AP\) a set of atomic propositions,
\(p\) a PTL formulas
Notation: \(CL^-(\phi)\)

Definition: \(CL(\phi)\setminus CL^-(\phi)\)
Page: 4
Section: 2.2
Variables: \(AP\) a set of atomic propositions,
\(p\) a PTL formulas
Notation: \(CL^+(\phi)\)

Name: A \(\phi\)-atom
Definition: \(false\not\in A\),$
Page: 4
Section: 2.2
Variables: \(\phi\) a PTL formula
Definition2: \(\neg p\in A\) implies \(p\not\in A\)
Conjdef: A set of formula such that
Definition3: \(first\in A\) implies \(\ominus p\not\in A\) for any \(p\)
Definition4: \(p\in CL(\phi)\) is non basic, implies \(p\in A\) iff \(pre_i\subseteq A\) for one of the preconditions of \(p\)
Denoted by: \(A\)

Question: The number of \(\phi\)-atom is
Answer: at most \(3^{|CL^+(\phi)|}=3^{1.5|\phi|+2}\)
Page: 4
Chapter: A decision algorithm for full propositional temporal logic
Section: 2.2
Variables: \(\phi\) a PTL formula

Name: \(A\) generalize \(B\)
Definition: \(A\subseteq B\) and
Page: 4
Section: 2.2
Variables: \(\phi\) a PTL formula,
\(A,B\) \(\phi\)-atoms
Notation: \(A\sqsubseteq B\)
Definition2: For every \(p\mathcal Uq\in CL(\phi)\), if \(p\mathcal Uq\in A\) and \(q\in B\), then \(q\in A\)
Conjdef: Both

Name: \(A\) strictly generalize \(B\)
Definition: \(A\sqsubseteq B\) and \(A\ne B\)
Page: 4
Section: 2.2
Variables: \(\phi\) a PTL formula,
\(A,B\) \(\phi\)-atoms
Notation: [$]A\sqsubsetneq B[/$]