| Week |
Topic |
Wednesday (14:00:-15:30) |
Thursday (15:45-19:00) |
| 1:Oct 01-02 |
FOL and CQs |
Lectures 1-2
- Introduction to the course
- First-order logic
|
Lectures 3-6
- Open and closed formulas
- Logical implication
- Evaluation of a formula
|
| 2:Oct 8-9 |
FOL and CQs |
Lectures
7-8
- Time cost of evaluation
- Space cost of evaluation
- Combined complexity, Data complexity, Query complexity
| Cancelled
|
| 3:Oct 15-16 |
FOL and CQs |
Lectures 9-10
- Theory of conjunctive queries (CQs)
- NP completeness of CQs evaluation
- Homomorphism
- Chandra-Merlin Theorem on CQ evaluation
|
Lectures 11-14
- Query containment
- Chandra-Merlin Theorem on CQ query containment
- Execises on CQs and FOL
|
| 4:Oct 22-23 |
Formalizing UML Class Diagrams |
Lectures 15-16
- Incomplete databases
- Certain answers
- CQs in incomplete databases
- UML class diagrams
- Fomalization in FOL
|
Lectures 17-20
- UML class diagrams
- Fomalization in FOL
- Fomalization of classes
- Formalization of Attributes
- Formalization of Associations
- Mutiplicity constraints
|
| 5:Oct 29-30 |
Formalizing UML Class Diagrams |
Lectures 21-22
- Automated reasoning on UML class diagrams
- Complexity of reasoning on UML class diagrams |
Lectures 23-24
(Lesson starts at 17:15)
- Instantiations of UML class diagrams without ISAs
- Query instantiation of UML class diagram with ISAs
- Instantiations of UML class diagrams with ISAs
|
| 6:Nov 5-6 |
Query Answering through UML Class Diagrams |
Lectures 25-26
- Chase and saturation of intantiations
- Query instantiation of UML class diagram with ISAs
- Structural operational semantics
|
Cancelled
|
| 7:Nov 12-13 |
Semantics of programs |
Lectures 27-28
- Structural operational semantics
- Evaluation semantics
-
Transition semantics
- Concurrency |
Lectures 29-32
-
Hoare Logic
-
Weakest preconditions
- Invariants
- Variants |
| 8:Nov 19-20 |
Fixpoint theory |
Lectures 33-34
- Fixpoints
- Least and greatest fixpoints
- Knaster-Tarski theorem
- Approximates of least-fixpoint
- Approximates of greatest-fixpoint
- Approximates theorem |
Lectures 35-38
- Least and greatest fixpoints
- Approximates of least-fixpoint
and greatest-fixpoint
- Transition Systems
- Mu-calculus
|
| 9:Nov 26-27 |
Model checking |
Cancelled
|
Cancelled
|
| 10:Dec 03-04 |
Model checking |
Lectures 39-40
- Mu-calculus
- Properties of mu-calculus
- Evaluating mu-calculus formulas over transition systems: model checking
|
Lectures 41-44
- Introduction to model checking
- Transition systems
-
Temporal logics: LTL, CTL e CTL*
|
| 11:Dec 10-11 |
Model checking |
Lectures 45-46
- Linear time framework
- Linear time logic (LTL)
- Properties of LTL
- Expressing safeness, liveness and fainess properties in LTL |
Lectures 47-50
- Branching time framework
-
Computational Tree Logic (CTL)
-
Properties of CTL
- Expressing safeness, liveness and fairness properties in CTL
- Translation of CTL formulas into mu-calculus
-
Model checking in CTL via mu-calclulus modelchecking
- LTL, CTL are uncomparable from the point of view of expressiveness
-CTL*
|
| 12:Dec 17-18 |
Question time and exam exercises |
Lectures 51-52
- Model checking in the linear time framework
- Transition systems runs as infinite strings
- Buchi Automata on infinite strings
- LTL model checking as nonemptiness of Buchi automata
|
Lectures 53-56
-
Exam exercises
|