Detail publikace

Reasoning about Regular Properties: A Comparative Study

FIEDOR Tomáš, HOLÍK Lukáš, HRUŠKA Martin, ROGALEWICZ Adam, SÍČ Juraj a VARGOVČÍK Pavol. Reasoning about Regular Properties: A Comparative Study. In: Automated Deduction - CADE 29. Cham: Springer Nature Switzerland AG, 2023, s. 286-306. ISSN 0302-9743.
Název česky
Uvažování o regulárních vlastnostech: Srovnávací studie
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Fiedor Tomáš, Ing., Ph.D. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Hruška Martin, Ing. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Síč Juraj, Mgr. (UITS FIT VUT)
Vargovčík Pavol, Ing. (UITS FIT VUT)
Klíčová slova

Regulární jazyky, konečné automaty, nedeterministické automaty, srovnání nástrojů.

Abstrakt

V poslední době bylo navrženo několik nových algoritmů pro rozhodování o prázdnosti booleovských kombinací regulárních jazyků a jazyků střídavých automatů, zejména v souvislosti s analýzou regulárních výrazů a řešením řetězcových omezení. Nové algoritmy prokázaly značný potenciál, ale nikdy nebyly systematicky porovnány ani mezi sebou, ani s nejmodernějšími implementacemi stávajících metod založených na (ne)deterministických automatech. V tomto příspěvku takové srovnání přinášíme, stejně jako přehled existujících algoritmů a jejich implementací. Shromažďujeme různorodý benchmark většinou pocházející nebo související s praktickými problémy z oblasti řešení řetězcových omezení, analýzy vlastností LTL a kontroly regulárních modelů a vyhodnocujeme na něm shromážděné implementace. Výsledky odhalují nejlepší nástroje a napovídají, jaké jsou nejlepší algoritmy a implementační techniky. Zhruba lze říci, že ačkoli jsou některé pokročilé algoritmy rychlé, například antichainové algoritmy a redukce na IC3/PDR, nejsou tak drtivě dominantní, jak se někdy prezentuje, a není zde jasný vítěz. Nejjednodušší technologie založená na NFA může být někdy lepší volbou v závislosti na zdroji problému a stylu implementace. Domníváme se, že naše zjištění jsou relevantní pro vývoj automatových technik i pro příbuzné obory, jako je řešení řetězcových omezení.

Rok
2023
Strany
286-306
Časopis
Lecture Notes in Computer Science, č. 14132, ISSN 0302-9743
Sborník
Automated Deduction - CADE 29
Konference
29th International Conference on Automated Deduction, Rome, IT
Vydavatel
Springer Nature Switzerland AG
Místo
Cham, CH
DOI
10.1007/978-3-031-38499-8_17
BibTeX 
@INPROCEEDINGS{FITPUB13027,
   author = "Tom\'{a}\v{s} Fiedor and Luk\'{a}\v{s} Hol\'{i}k and Martin Hru\v{s}ka and Adam Rogalewicz and Juraj S\'{i}\v{c} and Pavol Vargov\v{c}\'{i}k",
   title = "Reasoning about Regular Properties: A Comparative Study",
   pages = "286--306",
   booktitle = "Automated Deduction - CADE 29",
   journal = "Lecture Notes in Computer Science",
   number = 14132,
   year = 2023,
   location = "Cham, CH",
   publisher = "Springer Nature Switzerland AG",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-031-38499-8\_17",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13027"
}
Nahoru