Detail publikace

A Decision Procedure For The WSkS Logic

FIEDOR Tomáš. A Decision Procedure For The WSkS Logic. Saarbrücken: Lambert Academic Publishing, 2014. ISBN 978-3-659-63583-0.
Název česky
Rozhodovací Procedura Pro Logiku WSkS
Typ
odborná monografie
Jazyk
angličtina
Autoři
Fiedor Tomáš, Ing., Ph.D. (UITS FIT VUT)
Abstrakt

Různé typy logik se často používají jako prostředky pro formální specifikaci systémů. Slabá monadická logika druhého řádu s k následníky (WSkS) je jednou z nich a byť má poměrně velkou vyjadřovací sílu, stále je rozhodnutelná. Ačkoliv složitost testování splnitelnosti WSkS formule není ani ve třídě ELEMENTARY, tak existují přístupy založené na deterministických automatech, implementované např. v nástroji MONA, které efektně řeší omezenou třídu praktických příkladů, nicméně nefungují pro jiné. Tato práce rozšiřuje třídu prakticky řešitelných příkladů, a to tak, že využívá nedávno vyvinutých technik pro efektní manipulaci s nedeterministickými automaty (jako je například testování universality jazyka pomocí přístupu založeného na antichainech) a navrhuje novou rozhodovací proceduru pro WSkS využívající právě nedeterministické automaty. Procedura je implementována a ve srovnání s nástrojem MONA dosahuje v některých případech řádově lepších výsledků.

Rok
2014
Strany
60
ISBN
978-3-659-63583-0
Vydavatel
Lambert Academic Publishing
Místo
Saarbrücken, DE
BibTeX 
@BOOK{FITPUB10794,
   author = "Tom\'{a}\v{s} Fiedor",
   title = "A Decision Procedure For The WSkS Logic",
   pages = 60,
   year = 2014,
   location = "Saarbr{\"{u}}cken, DE",
   publisher = "Lambert Academic Publishing",
   ISBN = "978-3-659-63583-0",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10794"
}
Nahoru