BABIAK, Tomáš, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, Jan KŘETÍNSKÝ, David MÜLLER, David PARKER a Jan STREJČEK. The Hanoi Omega-Automata Format. In Daniel Kroening, Corina Pasareanu. Computer Aided Verification: 27th International Conference, CAV 2015. Cham: Springer. s. 479-486. ISBN 978-3-319-21689-8. doi:10.1007/978-3-319-21690-4_31. 2015.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název The Hanoi Omega-Automata Format
Autoři BABIAK, Tomáš (703 Slovensko, domácí), František BLAHOUDEK (203 Česká republika, domácí), Alexandre DURET-LUTZ (250 Francie), Joachim KLEIN (276 Německo), Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí), David MÜLLER (276 Německo), David PARKER (826 Velká Británie a Severní Irsko) a Jan STREJČEK (203 Česká republika, domácí).
Vydání Cham, Computer Aided Verification: 27th International Conference, CAV 2015, od s. 479-486, 8 s. 2015.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Švýcarsko
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/15:00080919
Organizační jednotka Fakulta informatiky
ISBN 978-3-319-21689-8
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-21690-4_31
UT WoS 000364182900031
Klíčová slova anglicky automata; infinite words; verification
Štítky best, core_A, firank_1, formela-conference
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 4. 2016 14:24.
Anotace
We propose a flexible exchange format for omega-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people's work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Buchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.
Návaznosti
GBP202/12/G061, projekt VaVNázev: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky
MUNI/A/1159/2014, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1206/2014, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 20. 4. 2024 03:01