Otázka korektnosti je bezpochyby zásadním faktorem při návrhu
počítačových systémů, což dělá z oblasti specifikace a
verifikace důležitou součást informatiky. K tomu, abychom mohli
v této oblasti použít formálních metod, potřebujeme dobrý
specifikační formalismum. Jednou možností je popsat požadované
vlastnosti systému pomocí formulí vhodné logiky. Jinou možností
je přístup založený na chování, při němž se jak specifikace,
tak implementace systému popisují za použití stejného
formalismu a správnost systému se pak ověřuje za použití
jistého druhu ekvivalence či jiné relace. V této práci se
zaměřujeme hlavně na tento přístup, ačkoli i ten dáváme do
souvislosti s přístupem logickým. Modální přechodové systémy
jsou formalismem, který je schopen popisovat specifikace i
implementace. Jeho hlavním přínosem je to, že umožnuje jistou
volnost ve specifikacích, možnost nechat části systému
nedospecifikovány. Toho je dosaženo rozšířením standardních
přechodových systémů o dva druhy přechodů — tzv. must a may
přechody, které popisují požadované, respektive povolené
chování. Tento formalismus podporuje postupně zpřesňování
specifikace a návrh systému založený na komponentách.
Disjunktivní modální přechodové systémy jsou dalším rozšířením,
původně navrženým pro popis řešení jistých procesových rovnic.
Přechody must se zde mění na tzv. hyperpřechody, tj. přechody s
více než jedním cílem, což umožňuje vyjádřit vlastnosti tvaru
„buď — nebo“. V této práci představujeme zobecněnou verzi
těchto přechodových systémů, která zahrnuje řadu předchozích
formalismů. Stejně jako klasické přechodové systémy mohou být
různých druhů — založené na vlastnostech stavů nebo akcí či
jejich kombinací, tak i disjunktivní modální přechodové systémy
se mohou vyskytovat v těchto variantách. Naše zobecněná
definice zahrnuje všechny tyto možnosti. Poté, co představíme
hlavní objekty svého studia, zaměříme se na jisté fundamentální
problémy, které byly již dříve studovány v oblasti modálních
přechodových systémů. Nejprve zkoumáme vztah mezi modálním a
zevrubným zjemněním, což jsou relace popisující postupné
zpřesňování specifikací, první z nich definovaná koinduktivní
způsobem podobným bisimulaci, druhá založená na sémantice. Dále
studujeme problém konzistence dvou typů: zda je daná
specifikace implementovatelná a zda má daná množina specifikací
alespoň jednu společnou implementaci. Poté se věnujeme
zobecněnému ověřování modelu, což je právě kombinace přístupu
logického s přístupem založeným na chování. Popisujeme
teoretickou složitost zkoumaných problémů a nabízíme algoritmy
pro jejich řešení, s přihlédnutím k různým podtřídám
disjunktivních modálních přechodových systémů.