Zadání
15. Současné metody specifikace a analýzy souběžných procesů
Vypracování
Na tuto otázku nemám čas, ale protože se nikdo nehlásí, navrhuju následující postup. Pokud má někdo ještě další nápady, doplňte je, prosím.
Jedna z možností je charakterizovat procesy jako Petriho sítě. Tomu se věnuje samostatná otázka.
Druhá možnost je chtít použít model checking nebo equivalence checking (který je založený na bisimulaci). V tom případě potřebuju explicitně nebo implicitně definovaný stavový prostor, konkrétně Labelled Transition System. K jeho specifikaci se pak dají použít různé formalismy, například CCS (Calculus of Communicating Systems), kterému se věnuje předmět IV010 Komunikace a paralelismus (včetně různých variant bisimulace) a materiály k němu by měly poskytnout dostatečný předmět. Model checking je zpracovaný v samostatné otázce.
Poznamky z IV010 Komunikace a paralelismus - zacal jsem prvni prednaskou a od druhe premyslim, jestli to ma vubec cenu jednu po jedne prepisovat, protoze ty slidy jsou pomerne strohe a prijde mi, ze bych to bral skoro 1:1, pridal jsem aspon nejaky zakladni prehled, co se v jednotlivych slidech objevuje
CCS (Calculus of Communicating Systems)
- Prvky systemu budeme nazyvat procesy (agenty)
- Proces = system, jehoz chovani je tvoreno diskretnimi akcemi.
- Akce je bud interakci s jinym procesem - komunikaci nebo probiha nezavisle na jinych procesech a muze tedy probihat paralelne s jinymi akcemi jinych procesu
- kazda akce je komunikace (CCS)
- Chovani systemu - schopnost komunikovat
Komunikace
- vysilac, prijmac, medium - pres zpravy
- medium - eter, omezeny eter, buffer, omezeny buffer, sdilena pamet
- handshake - vzajemna komunikace probihajici soucasne
- typy komunikace: s vnejsim prostredim, mezi komponentami (procesy) a uvnitr procesu
Procesy
- pametova bunka
- bufer
- dvoucestny bufer
Operace
- prefix
- sumace
- paralelni kompozice
- restrikce
- prejmenovani
- definice
Syntax a semantika
- nekonecna mnozina jmen a ko-jmen
- navesti - porty
- provedeni akce - zmena stavu
- prechody
- prechodovy strom
- nekonecny strom se opakuje → mozna reprezentace prechodovym grafem
- prechodovy system s navestimi
- odvozovaci pravidla
Silna bisimulace
- Ekvivalence - moznost odlisovat ci ztotoznovat procesy
- jazykova ekvivalence
- komunikacni ekvivalence
- komunikacni hra 2 hracu
- Silna bisimulace
- Ekvivalence v relaci silne bisimulace
- Charakteristika silne bisimulace (od slide 12 lekce 4 dal)
- funkce monotonni, pevny bod
- algebraicke zakony:
- staticke
- dynamicke
- expanzni
- kongruence
- rekurzivni definice silne bisimulace
Slaba bisimulace
- definice
- planovac
Priklady
- dynamicka zmena struktury systemu
- citac
- zasobnik
- ABP
Bisimulacni kongruence
- definice
- jednoznacnost reseni rekurzivnich rovnic
- axiomatizace konecnych procesu
- axiomatizace konecne-stavovych procesu
Rozsireni CCS
- stopove (jazykove) ekvivalentni procesy
- jazykova ekvivalence
- selhani
- dalsi operatory
- sekvencni kompozice
- preruseni
- garbage collection
Temp. vlastnosti procesu
- Hennessy-Milnerova logika
- deadlock-free procesy
- modalni mu-kalkul
Taky nemusí být od věci přečíst si něco o Process Rewrite Systems. — Tomáš Vejpustek 2013/06/20 19:34
Ďalšie nápadady - z predmetu IA006 (Automaty II):
- BPA - Basic Process Algebra - http://www.fi.muni.cz/usr/kretinsky/nBPA_LICS91.pdf
- Gramatiky ako popis aj paralélnych procesov - http://www.fi.muni.cz/usr/kretinsky/prs.pdf - to budu asi tie Process Rewrite Systems
- uvedené odkazy sú odkazy na materiály použité k výuke predmetu IA006, pravdepodobne nájdete aj niekde čosi ďalšie
Diskuze
Jo, ten druhý materiál (http://www.fi.muni.cz/usr/kretinsky/prs.pdf) se týká Process Rewrite Systems. Úplně jsem zapomněl, že se něco takového v pokročilých automatech dělalo (ale ty brýle jsou mi povědomé).