CMPT 477/777- Fall 2015
Final exam: THU 17-DEC 15:30-18:30 AQ3153
student card is required
Important: Please check with Student Information System
for room changes
I will be posting my slides on this page, after each class.
The examples that I do in class in interaction with you are NOT in the slides.
We solve them in class together.
PART 0: Model Checking. Introduction
[pdf] my slides on Part 0
PART 1: Propositional logic and SAT
Notes on Propositional Logic and Satisfiability by David Mitchell:
CNF Formulas and Efficient Transformation to CNF. You can skip Version 2 of K-colouring
Linear Time Unit Propagation, Horn-SAT and 2-SAT. Skip sections 3 and 4.
Resolution and Backtracking. Skip sections 2 and 4.
You are required to know all the notes except the sections I said you can skip (above).
If you want to know what the best SAT solvers are,
here is a link to SAT competitions:
The first quiz will be based on Part 1 only.
My slides I used in lectures:
[pdf] Syntax of Propositional Logic, Semantics, satisfiable, valid formulas (tautologies), contradictions.
[pdf] Logical consequence (= logical (tautological) implication,
(= logical (tautological) entailment,
(= semantic entailment)
semantic equivalence, complete (adequate) set of connectives.
[pdf] CNF, Horn satisfiability
[pdf] transformation to CNF
[pdf] Unit propagation
[pdf] SAT
[pdf] Example: Colouring as SAT
[pdf] backtracking and resolution
In this course, we study both SAT-based and BDD-based methods.
The methods are complementary, in some case one is better,
in others the other one.
PART 2: Temporal logics LTL and CTL. Foundations of model checking.
Chapters 3 of Huth an Ryan’s book Logic in Computer Science, 2nd edition
Please google the book, it is online, in [pdf] form.
or you can order it from Amazon
Please note: there is a typo on page 217, in 3.5. Fp --> Fp is expressible
in CTL.. The web site for the book has some other typos as well.
You are required to know all of chapter 3 (and chapter 6 for the last part of the course).
It is VERY IMPORTANT to read the textbook, not just my slides.
My goal is to introduce you to the material, to make your reading
easier. I give you many intuitions, that come from experience, mostly
orally and through examples, but I do not replace the textbook (it does not make sense to me).
I do assume that you read it!
Slides in Part 2 will be posted AFTER the lecture because
our goal in lectures often is to come up with a solution together.
This process is important to achieve understanding of some fundamental issues.
If you want to read ahead, please read the textbook.
[pdf] LTL
[pdf] Mutual Exclusion
[pdf] CTL,CTL*
Please note:. Fp --> Fp is expressible
in CTL..
[pdf] The language of SMV, examples
Synchronous/ Asynchronous composition in SMV,
Fairness Constraints
More Examples (Alternating Bit Protocol)
[pdf] A property not expressible in LTL (with a proof)
Additional explanation why CTL cannot be used to restrict specifications to fair paths,
while LTL can. It was not in the lecture, but I think is a useful additional explanation.
[pdf] Restricting SPECS to fair paths: CTL vs LTL
FIXPOINT characterization of CTL.
[pdf] Basic Labelling Algorithm (BLA)
[pdf] Pseudocode of BLA
[pdf] Monotone Functions, Knaster-Tarski Theorem
[pdf] Correctness of SAT_EG
[pdf] Model Checking with Fairness
PART 3: Symbolic Model Checking: Ordered Binary Decision Diagrams (OBDDs)
Chapter 6 of Huth an Ryan’s book Logic in Computer Science
http://www.eserna.com/Logica/5%20Lectura%202.pdf
(Please search the web for the pdf if this link is not working. It has happened before. The file is online.)
[pdf] Boolean Functions
[pdf] Algorithms for OBDDs
[pdf] Representing sunsets of states and transition relations by boolean functions
[pdf] Mu-calculus
[pdf] Expressing CTL connectives using fixpoints
[pdf] Example
[pdf] Example
[pdf] Example
Final exam: THU 17-DEC 15:30-18:30 AQ3153
student card is required
