Distributed state space reductions - Moravec, Pavel, 1979- (2008)
Fundamentální problém formální verifikace, takzvaný problém stavové exploze, již byl řešen mnoha způsoby. Dvě skupiny přístupů jsou redukce stavových prostorů a použití paralelních nebo distribuovaných algoritmů. Zatímco se techniky v první skupině snaží zmenšit objem nutně vykonané práce (bezpečným zmenšením odpovídajících stavových prostorů), techniky z druhé skupiny používají k řešení daného problému více zdrojů (počítačů ap.). Přestože jsou techniky z uvedených skupin často komplementární, kombinaci metod z první a druhé skupiny bylo zatím věnováno pouze málo pozornosti. Důvodem může být to, že používání redukcí stavových prostorů často zahrnuje řešení problémů které lze jen obtížně řešit paralelně. Předkládaná disertační práce se proto zaměřuje na kombinaci redukčních technik a verifikace v distribuovaném prostředí. Jmenovitě navrhuje efektivní distribuované algoritmy pro generování redukovaných stavových prostorů. Práce se zabývá třemi redukcemi: partial order reduction (redukce .