Forkable Regular Expressions

TL;DR

This paper introduces forkable regular expressions with a fork operator to analyze concurrent program communication, providing a formal semantics, automata generation methods, and conditions for finiteness despite potential non-regularity.

Contribution

It develops a formal foundation for forkable regular expressions, including semantics, derivatives, and automata construction, addressing challenges posed by non-regular languages.

Findings

Defined a novel semantics for forkable expressions

Established derivatives for automata generation

Identified conditions ensuring automata finiteness

Abstract

We consider forkable regular expressions, which enrich regular expressions with a fork operator, to establish a formal basis for static and dynamic analysis of the communication behavior of concurrent programs. We define a novel compositional semantics for forkable expressions, establish their fundamental properties, and define derivatives for them as a basis for the generation of automata, for matching, and for language containment tests. Forkable expressions may give rise to non-regular languages, in general, but we identify sufficient conditions on expressions that guarantee finiteness of the automata construction via derivatives.