Forkable Regular Expressions
Martin Sulzmann, Peter Thiemann

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · semigroups and automata theory
