Formal Aspects of Process Science

• Explain the syntax and execution semantics of several Petri net classes.
• Explain syntax and semantics of several temporal logics.
• Explain how temporal logics can be used for modelling and specifying properties of processes.
• Identify Petri net classes and use them to create models for a given scenario.
• Identify declarative formalisms and use them to create models for a given scenario.
• Explain how different computational models (reachability and coverability graphs) can be generated from Petri nets using their execution semantics.
• Explain algorithmic aspects of analysis tasks studied during the course.
• Argue formally why a given Petri net or declarative model has certain properties.
• Operate modelling and verification tools and interpret their results.
• Link approaches and concepts from the relevant literature to the ones seen in the course.
• Create process modelling formalisms, define their formal properties and provide tool support.

The course will cover the following topics:
● Classes of Petri nets and their data/time/stochastic extensions. Structural and behavioural properties of such classes; decidability results for main analysis tasks such as boundedness, reachability, cover ability and termination. Verification of the said classes of Petri nets using temporal logics.

●Foundations of declarative process models based on Linear Temporal Logic on finite traces and its first-order extensions. Analysis of declarative processes in the context of model checking, runtime verification/monitoring and satisfiability.

● Software tools for analysis and modelling of Petri nets and declarative processes based on
temporal logics.

• 36 – 49 (Mon 8-12)

02141, The students are expected to be familiar with finite automata and/or transition systems. The students must be able to write programs in a programming language.

Lectures, theoretical exercises, and practical exercises.