Detail výsledku

Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing

HOLÍK, L.; VOJNAR, T.; CHEN, Y.; MAYR, R.; HONG, C.; ABDULLA, P.; CLEMENTE, L. Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. FIT-TR-2010-02, Brno: Faculty of Information Technology BUT, 2010. 30 p.
Typ
zpráva odborná
Jazyk
anglicky
Autoři
Holík Lukáš, doc. Mgr., Ph.D., FIT (FIT), UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Chen Yu-Fang
Mayr Richard
Hong Chih-Duo
Abdulla Parosh
Clemente Lorenzo
Abstrakt

There are two main classes of methods for checking universality
and language inclusion of Büchi-automata: Rank-based methods
and Ramsey-based methods. While rank-based methods have a better
worst-case complexity, Ramsey-based methods have been shown to be
quite competitive in practice. Previously, it was also shown (for universality checking) that a simple subsumption technique, which avoids exploration of certain cases, greatly improves the performance of the Ramsey-based method. Here, we present a much more general subsumption technique for the Ramsey-based method, which is based on using simulation preorder on the states of the Büchi-automata. This technique applies to both universality and inclusion checking, yielding a substantial performance gain over the previously known simple subsumption approach.

Klíčová slova

Büchi automata, universality, language inclusion, Ramsey-based methods, simulation subsumption

URL
Anotace

Existují dva základní přístupy k testování univerzality a jazykové inkluze Büchiho automatů. Tak zvané Ramseyho metody a metody využívající alternující automaty. V tomto článku rozvíjíme Ramseyho metodu, kterou obohacujeme o využití principu simulačního pokrytí. Jak dokazují naše experimenty, dosáhli jsme tak výrazného zvýšení efektivity Ramseyho metody.

Rok
2010
Strany
30
Vydavatel
Faculty of Information Technology BUT
Místo
FIT-TR-2010-02, Brno
BibTeX 
@misc{BUT192678,
  author="Lukáš {Holík} and Tomáš {Vojnar} and Yu-Fang {Chen} and Richard {Mayr} and Chih-Duo {Hong} and Parosh {Abdulla} and Lorenzo {Clemente}",
  title="Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing",
  year="2010",
  pages="30",
  publisher="Faculty of Information Technology BUT",
  address="FIT-TR-2010-02, Brno",
  url="http://www.fit.vutbr.cz/~holik/pub/FIT-TR-2010-002.pdf"
}
Projekty
Bezpečné, spolehlivé a adaptivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-10-1, zahájení: 2010-03-01, ukončení: 2010-12-31, ukončen
Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů, GAČR, Doktorské granty, GD102/09/H042, zahájení: 2009-01-30, ukončení: 2012-12-31, ukončen
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit, MŠMT, COST, OC10009, zahájení: 2010-01-01, ukončení: 2012-12-31, řešení
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru