Detail publikace

Reasoning about Regular Properties: A Comparative Study

HOLÍK, L.; HRUŠKA, M.; SÍČ, J.; VARGOVČÍK, P.; FIEDOR, T.; ROGALEWICZ, A. Reasoning about Regular Properties: A Comparative Study. In Automated Deduction - CADE 29. Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2023. p. 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
anglicky
Autoři
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Hruška Martin, Ing., Ph.D. (VZ Automata@FIT)
Síč Juraj, Mgr. (UITS)
Vargovčík Pavol, Ing. (UITS)
Fiedor Tomáš, Ing., Ph.D. (VZ VERIFIT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
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
Vydavatel
Springer Nature Switzerland AG
Místo
Cham
DOI
10.1007/978-3-031-38499-8_17
UT WoS
001156342400017
EID Scopus
2-s2.0-85172215435
BibTeX 
@inproceedings{BUT185181,
  author="Lukáš {Holík} and Martin {Hruška} and Juraj {Síč} and Pavol {Vargovčík} and Tomáš {Fiedor} and Adam {Rogalewicz}",
  title="Reasoning about Regular Properties: A Comparative Study",
  booktitle="Automated Deduction - CADE 29",
  year="2023",
  journal="Lecture Notes in Computer Science",
  number="14132",
  pages="286--306",
  publisher="Springer Nature Switzerland AG",
  address="Cham",
  doi="10.1007/978-3-031-38499-8\{_}17",
  issn="0302-9743"
}
Nahoru