Etienne Renault

Translation of semi-extended regular expressions using derivatives

By Antoine Martin, Etienne Renault, Alexandre Duret-Lutz

2024-06-20

In Proceedings of the 28th international conference on implementation and applications of automata (CIAA’24)

Abstract

We generalize Antimirov’s notion of linear form of a regular expression, to the Semi-Extended Regular Expressions typically used in the Property Specification Language or SystemVerilog Assertions. Doing so requires extending the construction to handle more operators, and dealing with expressions over alphabets $\Sigma=2^{AP}$ of valuations of atomic propositions. Using linear forms to construct automata labeled by Boolean expressions suggests heuristics that we evaluate. Finally, we study a variant of this translation to automata with accepting transitions: this construction is more natural and provides smaller automata.

Continue reading