The topic of the lecture is the verification of concurrent systems. We will study automata models for these systems (e.g Petri nets, WSTS, and distributed automata) and show how algorithmic problems for these models can be solved.
We plan to cover the following topics in detail:
- Petri nets: Reachability and coverability
- Well-structured transition systems
- Distributed automata
- Multi-pushdown automata
- TSO - A weak memory model for x86