Informační systém Masarykovy univerzity 

Is there a best Büchi automaton for explicit model checking?

česky | in English

BLAHOUDEK, František, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Is there a best Büchi automaton for explicit model checking? In Neha Rungta and Oksana Tkachuk. 2014 International SPIN Symposium on Model Checking of Software. New York: ACM, 2014. s. 68-143. ISBN 978-1-4503-2452-6. doi:10.1145/2632362.2632377.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Is there a best Büchi automaton for explicit model checking?
Název česky Existuje nejlepší Büchiho automat pro explicitní metodu ověřování modelu?
Autoři BLAHOUDEK, František (203 Česká republika, domácí), Alexandre DURET-LUTZ (250 Francie), Mojmír KŘETÍNSKÝ (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí).
Vydání New York, 2014 International SPIN Symposium on Model Checking of Software, s. 68-143, 2014.
Nakladatel ACM
Další údaje
Originální jazyk angličtina
Typ výsledku Článek ve sborníku
Obor Informatika
Stát vydavatele Spojené státy americké
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
Kód RIV RIV/00216224:14330/14:00073815
Organizační jednotka Fakulta informatiky
ISBN 978-1-4503-2452-6
Doi http://dx.doi.org/10.1145/2632362.2632377
Klíčová slova anglicky linear temporal logic; Büchi automata; explicit model checking
Štítky Büchi automata, formela-conference, LTL, Model checking
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: doc. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 2. 4. 2015 16:51.
Anotace
LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.
Anotace česky
Překladače LTL na Büchiho automaty jsou obvykle optimalizovány tak, aby produkovaly automaty s co nejmenším počtem stavů, či s co nejmenším počtem nedeterministických stavů. V této publikaci hledáme vlastnosti Büchiho automatů, které skutečně ovlivňují výkon nástrojů pro explicitní metodu ověřování modelu (model checking). A to pomocí manuální analýzy několika automatů a experimenty s běžnými překladače LTL na automaty a realistickými verifikačními úlohami. Výsledkem těchto experimentů je lepší porozumění charakteristik automatů, které jsou dobré pro model checker Spin.
Návaznosti
GBP202/12/G061, projekt VaVNázev: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Projekty na podporu excelence v základním výzkumu
MUNI/A/0765/2013, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0855/2013, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
Typ Název Vložil/a Vloženo Práva
1196458 /1 Blahoudek, F. 2. 9. 2014

Vlastnosti

Název
1196458
Aplikace
Obnovit.
Adresa v ISu
https://is.muni.cz/auth/repo/1196458/
Adresa ze světa
https://is.muni.cz/repo/1196458/
Adresa do Správce
https://is.muni.cz/auth/repo/1196458/?info
Ze světa do Správce
https://is.muni.cz/repo/1196458/?info
Vloženo
Út 2. 9. 2014 09:39

Práva

Právo číst
  • kdokoliv v Internetu
Právo vkládat
 
Právo spravovat
  • osoba RNDr. František Blahoudek, učo 208029
  • osoba doc. RNDr. Jan Strejček, Ph.D., učo 3366
  • osoba prof. RNDr. Mojmír Křetínský, CSc., učo 631
Atributy
 
spin2014preprint.pdf Licence Creative Commons  Verze souboru Blahoudek, F. 2. 9. 2014

Vlastnosti

Adresa v ISu
https://is.muni.cz/auth/repo/1196458/spin2014preprint.pdf
Adresa ze světa
https://is.muni.cz/repo/1196458/spin2014preprint.pdf
Adresa do Správce
https://is.muni.cz/auth/repo/1196458/spin2014preprint.pdf?info
Ze světa do Správce
https://is.muni.cz/repo/1196458/spin2014preprint.pdf?info
Vloženo
Út 2. 9. 2014 09:39

Práva

Právo číst
  • kdokoliv v Internetu
Právo vkládat
 
Právo spravovat
  • osoba RNDr. František Blahoudek, učo 208029
  • osoba doc. RNDr. Jan Strejček, Ph.D., učo 3366
  • osoba prof. RNDr. Mojmír Křetínský, CSc., učo 631
Atributy
 

spin2014preprint.pdf

Aplikace
Otevřít soubor.
Stáhnout soubor.
Adresa v ISu
https://is.muni.cz/auth/repo/1196458/spin2014preprint.pdf
Adresa ze světa
http://is.muni.cz/repo/1196458/spin2014preprint.pdf
Typ souboru
PDF (application/pdf)
Velikost
275,5 KB
Hash md5
f9fe3e978d5e63e5fa4c0f0058ca935b
Vloženo
Út 2. 9. 2014 09:39

spin2014preprint.txt

Aplikace
Otevřít soubor.
Stáhnout soubor.
Adresa v ISu
https://is.muni.cz/auth/repo/1196458/spin2014preprint.txt
Adresa ze světa
http://is.muni.cz/repo/1196458/spin2014preprint.txt
Typ souboru
holý text (text/plain)
Velikost
38,9 KB
Hash md5
31dd63fb0a882c939dc34a0c9aef2f53
Vloženo
Út 2. 9. 2014 09:42
Vytisknout
Nahlásit neoprávněně vložený soubor Zobrazeno: 13. 12. 2017 19:40

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 13. 12. 2017 19:40, 50. (sudý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému