Required in stage
Optional in stage
First term
Second term
Both terms
Not organised
This year
Next year
Alternating years
External
Prerequisites
Taught by
Language of instruction
Duration
Identical coursesModelling of Complex Systems (B-KUL-H0N05A)
Cannot be taken as part of an examination contractAims
The students are familiarized with a number of basic logics and formal systems to model complex systems. They understand for which type of propositions these languages are suitable and are capable of expressing relevant properties in these languages and to use these to solve certain types of tasks and problems, including verification tasks by means of suitable forms of inference. They should be able to motivate the choice for the formal system or the form of inference. Global advantages and disadvantages of the techniques are known and have to be used in this choice. The connections and differences between the different languages are understood.
Students are capable of recognizing the relevant concepts in a problem domain and to design a logical vocabulary for them. They can distinguish not only explicit but also implicit information in a problem setting and can express both types of information in the logics of this course, or they can evaluate whether these logics are suitable for expressing these. They can analyze tasks and problems and classify them as formal logic inference tasks. They are capable of specifying these inference tasks in a concrete way and let them solve by a suitable inference tool.
The students are familiar with a number of static information concepts such as
enumeration, sufficient and necessary conditions, inductive definitions, unique name propositions, domain closure propositions. They are familiar with information concepts in the context of dynamic systems such as inertia, pre- and postconditions, state formulas and invariants, causal rules, and with process properties including fairness, deadlock, aliveness, reachability. They have an understanding of modelling at different levels of abstraction and of the refinement principle to connect these different levels of abstraction.
The students are also familiar with fundamental logical concepts such as model semantics, logical entailment, satisfiability, logical equivalence, contradiction. They know fundamental results and what they mean, such as the incompleteness theorem of Goedel, expressiveness limitations and the undecidability of classical logic and extensions. For certain of these properties they can formulate the proof.
The students are able to understand proof principles for proving or disproving invariants, refinement statements, and process properties.
The students understand a number of fundamental inference algorithms and can describe and apply these, and explain their complexity.
The different topics and used systems are close to current research. In the course, many links are laid between different research fields in formal methods and artificial intelligence and we frequently hit unsolved research questions.
Previous knowledge
Preliminary knowledge of logics or formal systems is not required since the study material is introduced from the ground up. It is important to have a base level of mathematical maturity. This is the level required for the mathematically oriented courses in the bachelor of Informatics and Engineering at the KU Leuven. In the bachelor of Informatics, these courses are: Logica voor Informatici, Beginselen van Programmeren, Fundamenten voor de Informatica, Object-gericht programmeren, Artificiele Intelligentie, Automaten en Berekenbaarheid.
Identical courses
This course is identical to the following courses:
G0B23A : Modellering van complexe systemen
Is included in these courses of study
Activities
3.5 ects. Modelling of Complex Systems (B-KUL-H0N05a)
Content
The content of this course is originally based on the book Logic in Computer Science by Michael Huth and Mark Ryan, and was extended with additional materials, e.g., about modelling and problem solving using predicate logic, techniques from knowledge representation and articificial intelligence, and specification and verification in Event-B, CTL and LTL with abstraction and refinement. The book contains many exercises. The auteurs have a website with for each chapter a number of multiple choice questions with feedback for each choosen answer. The book deals with certain topics in deeper way than is intended. In particular, the chapters on modal logic and OBDD's can be skipped without a problem. Other aspects are dealt with in more depth in the course than in the book. Also the connections between the different topics and chapters are investigated more thoroughly in the course than in the book.
The course consists of the following chapters:
0. Introduction
- What is modelling?
- About the role of knowledge representation and formal methods in computer science
- Motivation for this course
1. Propositional logic
- Syntax, semantics
- Normalisation to CNF
- SAT algorithms
2. Predicate logic
- Syntax, semantics
- Undecidability of deduction
- Expressiveness
- Extensions of predicate logic
- Problem solving through logic inference systems
+ database model checking and query answering inference as model checking
+ model generation, model revision
+ theorem proving/deduction
- Algorithms for grounding
3. Modelling of dynamic systems
- The frame problem
- Temporal formalisms: Linear Time Calculus (LTC), Event-B
- Inference methods for Verification and problem solving for dynamic systems
- Modelling on different levels of abstraction and the refinement principle.
- Verification in the context of refinement
4. Verification by model checking
- Motivation for verification
- Temporal logics
* linear time temporal logics (LTL): syntax, semantics, specification patterns, important equivalences, connectives, links with LTC (Linear Time Calculus)
* Branching-time temporal logic (CTL): syntax, semantics, specification patterns, important equivalences, connectives
* Comparison LTL and CTL
- Model checking
* model checking in CTL
* SAT-solvers for model checking
* model checking in LTL using automata-theoretic techniques
Course material
- Course
- Transparencies: are complete and contain all information that is supposed to be known on the exam
- The book "Logic in Computer Science" by Michael Huth and Mark Ryan: is used as support of course. There is an overlap of approximately 40%. The book is closely followed in the chapters on modelchecking with LTL and CTL
- Didactic tools:
- IDP for inference problems in predicate logic extensions
- ProB for Event-B and for verification with CTL and LTL on dynamic worlds
http://www.stups.uni-duesseldorf.de/ProB/index.php5/LTL_Model_Checking - Rodin for building Event-B specifications of dynamic systems using refinement, and verification of invariants
The course, transparencies, project assignments, exercises, home works and a discussion forum to discuss the course is made available on Toledo.
1.5 ects. Modelling of Complex Systems: Exercises (B-KUL-H0N06a)
Content
Exercises consists of standard exercise sessions of 2h30 in which all important aspects of the course are trained. Most of these sessions are on computer using the systems IDP, ProB, Rodin that are the didactic tools of this course.
Format: more information
Standard exercise sessions where students receive a number of questions and solve them with support of the assistant.
1 ects. Modelling of Complex Systems: Project (B-KUL-H0N07a)
Content
The project consists of building specifications of a dynamic application using predicate logic, Event-B, CTL and LTL, and refinement and performing problem solving and verifications on these specifications using the systems IDP, ProB and Rodin.
Evaluation
Evaluation: Modelling of Complex Systems (B-KUL-H2N05a)
Explanation
The exam consists of a theory part and an exercise part.
- The theory part is closed book. The student should pass for this part of the exam.
- The exercise part is open book. The student may bring the course and slides.
The total score of the course is computed from the scores of the exam and the project, with a maximum of 9/20 if the student fails the theory part. A score less than 10/20 is rounded down, a score more than 10/20 is rounded to the closest integer.