Automata and Logic in IT System Modelling

5 credits

Syllabus, Bachelor's level, 1DL500

Education cycle
First cycle
Main field(s) of study and in-depth level
Computer Science G1F, Mathematics G1F
Grading system
Pass with distinction, Pass with credit, Pass, Fail
Finalised by
The Faculty Board of Science and Technology, 30 August 2018
Responsible department
Department of Information Technology

Entry requirements

Algebra I and Program Design and Data Structures.

Learning outcomes

On completion of the course, the student should be able to:

  • translate statements and reasoning given in natural language to propositional and predicate logic, explain how predicate logic formulas are interpreted as true or false, and explain the concepts of tautology, valid inference, logical truth and logical consequence
  • describe some mathematical models for calculations such as finite automata, regular and context-free grammars, and how these models are related to each other
  • use automata and logic to model simple systems and define and explain basic correctness properties of models
  • use tools to, in simple cases, determine if a model satisfies a correctness property


The course consists of a theoretical part and a practical part. The theoretical part contains:

Logical expressions, formulation and specification of natural language, logical consistency and equivalence. Regular expressions, context-free and regular grammars, finite automata. System modelling. Interpretation and model. Modal logic.

The practical part contains: Modelling of a small IT system, formulation of correctness properties and analysis of systems with respect to correctness properties.


Lectures, tutorials, labs.


Oral and written assessment of assignments, 3 credits, written examination, 2 credits.

If there are special reasons for doing so, an examiner may make an exception from the method of assessment indicated and allow a student to be assessed by another method. An example of special reasons might be a certificate regarding special pedagogical support from the disability coordinator of the university.