[MSUS | Prednáška] 11 - Workflow siete

Zhrnutie prednášky

Prednáška sa venuje Workflow sieťam ako špeciálnej podtriede Petriho sietí, ktoré majú práve jedno vstupné a jedno výstupné miesto a slúžia na modelovanie udalostných systémov zdieľajúcich zdroje. Vysvetľuje sa formálna definícia korektnosti (soundness) Workflow siete, teda podmienky, že z počiatočného značkovania musí byť vždy dosiahnuteľné jediné značkovanie s jedným tokenom vo výstupnom mieste. Na ilustratívnom príklade výpočtového systému (pridelenie pamäte a procesora úlohe) sa demonštruje korektná sieť a na dvoch protipríkladoch sa ukazujú spôsoby porušenia korektnosti — nedosiahnuteľnosť výstupu alebo existencia viacerých značkovaní s tokenom vo výstupe. Ďalej sa odvodzuje tvrdenie, že korektná Workflow sieť musí byť ohraničená, s náčrtom dôkazu využívajúcim Dicksonovu lemu, čo umožňuje navrhnúť algoritmus na overenie korektnosti pomocou grafu dosiahnuteľnosti.

• - Workflow sieť je Petriho sieť s práve jedným vstupným a jedným výstupným miestom
• - Korektnosť (soundness) vyžaduje dosiahnuteľnosť jediného značkovania s tokenom vo výstupe zo všetkých dosiahnuteľných stavov
• - Nekorektnosť môže vzniknúť buď nedosiahnuteľnosťou výstupného značkovania, alebo existenciou viacerých značkovaní s tokenom vo výstupe
• - Ilustračný príklad: systém prideľujúci pamäť a procesor výpočtovej úlohe
• - Ukázané dva protipríklady nekorektných sietí (uviaznutie a nejednoznačnosť výstupu)
• - Tvrdenie: korektná Workflow sieť musí byť ohraničená, dokázané s využitím Dicksonovej lemy
• - Ohraničenosť umožňuje overiť korektnosť algoritmicky pomocou grafu dosiahnuteľnosti

Zhrnutie pripravené s pomocou AI z prepisu videa.