===== 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 [[mgr-szz:in-tei:13-tei|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 [[https://is.muni.cz/auth/predmet/fi/IV010|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 [[mgr-szz:in-tei:16-tei|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. --- //[[xvejpust@fi.muni.cz|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

===== Předměty =====
  * [[https://is.muni.cz/auth/predmet/fi/IV010|IV010 Komunikace a paralelismus]]
  * [[https://is.muni.cz/auth/predmet/fi/IA006|IA006 Vybrané kapitoly z teorie automatů]]

~~DISCUSSION~~