Introduction to Formal Specification, 5 op

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 modeling exercises where logic-based formal specifications are devised and cross-checked against reference specifications.