Arrow Research search

Author name cluster

Nicolas Mazzocchi

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers
2 author rows

Possible papers

4

Highlights Conference 2024 Conference Abstract

Safety and Liveness but Quantitative

  • Nicolas Mazzocchi

Safety and liveness are fundamental concepts in computer-aided verification. The safety-liveness classification of Boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In the quantitative setting, properties are arbitrary functions from infinite words to partially-ordered domains. First, we define quantitative safety and liveness, and prove that our definitions induce conservative quantitative generalizations of both the safety-progress hierarchy and the safety-liveness decomposition of Boolean properties. Consequently, like their Boolean counterparts, quantitative properties can be written as the pointwise minimum of a quantitative safety property and a quantitative liveness property. This work has been published in FoSSaCS 2023 Proceedings. Second, we instantiate our framework with the classes of quantitative properties expressed by automata. These quantitative automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totally-ordered domain of real numbers. In this automata-theoretic setting, we establish a connection between quantitative safety and topological continuity and provide alternative characterizations of quantitative safety and liveness in terms of their boolean analogs. For all common value functions, we provide a procedure for deciding whether a given automaton is safe or live, we show how to construct its safety closure, and we present a decomposition into safe and live automata. This work has been published in CONCUR 2023 Proceedings. Third, we provide a program that implements the above decide procedures and constructions for Inf, Sup, LimInf, LimSup, LimInfAvg, and LimSupAvg quantitative automata given in an input text file. The performance of our tool is based on a quantitative generalization of the omega-regular language inclusion checker FORKLIFT (published in CAV 2022 Proceedings). This tool is currently unpublished.

Details

MFCS Conference 2020 Conference Paper

Unary Prime Languages

  • Ismaël Jecker
  • Orna Kupferman
  • Nicolas Mazzocchi

A regular language L of finite words is composite if there are regular languages L₁, L₂, …, L_t such that L = ⋂_{i = 1}^t L_i and the index (number of states in a minimal DFA) of every language L_i is strictly smaller than the index of L. Otherwise, L is prime. Primality of regular languages was introduced and studied in [O. Kupferman and J. Mosheiff, 2015], where the complexity of deciding the primality of the language of a given DFA was left open, with a doubly-exponential gap between the upper and lower bounds. We study primality for unary regular languages, namely regular languages with a singleton alphabet. A unary language corresponds to a subset of ℕ, making the study of unary prime languages closer to that of primality in number theory. We show that the setting of languages is richer. In particular, while every composite number is the product of two smaller numbers, the number t of languages necessary to decompose a composite unary language induces a strict hierarchy. In addition, a primality witness for a unary language L, namely a word that is not in L but is in all products of languages that contain L and have an index smaller than L’s, may be of exponential length. Still, we are able to characterize compositionality by structural properties of a DFA for L, leading to a LogSpace algorithm for primality checking of unary DFAs.

Details

Highlights Conference 2018 Conference Abstract

A Pattern Logic for Automata with Outputs

  • Nicolas Mazzocchi

ABSTRACT. We introduce a logic to express structural properties of automata with string inputs and, possibly, outputs in some monoid. In this logic, the set of predicates talking about the output values is parametric, and we provide sufficient conditions on the predicates under which the model-checking problem is decidable. We then consider three particular automata models (finite automata, transducers and automata weighted by integers) and instantiate the generic logic for each of them. We give tight complexity results for the three logics with respect to the model-checking problem, depending on whether the formula is fixed or not. We study the expressiveness of our logics by expressing classical structural patterns characterising for instance finite ambiguity and polynomial ambiguity in the case of finite automata, determinisability and finite-valuedness in the case of transducers and automata weighted by integers. As a consequence of our complexity results, we directly obtain that these classical properties can be decided in polynomial time.

Details
v2026.09.13