Syllabus for Automata and Logic in IT System Modelling

Automater och logik i modellering av IT-system

A revised version of the syllabus is available.

Syllabus

  • 5 credits
  • Course code: 1DL500
  • Education cycle: First cycle
  • Main field(s) of study and in-depth level: Computer Science G1F, Mathematics G1F
  • Grading system: Fail (U), Pass (3), Pass with credit (4), Pass with distinction (5)
  • Established: 2014-03-11
  • Established by: The Faculty Board of Science and Technology
  • Applies from: Autumn 2014
  • Entry requirements:

    Algebra I and Program Design and Data Structures.

  • Responsible department: Department of Information Technology

Learning outcomes

To pass 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

Content

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.

Instruction

Lectures, tutorials, labs.

Assessment

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

Syllabus Revisions

Reading list

Reading list

Applies from: Spring 2014

Some titles may be available electronically through the University library.

  • Baier, Christel.; Katoen, Joost-Pieter. Principles of model checking

    Cambridge, Mass.: The MIT Press, cop. 2008

    Find in the library

Print syllabus and reading list
Last modified: 2022-04-26
Print