Aurèle Barrière

Victor Deng, Aurèle Barrière, Clément Pit-Claudel

Despite widespread use, the complexity class of modern regular expression matching was not well-understood. Previous work proved that regular expression matching with backreferences and lookarounds was PSPACE-complete, but the proof was not mechanized and applied to an abstract regex language. This paper clarifies the question for JavaScript regular expressions. In this paper, we prove the following new results, with most core proofs mechanized in the Rocq proof assistant. We prove that JavaScript regex matching is indeed PSPACE-hard, even without negative lookarounds, and OptP-hard as well; that JavaScript regex matching without lower-bounded quantifiers (i.e. quantifiers with a non-zero minimum number of repetitions) is PSPACE-complete; and that JavaScript regex matching without lower-bounded quantifiers and without lookarounds is OptP-complete.

Aurèle Barrière, Victor Deng, Clément Pit-Claudel

We present the first mechanized, succinct, practical, complete, and proven-faithful semantics for a modern regular expression language with backtracking semantics. We ensure its faithfulness by proving it equivalent to a preexisting line-by-line embedding of the official ECMAScript specification of JavaScript regular expressions. We demonstrate its practicality by presenting two real-world applications. First, a new notion of contextual equivalence for modern regular expressions, which we use to prove or disprove rewrites drawn from previous work. Second, the first formal proof of the PikeVM algorithm used in many real-world engines. In contrast with the specification and other formalization work, our semantics captures not only the top-priority match, but a full backtracking tree recording all possible matches and their respective priority. All our definitions and results have been mechanized in the Rocq proof assistant.

Aurèle Barrière, Bastien Maubert, Aniello Murano et al.

We study dynamic changes of agents' observational power in logics of knowledge and time. We consider CTL*K, the extension of CTL* with knowledge operators, and enrich it with a new operator that models a change in an agent's way of observing the system. We extend the classic semantics of knowledge for perfect-recall agents to account for changes of observation, and we show that this new operator strictly increases the expressivity of CTL*K. We reduce the model-checking problem for our logic to that for CTL*K, which is known to be decidable. This provides a solution to the model-checking problem for our logic, but its complexity is not optimal. Indeed we provide a direct decision procedure with better complexity.