15. Současné metody specifikace a analýzy souběžných procesů

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

• 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

• IV010 Komunikace a paralelismus
• IA006 Vybrané kapitoly z teorie automatů