Introduction to Formal Specification, Lectures

Having completed the course, the student is able to write simple
specifications using the approaches of the course, can analyze the
properties of the specified system using these specifications, can
animate and simulate a formal specification, and understands some
principles that can be used to implement the specified system.

The course provides a first yet comprehensive introduction to the formal
specification of state-based systems using declarative specification
languages such as linear temporal logic. The course covers basic
concepts related to formal specifications and their application to the
analysis, verification, and implementation of state-based systems. The
first part of the course concentrates on declarative specifications of
relations written down in a logic programming notation. The second part
illustrates the use of temporal specifications in the context of
multi-agent systems, which are ecosystems of interacting intelligent
agents used to solve complex problems arising in artificial
intelligence. The course involves hands-on programming exercises where
logic-based formal specifications are devised.

Common learning events for all

Exercise: Tutorial

28.10.2021 12:00 - 14:00, TAU Pinni B0016 luentosali (41)
04.11.2021 12:00 - 14:00, TAU Pinni B0016 luentosali (41)
11.11.2021 12:00 - 14:00, TAU Pinni B0016 luentosali (41)
18.11.2021 12:00 - 14:00, TAU Pinni B0016 luentosali (41)
25.11.2021 12:00 - 14:00, TAU Pinni B0016 luentosali (41)
02.12.2021 12:00 - 14:00, TAU Pinni B0016 luentosali (41)

Lecture: Lecture 1 / Lecture 2

26.10.2021 12:00 - 14:00, TAU Pinni B1096 auditorio (100)
28.10.2021 10:00 - 12:00, TAU Pinni B1097 auditorio (100)
02.11.2021 12:00 - 14:00, TAU Pinni B1096 auditorio (100)
04.11.2021 10:00 - 12:00, TAU Pinni B1097 auditorio (100)
09.11.2021 12:00 - 14:00, TAU Pinni B1096 auditorio (100)
11.11.2021 10:00 - 12:00, TAU Päätalo D13 auditorio (50)
16.11.2021 12:00 - 14:00, TAU Pinni B1096 auditorio (100)
18.11.2021 10:00 - 12:00, TAU Pinni B1097 auditorio (100)
23.11.2021 12:00 - 14:00, TAU Pinni B1096 auditorio (100)
25.11.2021 10:00 - 12:00, TAU Pinni B1097 auditorio (100)
30.11.2021 12:00 - 14:00, TAU Linna K103 auditorio (113)
02.12.2021 10:00 - 12:00, TAU Pinni B1097 auditorio (100)

Prerequisites

B.Sc. Degree or equivalent studies. Basic knowledge of propositional (Boolean) logic and basic programming skills, preferably, in Python are strongly recommended.

Reading material and on-line exercises at https://plus.tuni.fi

General scale, 0-5