Modal Transition Systems: Extensions and Analysis - Křetínský, Jan, 1984- (2014)
Tato dizertační práce studuje specifikační formalizmus zvaný modální přechodové systémy (MTS). Zavádíme několik rozšíření MTS a rozebíráme jejich vzájemné vztahy a modelovací sílu. Zaprvé rozšiřujeme modality MTS, zadruhé uvažujeme rozšíření s prvky času a ceny a zatřetí zavádíme různé třídy MTS s nekonečně mnoha stavy. Rovněž tato rozšíření MTS srovnáváme jako formalizmy automatové s formalizmy logickými. Těžiště práce se nachází v oblasti algoritmické analýzy a verifikace uvedených systémů. Zajímá nás především kontrola zjemňování, ověřování modelu, obvyklé logické a strukturální operace používané v kontextu specifikačních teorií, automatická tvorba implementací splňujících danou logickou formuli či optimalitu vzhledem k danému cenovému schématu. Věnujeme se jak teroretickým otázkám, zejména složitosti zkoumaných problémů, tak i praktickým aspektům, zejména heuristikám a softwarovému nástroji pro podporu práce s MTS.