Kurset giver en omfattende oversigt over standard og moderne tilgange til ræsonnering om processer i informationssystemer. Disse processer varierer i kompleksitet, fra e-handelsarbejdsgange til sikkerhedskritiske sundhedssystemer. Gennem kurset opnår de studerende dybdegående viden om formelle modelleringsnotationer (baseret på Petri-net og temporale logikker) og relaterede analyseteknikker, efterfulgt af grundige studier af praktiske anvendelser. Derudover får de studerende mulighed for at eksperimentere med forskellige design- og analyseværktøjer til det formalismestudie, der dækkes i kurset, samt udvikle deres egne modellerings- og analyseværktøjer baseret på den viden, de tilegner sig undervejs. En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:

• Forklar syntaks og eksekveringssemantik for flere klasser af Petri-net.
• Forklar syntaks og semantik for flere temporale logikker.
• Forklar, hvordan temporale logikker kan bruges til modellering og specifikation af procesegenskaber.
• Identificér Petri-net-klasser og brug dem til at oprette modeller for et givet scenarie.
• Identificér deklarative formaliser og brug dem til at oprette modeller for et givet scenarie.
• Forklar, hvordan forskellige beregningsmodeller (rækkevidde- og dækbarhedsgrafer) kan genereres fra Petri-net ved hjælp af deres eksekveringssemantik.
• Forklar de algoritmiske aspekter af analyseteknikker, der er blevet studeret i kurset.
• Argumentér formelt for, hvorfor et givet Petri-net eller deklarativ model har visse egenskaber.
• Betjen modellerings- og verifikationsværktøjer og fortolk deres resultater.
• Kobl tilgange og koncepter fra relevant litteratur til dem, der er blevet gennemgået i kurset.
• Opret procesmodelleringsformalismer, definer deres formelle egenskaber og udvikl værktøjsunderstøttelse.

Kurset vil dække følgende emner:
● Klasser af Petri-net og deres udvidelser med data, tid og stokastiske egenskaber. Strukturelle og adfærdsmæssige egenskaber ved disse klasser; afgørelsesresultater for centrale analyseteknikker såsom begrænsning, rækkevidde, dækbarhed og terminering. Verifikation af disse Petri-net-klasser ved hjælp af temporale logikker.

● Grundlag for deklarative procesmodeller baseret på Lineær Temporal Logik på endelige spor og dens førsteordensudvidelser. Analyse af deklarative processer i forbindelse med modeltjek, runtime-verifikation/​overvågning og tilfredsstillelse.

● Softwareværktøjer til analyse og modellering af Petri-net og deklarative processer baseret på temporale logikker. -- Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. Wolfgang
Reisig, 2013 (Springer)

-- Handbook of Model Checking. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem, 2018 (Springer)

-- Process Mining Handbook. Wil M. P. van der Aalst, Josep Carmona, 2022 (Springer)

-- Research papers 02. maj, 2025