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
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
UT WoS
001156342400017
EID Scopus
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