Detail publikace

A Decision Procedure For The WSkS Logic

FIEDOR, T. A Decision Procedure For The WSkS Logic. Saarbrücken: Lambert Academic Publishing, 2014. 60 p. ISBN: 978-3-659-63583-0.
Název česky
Rozhodovací Procedura Pro Logiku WSkS
Typ
kniha odborná
Jazyk
anglicky
Autoři
Fiedor Tomáš, Ing., Ph.D. (VZ VERIFIT)
Klíčová slova

antichainsWSkSfinite automatatree automatanondeterministic automata

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
BibTeX 
@book{BUT111679,
  author="Tomáš {Fiedor}",
  title="A Decision Procedure For The WSkS Logic",
  year="2014",
  publisher="Lambert Academic Publishing",
  address="Saarbrücken",
  pages="60",
  isbn="978-3-659-63583-0"
}
Nahoru