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):

- 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

Diskuze

, 2013/06/21 20:43

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é).

You could leave a comment if you were logged in.
mgr-szz/in-tei/15-tei.txt · Poslední úprava: 2014/10/27 09:07 (upraveno mimo DokuWiki)
Nahoru
CC Attribution-Noncommercial-Share Alike 3.0 Unported
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0