Elvio G. Amparore is an Assistant Professor (Ricercatore RTD-B) at Computer Science Dep. of the Università degli Studi di Torino. He is a member of the System and Service Quality group, focused on the analysis of performance, reliability, security, scalability, and availability of complex systems. He is also part of the GreatSPN (https://github.com/greatspn/SOURCES) development team, a software package for the modeling, validation, and performance evaluation of distributed systems using Generalized Stochastic Petri Nets and their colored extension, Stochastic Well-formed Nets.

He is a member of the Inf-Q/CINI Working Group on System and Service Quality. His research is currently focused on formal models, performance evaluation, Model Checking techniques, data analysis and explainable machine learning. Moreover, he works on numerical optimization of combinatorial data structures (decision diagrams) used in classical Model Checking, as well as numerical linear algebra optimization for stochastic analysis of Discrete Event Systems, both in collaboration with Iowa State University (IA, USA).

Topics covered:
Model-based validation and evaluation of systems using Stochastic Petri nets (SPN):

• SPN as a stochastic extension of Petri nets with priorities and inhibitor arcs
• model-based evaluation (model construction; qualitative properties; quantitative properties)
• compositional techniques
• coloured Petri nets (specification of systems where multiple components have similar behaviour)
• structural analysis (P- and T-semiflows, bounds, siphons and traps)
• model checking (LTL, CTL and CTL* properties)
• decision diagrams
• Continuous Time Markov Chains (CTMC)
• stochastic logic CSLTA
• non-exponential delays for transitions
• experimentation using the tool GreatSPN

Kamila Barylska received her PhD degree from the Institute of Computer Science Polish Academy of Sciences and works AT the Faculty of Mathematics and Computer Sciences of Nicolaus Copernicus University In Toruń. Her scientific interests include the mathematical foundations of computer science and are focused on the theory of concurrency (mainly related to Petri nets – their analysis and synthesis).

Topics covered:

1. Choice-free nets
1. Implementation
2. Pre-synthesis
3. Proper synthesis
4. Simultaneous proper synthesis
2. Weighted Marked Graphs
3. Marked Graphs
4. Divide and Conquer
1. Products and Sums
2. Articulations
3. Mixed Decomposition

Jörg Desel is a full professor at FernUniversität in Hagen, the leading distance university in Germany. He studied at the University of Bonn and received his doctorate degree from Technical University Munich in 1992 and his Habilitation in 1997 from Humboldt-Universität zu Berlin. His research interest concentrates on theory and application of process modeling languages, with an emphasis on semantics, analysis and synthesis of process models. Jörg Desel (co-)authored or (co-)edited 20 books, published more than 50 peer-reviewed papers in journals or books and has numerous further publications.

Topics covered:
Introduction:

• welcome
• organisational matters
• goal of the Advanced Course
• brief overview of the lectures
• what we offer the participants and what we expect from them

• distributed systems and their behavior
• causality, independence, concurrency
• models of behavior - observation of executions vs. specification of processes
• creation of models
• choices, interfaces, policies
• the role of time

Susanna Donatelli holds a Laurea in Informatica from the University of Torino (1984), a Master in Electrical and Computer Engineering from the University of Massachusetts at Amherst, USA (1987), and a PhD in Computer Science from the University of Torino. Susanna Donatelli has been a researcher at the Computer Science Department of the University of Torino from 1990 to 1997, associate professor from 1998 to 2002 and full professor from 2002 onwards. She has co-authored more than a hundred papers in international journals, international conferences with peer review and contributions in books, as well as the book “Modelling with Generalized Stochastic Petri Nets”, published by John Wiley. Her main research interest is performance evaluation, with special attention to modelling formalisms, solution techniques, measure definition and to the so-called state space explosion problem, common to most formalisms for performance evaluation. Prof. Donatelli’s main contributions to the field are in the area of stochastic Petri net models. Her recent work has focused on stochastic and qualitative verification (model checking) and on the use of symbolic data structures, such as decision diagrams, for different problems, ranging from model checking of Petri nets to the mapping of DNA sequences on a reference genome.

Topics covered:
Model-based validation and evaluation of systems using Stochastic Petri nets (SPN):

• SPN as a stochastic extension of Petri nets with priorities and inhibitor arcs
• model-based evaluation (model construction; qualitative properties; quantitative properties)
• compositional techniques
• coloured Petri nets (specification of systems where multiple components have similar behaviour)
• structural analysis (P- and T-semiflows, bounds, siphons and traps)
• model checking (LTL, CTL and CTL* properties)
• decision diagrams
• Continuous Time Markov Chains (CTMC)
• stochastic logic CSLTA
• non-exponential delays for transitions
• experimentation using the tool GreatSPN

Javier Esparza received his PhD in Computer Science in 1990 on free-choice Petri nets from the University of Zaragoza. He habilitated 1994 at the University of Hildesheim on the subject of Petri net unfoldings. He worked at the Technische Universität München, the University of Edinburgh and the Universität Stuttgart. Since 2007, he holds the chair for Foundations of Software Reliability and Theoretical Computer Science, at the Technische Universität München. His area of interest are among other things: verification of systems, software model checking, program analysis, formal models for distributed systems: Petri nets and process algebras, logic and automata theory.

Topics covered:
Verifying Liveness Properties of Replicated Systems:

• verification of qualitative liveness properties of replicated systems under stochastic scheduling,
• a finite-state program, executed by an unknown number of indistinguishable agents,
• a Presburger stage graph,
• Presburger-definable sets of configurations,
• complexity of the verification problem,
• an incomplete procedure for the construction of Presburger stage graphs,
• the theory of well-quasi-orders,
• the structural theory of Petri nets and vector addition systems,
• a set of benchmarks (population protocols).

Dirk Fahland is an Associate Professor in Process Analytics on Multi-Dimensional Event Data at Eindhoven University of Technology (TU/e). His research area is the analysis and improvement of complex, distributed systems through event data, process mining, and explainable models. Dirk has contributed to research in process management and mining since 2008 in over 80 journal, conference, and workshop publications with foundational results in process modeling, discovery, analysis, and repair. His current research specifically studies cause-effect relations and emergent behavior in networks and dynamic systems as a whole. Insights gained in numerous industrial projects led to the idea of encoding behavioral information in event knowledge graphs, a cornerstone of a new generation of "AI-Augmented BPM Systems".

Jetty Kleijn is a professor of Theoretical Computing Science at the Leiden Institute of Advanced Computer Science (LIACS) of Leiden University, the Netherlands, and a visiting fellow of the School of Computing of Newcastle University, UK. In 2015 she was a visiting professor at the Faculty of Mathematics and Computer Science of Nicolaus Copernicus University, Torun, Poland. She is affiliated with the Theory research cluster and the Bioinformatics cluster of LIACS. Her research areas are the theory of concurrency, bio-inspired computing and the modelling of biological systems, and theory of automata and formal languages. Currently, her research focuses on the modelling of concurrent and distributed systems with understanding and capturing concurrency phenomema in the behaviour of such systems as its underlying aims. Petri nets provide a suitable framework for this research but other models like reaction systems are also considered. Central themes are causality, order structures, formal models inspired by biochemical processes, modeling of biological processes, and composition of and collaboration in multi-component systems. Jetty Kleijn is a member of the Steering Committee for the International Conferences on Application and Theory of Petri Nets and Other Models of Concurrency and Tutorial Chair and moderator of the Petri Net Course at these conferences. She is an associate editor of the LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC) and an editor of the journal Fundamenta Informaticae.

Topics covered:
Petri Nets - local dynamics, occurrence of single transitions sequential semantics:

• firing sequences
• (labelled) transition systems
• behavioural equivalences

• processes
• partial orders
• traces (equivalence classes of firing sequences)

Maciej Koutny is a Professor of Computing Science in the School of Computing at Newcastle University, UK. His research interests centre on the theory of distributed and concurrent systems, including both theoretical aspects of their semantics and application of formal techniques to the modelling, synthesis and verification of such systems. He is the chair of the Steering Committee of the International Conferences on Application and Theory of Petri Nets.

Topics covered:

• Elementary Net Synthesis
• Different Forms of the Synthesis Problem
• General Theory of Net Synthesis
• Synthesis of P/T-Nets
• Synthesis of Nets with the Step Firing Rule

Lars Michael Kristensen is professor of computer science and software engineering at Western Norway University of Applied Sciences (HVL), Campus Bergen. He holds a PhD degree in computer science from the University of Aarhus where he was a member of the Coloured Petri Nets Research Group that developed the CPN modelling language and the supporting CPN Tools. He has been involved in numerous projects on the application of CPN technology in collaboration with industry, including Nokia, Hewlett-Packard, Ericsson, Kongsberg, and Xylem. At HVL he has led the establishment of a PhD programme in computer science, and a master education in applied computer science and engineering. His current research interests are within IoT, embedded systems, cloud computing, and model-driven software engineering for development of smart software systems. He is co-investigator and work package leader in the Smart Ocean Centre for a research-based innovation funder by the Norwegian Research Council, member of the Norwegian Academy of Technological Sciences, and member of several international programme committees within distributed systems and concurrency.

Topics covered:
Coloured Petri Nets for Concurrent Software Systems Engineering:

• Coloured Petri Nets (combining Petri Nets with a functional programming language)
• formal foundation (concurrency, synchronization, communication, and resource sharing)
• sequential computations on data
The theory-tool module:
• syntax and semantics of the CPN modelling language
• editing, simulation, and validation of CPN models
• hierarchical CPNs (support for scalability, abstraction, and maintainability)
• examples of CPN models from recent projects in the domain of smart software systems
• the case-study (constructing and simulating CPN models using CPN Tools)

Sławomir Lasota is a professor at the University of Warsaw. He received his PhD in computer science in 2000 from the University of Warsaw, with which he is affiliated until now: since 2002 as an assistant professor, since 2009 as an associate professor, and since 2019 as a professor. From 2001 to 2002 he was a postdoc in Laboratoire Spécification et Vérification at ENS Cachan (currently ENS Paris-Saclay). In 2004 he was a postdoc in the University of Bordeaux in 2004, and an invited professor in ENS Cachan.

His main research interests are automata theory, concurrency theory and formal verification. His recent research focuses on algorithmic analysis of infinite-state models of computation, such as Petri nets, or register/timed automata.

Topics covered:
The Reachability Problem for Petri Nets:

• Reachability and coverability; relevance and brief history of the problems
• Vector addition systems and counter programs
• Decidability of reachability
• ACKERMANN lower bound for reachability

dr. ir. Xixi Lu is an assistant professor at Utrecht University's Information and Computing Sciences department. She received her Ph.D. and M.Sc. degree in the department of Mathematics and Computer Science at the Eindhoven University of Technology in the Netherlands. The dissertation received the Best Process mining Dissertation award from the IEEE Task Force on Process mining. She was also a postdoctoral researcher at Vrije University Amsterdam. Her research interests are in Process Mining and Process Analytics. In particular, she focuses on methods, approaches, and algorithms to analyze complex event data for understanding the behavior of processes. These approaches have been applied in the healthcare and auditing domains.

Topics covered:
Process Mining (Process Discovery and Event Log Pre-Processing):
Process Discovery:

• the automatic learning of process models using event data
• well-known discovery algorithms (directly-follows-graph miner, inductive miner)
• the event-data preprocessing techniques (creating views, filtering event logs, event abstraction, and label refinements)
• quality and accuracy of the discovered models

• popular process mining tools and libraries.
• hands-on exercises with real-life event data (preprocessing event data and discovering process models effectively).

Łukasz Mikulski is an assistant professor at Nicolaus Copernicus University in Toruń. He received his PhD in computer science in 2012 from the University of Warsaw. He was a postdoc in Polish Academy of Sciences (2012), Newcastle University (2012-2013) and Warsaw University (2019-2020). Since 2011 he has been a visiting researcher at Newcastle University.

His research interests include various methods of modeling, synthesis and analysis of concurrent systems. Among others, they include Petri nets, generalizations of Mazurkiewicz's traces, order invariants, reaction systems or multi-agent systems.

Topics coveres:
Concurrency Paradigms:

• histories and observations

• elementary net systems with inhibitor and mutex arcs
• step traces, subclasses of step traces
• general order structures, maximal and closed relations

• elementary net systems with inhibitors
• interval traces and structures, relationship with Mazurkiewicz traces

Marco Montali is Full Professor in the Faculty of Engineering at the Free University of Bozen-Bolzano, Italy, where he also coordinates the BSc Program in Informatics and Management of Digital Business. The Leitmotiv of his research is to develop novel, foundational and applied techniques grounded in artificial intelligence, formal methods, and data management to create intelligent agents and information systems that combine processes and data. He has served as PC Chair of BPM 2018, RuleML+RR 2019, ICPM 2020, and CBI 2021, as General Chair of ICPM 2022 and EDOC 2022, and is steering committee member of the IEEE task force on process mining. He is co-author of more than 250 papers and recipient of 10 best paper awards and 2 test-of-time awards. He received the 2015 "Marco Somalvico" award, given by the Italian Association of Artificial Intelligence to the best under 35 Italian researcher in artificial intelligence.

Topics covered:
The need of combining static (i.e., data-related) and dynamic (i.e., process-related) aspects has been increasingly recognized as a key milestone towards the design, verification, and understanding of business and work processes.
Models for data-aware processes:

• formal modeling and analysis
• the usage of bounded Petri nets to account for the process control-flow
• possibility to handle verification tasks such as soundness and temporal model checking

Laure Petrucci has been a full professor since 2003 at the Networks and Telecommunications department of the Technology Institute of Villetaneuse, Université Paris 13. She also is a member of the LoVe (Logics and Verification) group of the Computer Science Laboratory of Paris North (LIPN). Her area of expertise is formal specification and verification of concurrent systems so as to guarantee their appropriate behaviour, using automata or Petri nets models, as well as parametric models. In order to tackle the well-known state space explosion problem, the research she develops exploits modularity in the models, proposes distributed approaches, and algorithms for parameter synthesis.

Topics covered:
Part 1: Timed models

• Timed Automata
• Time(d) Petri Nets syntax and concrete semantics
• region graph (symbolic semantics)

• LTL and CTL
• Adding time: TCTL
• Adding Strategies: TATL, STCTL

• Exploration strategies:
• BFS, DFS, ID

• adding temporal parameters
• tools: Imitator, Romeo

Wolfgang Reisig is a professor emeritus at the Informatics Institute of Humboldt-Universitaet zu Berlin, Germany. After his PhD at RWTH Aachen in 1979 on a topic about Petri nets, he joined the group of Carl Adam Petri at the research institution Gesellschaft fuer Mathematik und Datenverarbeitung (GMD), and later served as a professor at Technical University of Munich, from where he moved to Berlin.

Prof. Reisig was a senior research at the International Computer Science Institute (ICSI) in Berkeley, California in 1997, got the "Lady Davis Visiting Professorship" at the Technion, Haifa (Israel), the Beta Chair of Technical University of Eindhoven, and twice received an IBM Faculty Award for his contribution to Cross-organizational Business Processes and the Analysis of Service Models. He has been the speaker of a PhD school on Service Oriented Architectures, 2010 - 2017. Prof. Reisig is a member of a member of the European Academy of Sciences, Academia Europaea.

Prof. Reisig published and edited numerous books and articles on Petri Net Theory and Their Applications. He organized the Advanced Courses on Petri nets in Bad Honnef and in Dagstuhl. Presently, he develops the Petri net based modeling infrastructure HERAKLIT.

Topics covered:
Starting with C.A. Petri‘s seminal thesis in 1962, Petri nets challenge some assumptions about fundamentals of discrete behavior modeling in informatics:

• Petri nests emphasize that cause and effect of an event is locally confined. This yields a lot of insight into the nature of single behaviors of a system, and allows for specific classes of nets and analysis techniques;
• Petri nets base the notion of state on concepts of propositional and first order logic, and can be conceived as a dynamization of logic;
• Petri nets can be composed in a way that avoids the state explosion problem of automata, process algebras and many other modeling techniques.

Natalia Sidorova is an Assistant Professor at the Process analytics group of Eindhoven University of Technology, and she is a member of Eindhoven Artificial Intelligence Systems Institute. She received her Ph.D. in computer science from Yaroslavl State University, Russia in 1998, where she started working on system analysis and verification using Petri nets. Her current research interests include algorithms and techniques for process analytics using data-driven approaches. Next to theoretical contributions, Natalia has collaborated with industry partners to apply process mining and conformance checking techniques to real-world scenarios.

Topics covered:
Conformance checking (theory and tool):

• Introduction to Conformance Checking: importance, goals, and challenges.
• Types of conformance checking: replay-based, alignment-based, and model-based techniques.
• Evaluation metrics for conformance checking.
• Multi-perspective conformance checking: resource, data, and control-flow perspectives.
• Interpreting deviations in control-flow, resource and data perspectives.
• Hands-on exercises using ProM.
• Conformance checking on real-world event and discussion and analysis of the results obtained.
• Open research challenges in conformance checking.

Karsten Wolf received his PhD from Humboldt-Universität zu Berlin in 1996. He worked there as a researcher until 2005, with temporary visits (8 to 12 months) to Helsinki University of Technology, to Technical University Dresden, and to Carnegie Mellon University in Pittsburgh. Starting in 2006, he is a professor for theoretical computer science at Rostock University in Germany.

His main research field is Petri net model checking. He is the main author of the Petri net verification tool LoLA.

Topics covered:
The verification of Petri nets in a hands-on session:

• Petri net models and queries from the Model Checking Contest
• the performance of several verification techniques
• interplay of general state space reduction methods and Petri net theory
• stubborn set methods,
• symmetries,
• the state equation and Petri net invariants,
• siphons and traps,
• net reduction,
• formula rewriting.

Alex Yakovlev (FIEEE, FIET) received his Ph.D. degree from St. Petersburg Electrical Engineering Institute, in 1982. Since 1991 he is with Newcastle University where he is a Professor of Computer Systems Design, founded and leads the Microsystems Research Group, and co-founded the Asynchronous Systems Laboratory. He was awarded an EPSRC Dream Fellowship in 2011–2013. He has published 8 edited and co-authored monographs and more than 500 papers in IEEE/ACM journals and conferences, in the areas of concurrent and asynchronous circuits and systems, Petri nets, electronic design automation, low power circuits and systems, AI and machine learning hardware based on Tsetlin automata and electromagnetic computing, with several best paper awards and nominations. He co-invented Signal Transition Graphs (STGs) and co-led developments of tools for them (Petrify, Workcraft) throughout the last 30 years. He has chaired organizational committees of major international conferences, including ICATPN 2001, ACSD 2001, and ASYNC 2008. He has been principal investigator on more than 30 research grants and supervised over 60 PhD students. He is a Fellow of Royal Academy of Engineering in the United Kingdom and Fellow of IEEE.

Topics covered:
Day 1: Theory and Tools in Workcraft

• Slots 1 and 2: Fundamental principles of asynchronous design, models and tools
• Slot 3: Introductory practical in Workcraft (Petri net models, Signal Transition Graphs - STGs, Design of C-element)
• Slot 4: Logic Synthesis from STGs (Design of basic VME bus controller)

• Slot 1: State encoding
• Slot 2: Logic decomposition
• Slot 3: Hierarchical design and verification
• Slot 4: Case study: Design of DC/DC buck controller