|
|
Analýza plánovatelnosti úloh reálného času s ohledem na nejistotu
Čus, Samuel ; Šimek, Václav (oponent) ; Strnadel, Josef (vedoucí práce)
Cílem této bakalářské práce je seznámení se se systémy pracujícími v reálném čase, nejistotami a plánovacími mechanismy, souvisejícími s těmito systémy, statistickým ověřováním modelů, dále je to návrh a implementace přístupu k analýze plánovatelnosti s ohledem na nejistoty, vytvoření vhodných sad úloh reálného času a ověření jejich plánovatelnosti. Zaměřil jsem se na nejistoty způsobené přerušením systému a nedeterministickými parametry úloh. Zadaný problém jsem řešil vytvořením sad úloh, zavedením nejistot do systému a analýzou plánovatelnosti úloh. Modelování systému a jeho analýza bylo provedeno v nástroji UPPAAL SMC pro porovnaní také v nástroji Cheddar u vybraných sad úloh.
|
|
|
Hledání řídicích strategií pomocí UPPAAL STRATEGO
Hruška, Filip ; Hrubý, Martin (oponent) ; Strnadel, Josef (vedoucí práce)
Tato práce se zabývá hledáním řídicích strategií v předem vybraných problémech z různých oblastí pomocí nástroje Uppaal Stratego. Byly vybrány čtyři oblasti k řešení, jmenovitě šachy, hanojské věže, posuvné pole a kinematický problém zahrnující balíček, auto a letadlo. Pro zvolené problémy a oblasti byla navržena a vytvořena sada jim odpovídajícím modelů. U hanojských věží a posuvného pole bylo možné úspěšně vyhodnotit relevantní strategie, zvedající pravděpodobnosti úspěchu až na více než 90 %. U dalších modelů byl nalezen problém ve velikosti stavového prostoru a strategie nebylo možné vyhodnotit, protože maximální kapacita paměti, kterou nástroj využívá, nebyla dostatečná. U kinematického problému se po omezení a zjednodušení modelu podařilo strategie vyhodnotit, ovšem u šachů to nebylo možné ani po významném zjednodušení.
|
|
|
Proof Systems: A Study on Form and Complexity
Jalali Keshavarz, Raheleh ; Pudlák, Pavel (vedoucí práce) ; Metcalfe, George (oponent) ; Ramanayake, Revantha (oponent)
Důkazové systémy: forma a složitost Tato disertační práce obsahuje tři části. První dvě části spolu souvisí. V [1] a [2], Iemhoff objevila souvislost mezi existencí terminujícího sekvenčního kalkulu určitého druhu a uniformní interpolační vlastností superintuicioni- stické logiky, kterou tento kalkulus zachycuje. Ve druhé části budeme tento vztah zobecňovat tak, aby pokrýval také substrukturální nastavení na jedné straně a silnější typ systémů nazývaných semi-analytické kalkuly na straně druhé. Abychom byli přesnější, ukážeme, že jakákoli dostatečně silná sub- strukturální logika se semi-analytickým kalkulem má Craigovu interpolační vlastnost a v případě, že je kalkulus terminující, má uniformní interpo- laci. Tento vztah pak vede k některým konkrétním aplikacím. Pozitivním výsledkem je, že poskytuje jednotnou metodu k prokázání uniformní in- terpolační vlastnosti pro logiky FLe, FLew, CFLe, CFLew, IPC, CPC a některá z jejich modálních rozšíření K a KD. Další aplikací je nega- tivní výsledek, že mnohé substrukturální logiky, včetně Ln, Gn, BL, R a RMe , téměř všechny superintuicionistické logiky (kromě nejvýše sedmi z nich) a téměř všechna rozšíření S4 (kromě třiceti sedmi z nich)...
|
|
|
Hledání řídicích strategií pomocí UPPAAL STRATEGO
Hruška, Filip ; Hrubý, Martin (oponent) ; Strnadel, Josef (vedoucí práce)
Tato práce se zabývá hledáním řídicích strategií v předem vybraných problémech z různých oblastí pomocí nástroje Uppaal Stratego. Byly vybrány čtyři oblasti k řešení, jmenovitě šachy, hanojské věže, posuvné pole a kinematický problém zahrnující balíček, auto a letadlo. Pro zvolené problémy a oblasti byla navržena a vytvořena sada jim odpovídajícím modelů. U hanojských věží a posuvného pole bylo možné úspěšně vyhodnotit relevantní strategie, zvedající pravděpodobnosti úspěchu až na více než 90 %. U dalších modelů byl nalezen problém ve velikosti stavového prostoru a strategie nebylo možné vyhodnotit, protože maximální kapacita paměti, kterou nástroj využívá, nebyla dostatečná. U kinematického problému se po omezení a zjednodušení modelu podařilo strategie vyhodnotit, ovšem u šachů to nebylo možné ani po významném zjednodušení.
|
|
|
Možné světy Davida Kelloga Lewise
ŠTORKÁNOVÁ, Radka
Bakalářská práce se zabývá filosofickou teorií možných světů na hranici mezi logikou a metafyzikou. Jako ústřední motiv si klade za cíl představit a kriticky zhodnotit modální realismus amerického filosofa Davida Kelloga Lewise. Nejprve dochází k vymezení toho, co možné světy jsou a jaké mají využití. Východiska lze v tomto případě nalézt již v pre-filozofické intuici týkající se možnosti. V další části se zaměřuje na ústřední body Lewisova chápání možných světů. Jeho velmi originální koncept, zahrnující fakt, že ostatní možné světy existují stejně jako ten náš, sebou ovšem přináší mnohé obtíže. Povaha těchto problémů je diskutována v poslední části.
|
|
| |
|
|
Využití logiky v bezpečnosti IT
Švarný, Petr ; Řepa, Václav (vedoucí práce) ; Mařík, Vladimír (oponent)
Tato práce studuje užití dynamických epistemických logik pro zachování důvěrnosti informací. Základem je syntéza tří přístupů: bezpečnostních logiky A. Hommersoma, hodnověrnostní rámce a komunikační logiky A. Baltaga a S. Smets a studie tzv. Ruského karetního problému. V návaznosti na toto je prezentován také praktický model vytvořený v prostředí NetLogo pro ilustraci funkčnosti základních myšlenek.
|
host ::
RSS.