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., 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