Reasoning about Regular Properties: A Comparative Study

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F23%3APU149408" target="_blank" >RIV/00216305:26230/23:PU149408 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.1007/978-3-031-38499-8_17" target="_blank" >http://dx.doi.org/10.1007/978-3-031-38499-8_17</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-38499-8_17" target="_blank" >10.1007/978-3-031-38499-8_17</a>

Result language

angličtina

Original language name

Reasoning about Regular Properties: A Comparative Study

Original language description

Several new algorithms for deciding emptiness of Boolean combinations of regular languages and of languages of alternating automata have been proposed recently, especially in the context of analysing regular expressions and in string constraint solving. The new algorithms demonstrated a significant potential, but they have never been systematically compared, neither among each other nor with the state-of-the art implementations of existing (non)deterministic automata-based methods. In this paper, we provide such comparison as well as an overview of the existing algorithms and their implementations. We collect a diverse benchmark mostly originating in or related to practical problems from string constraint solving, analysing LTL properties, and regular model checking, and evaluate collected implementations on it. The results reveal the best tools and hint on what the best algorithms and implementation techniques are. Roughly, although some advanced algorithms are fast, such as antichain algorithms and reductions to IC3/PDR, they are not as overwhelmingly dominant as sometimes presented and there is no clear winner. The simplest NFA-based technology may sometimes be a better choice, depending on the problem source and the implementation style. We believe that our findings are relevant for development of automata techniques as well as for related fields such as string constraint solving.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/LL1908" target="_blank" >LL1908: Efficient Finite Automata for Automated Reasoning</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2023

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Automated Deduction - CADE 29

ISBN

—

ISSN

0302-9743

e-ISSN

—

Number of pages

21

Pages from-to

286-306

Publisher name

Springer Nature Switzerland AG

Place of publication

Cham

Event location

Rome

Event date

Jul 1, 2023

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001156342400017