-
The Trichotomy of Regular Property Testing
Authors:
Gabriel Bathie,
Nathanaël Fijalkow,
Corto Mascle
Abstract:
Property testing is concerned with the design of algorithms making a sublinear number of queries to distinguish whether the input satisfies a given property or is far from having this property. A seminal paper of Alon, Krivelevich, Newman, and Szegedy in 2001 introduced property testing of formal languages: the goal is to determine whether an input word belongs to a given language, or is far from…
▽ More
Property testing is concerned with the design of algorithms making a sublinear number of queries to distinguish whether the input satisfies a given property or is far from having this property. A seminal paper of Alon, Krivelevich, Newman, and Szegedy in 2001 introduced property testing of formal languages: the goal is to determine whether an input word belongs to a given language, or is far from any word in that language. They constructed the first property testing algorithm for the class of all regular languages. This opened a line of work with improved complexity results and applications to streaming algorithms. In this work, we show a trichotomy result: the class of regular languages can be divided into three classes, each associated with an optimal query complexity. Our analysis yields effective characterizations for all three classes using so-called minimal blocking sequences, reasoning directly and combinatorially on automata.
△ Less
Submitted 27 April, 2025;
originally announced April 2025.
-
On the Minimisation of Deterministic and History-Deterministic Generalised (co)Büchi Automata
Authors:
Antonio Casares,
Olivier Idir,
Denis Kuperberg,
Corto Mascle,
Aditya Prakash
Abstract:
We present a polynomial-time algorithm minimising the number of states of history-deterministic generalised coBüchi automata, building on the work of Abu Radi and Kupferman on coBüchi automata. On the other hand, we establish that the minimisation problem for both deterministic and history-deterministic generalised Büchi automata is NP-complete, as well as the problem of minimising at the same tim…
▽ More
We present a polynomial-time algorithm minimising the number of states of history-deterministic generalised coBüchi automata, building on the work of Abu Radi and Kupferman on coBüchi automata. On the other hand, we establish that the minimisation problem for both deterministic and history-deterministic generalised Büchi automata is NP-complete, as well as the problem of minimising at the same time the number of states and colours of history-deterministic generalised coBüchi automata.
△ Less
Submitted 23 November, 2024; v1 submitted 25 July, 2024;
originally announced July 2024.
-
Verification of Population Protocols with Unordered Data
Authors:
Steffen van Bergerem,
Roland Guttenberg,
Sandra Kiefer,
Corto Mascle,
Nicolas Waldburger,
Chana Weil-Kennedy
Abstract:
Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, that is, the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin…
▽ More
Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, that is, the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin and Ladouceur (ICALP'23) introduced population protocols with unordered data (PPUD). In PPUD, each agent carries a fixed data value, and the interactions between agents depend on whether their data are equal or not. Blondin and Ladouceur also identified the interesting subclass of immediate observation PPUD (IOPPUD), where in every transition one of the two agents remains passive and does not move, and they characterised its expressive power.
We study the decidability and complexity of formally verifying these protocols. The main verification problem for population protocols is well-specification, that is, checking whether the given PPUD computes some function. We show that well-specification is undecidable in general. By contrast, for IOPPUD, we exhibit a large yet natural class of problems, which includes well-specification among other classic problems, and establish that these problems are in EXPSPACE. We also provide a lower complexity bound, namely coNEXPTIME-hardness.
△ Less
Submitted 1 May, 2024;
originally announced May 2024.
-
The Complexity of Simplifying $ω$-Automata through the Alternating Cycle Decomposition
Authors:
Antonio Casares,
Corto Mascle
Abstract:
In 2021, Casares, Colcombet and Fijalkow introduced the Alternating Cycle Decomposition (ACD), a structure used to define optimal transformations of Muller into parity automata and to obtain theoretical results about the possibility of relabelling automata with different acceptance conditions. In this work, we study the complexity of computing the ACD and its DAG-version, proving that this can be…
▽ More
In 2021, Casares, Colcombet and Fijalkow introduced the Alternating Cycle Decomposition (ACD), a structure used to define optimal transformations of Muller into parity automata and to obtain theoretical results about the possibility of relabelling automata with different acceptance conditions. In this work, we study the complexity of computing the ACD and its DAG-version, proving that this can be done in polynomial time for suitable representations of the acceptance condition of the Muller automaton. As corollaries, we obtain that we can decide typeness of Muller automata in polynomial time, as well as the parity index of the languages they recognise.
Furthermore, we show that we can minimise in polynomial time the number of colours (resp. Rabin pairs) defining a Muller (resp. Rabin) acceptance condition, but that these problems become NP-complete when taking into account the structure of an automaton using such a condition.
△ Less
Submitted 28 June, 2024; v1 submitted 8 January, 2024;
originally announced January 2024.
-
Learning temporal formulas from examples is hard
Authors:
Corto Mascle,
Nathanaël Fijalkow,
Guillaume Lagarde
Abstract:
We study the problem of learning linear temporal logic (LTL) formulas from examples, as a first step towards expressing a property separating positive and negative instances in a way that is comprehensible for humans. In this paper we initiate the study of the computational complexity of the problem. Our main results are hardness results: we show that the LTL learning problem is NP-complete, both…
▽ More
We study the problem of learning linear temporal logic (LTL) formulas from examples, as a first step towards expressing a property separating positive and negative instances in a way that is comprehensible for humans. In this paper we initiate the study of the computational complexity of the problem. Our main results are hardness results: we show that the LTL learning problem is NP-complete, both for the full logic and for almost all of its fragments. This motivates the search for efficient heuristics, and highlights the complexity of expressing separating properties in concise natural language.
△ Less
Submitted 26 December, 2023;
originally announced December 2023.
-
Model-checking parametric lock-sharing systems against regular constraints
Authors:
Corto Mascle,
Anca Muscholl,
Igor Walukiewicz
Abstract:
In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong process fairness condition. A result of a potentially infinite execution of a system is a limit configuration, that is a potentially infinite tree. The verificat…
▽ More
In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong process fairness condition. A result of a potentially infinite execution of a system is a limit configuration, that is a potentially infinite tree. The verification problem is to determine if a given system has a limit configuration satisfying a given regular property. This formulation of the problem encompasses verification of reachability as well as of many liveness properties. We show that this verification problem, while undecidable in general, is decidable for nested lock usage. We show Exptime-completeness of the verification problem. The main source of complexity is the number of parameters in the spawn operation. If the number of parameters is bounded, our algorithm works in Ptime for properties expressed by parity automata with a fixed number of ranks.
△ Less
Submitted 10 July, 2023;
originally announced July 2023.
-
Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
Authors:
Lucie Guillou,
Corto Mascle,
Nicolas Waldburger
Abstract:
We consider the parameterized verification of arbitrarily large networks of agents which communicate by broadcasting and receiving messages. In our model, the broadcast topology is reconfigurable so that a sent message can be received by any set of agents. In addition, agents have local registers which are initially distinct and may therefore be thought of as identifiers. When an agent broadcasts…
▽ More
We consider the parameterized verification of arbitrarily large networks of agents which communicate by broadcasting and receiving messages. In our model, the broadcast topology is reconfigurable so that a sent message can be received by any set of agents. In addition, agents have local registers which are initially distinct and may therefore be thought of as identifiers. When an agent broadcasts a message, it appends to the message the value stored in one of its registers. Upon reception, an agent can store the received value or test this value for equality with one of its own registers. We consider the coverability problem, where one asks whether a given state of the system may be reached by at least one agent. We establish that this problem is decidable; however, it is as hard as coverability in lossy channel systems, which is non-primitive recursive. This model lies at the frontier of decidability as other classical problems on this model are undecidable; this is in particular true for the target problem where all processes must synchronize on a given state. By contrast, we show that the coverability problem is NP-complete when each agent has only one register.
△ Less
Submitted 4 March, 2024; v1 submitted 2 June, 2023;
originally announced June 2023.
-
Model-checking lock-sharing systems against regular constraints
Authors:
Corto Mascle
Abstract:
We study the verification of distributed systems where processes are finite automata with access to a shared pool of locks. We consider objectives that are boolean combinations of local regular constraints. We show that the problem, PSPACE-complete in general, falls in NP with the right assumptions on the system. We use restrictions on the number of locks a process can access and the order in whic…
▽ More
We study the verification of distributed systems where processes are finite automata with access to a shared pool of locks. We consider objectives that are boolean combinations of local regular constraints. We show that the problem, PSPACE-complete in general, falls in NP with the right assumptions on the system. We use restrictions on the number of locks a process can access and the order in which locks can be released. We provide tight complexity bounds, as well as a subcase of interest that can be solved in PTIME.
△ Less
Submitted 14 October, 2022;
originally announced October 2022.
-
Distributed controller synthesis for deadlock avoidance
Authors:
Hugo Gimbert,
Corto Mascle,
Anca Muscholl,
Igor Walukiewicz
Abstract:
We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable even for three processes each using a fixed number of locks. We propose two restrictions that make distributed control decidable. The first one is to allow each process to use at most two loc…
▽ More
We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable even for three processes each using a fixed number of locks. We propose two restrictions that make distributed control decidable. The first one is to allow each process to use at most two locks. The problem then becomes Sigma2P-complete, and even in PTIME under some additional assumptions. The dining philosophers problem satisfies these assumptions. The second restriction is a nested usage of locks. In this case the synthesis problem is NEXPTIME-complete. The drinking philosophers problem falls in this case.
△ Less
Submitted 1 November, 2024; v1 submitted 26 April, 2022;
originally announced April 2022.
-
Keyboards as a new model of computation
Authors:
Yoan Géran,
Bastien Laboureix,
Corto Mascle,
Valentin D. Richard
Abstract:
We introduce a new formalisation of languages, called keyboards. We consider a set of elementary operations (writing/erasing a letter, going to the right or to the left,...) and we define a keyboard as a set of finite sequences of such operations, called keys. The corresponding language is the set of words obtained by applying some sequence of those keys. Unlike classical models of computation, ev…
▽ More
We introduce a new formalisation of languages, called keyboards. We consider a set of elementary operations (writing/erasing a letter, going to the right or to the left,...) and we define a keyboard as a set of finite sequences of such operations, called keys. The corresponding language is the set of words obtained by applying some sequence of those keys. Unlike classical models of computation, every key can be applied anytime. We define various classes of languages based on different sets of elementary operations, and compare their expressive powers. We also compare them to well-known classes of languages (Chomsky hierarchy). We obtain a strict hierarchy of languages, whose expressivity is orthogonal to the one of the aforementionned classical models.
--
Nous introduisons une nouvelle représentation de langages, les claviers. On se munit d'un ensemble d'opérations élémentaires (ajout, effacement d'une lettre, déplacement à droite, à gauche, ...), et on définit un clavier comme un ensemble de suites finies d'opérations élémentaires, appelées touches. Son langage sera l'ensemble des mots obtenus en appliquant une suite quelconque de touches. Contrairement à des modèles de calcul classiques, toutes les touches peuvent être appliquées à tout moment. En premier lieu nous définissons différentes classes de claviers en faisant varier l'ensemble des opérations élémentaires autorisées, et nous comparons l'expressivité des classes de langages obtenues. Nous comparons également ces classes à la hiérarchie de Chomsky. Nous obtenons que toutes les classes étudiées sont différentes, et nous caractérisons les classes inclues dans les rationnels et les algébriques. L'expressivité des claviers semble orthogonale à celle des modèles évoqués précédemment.
△ Less
Submitted 1 July, 2021; v1 submitted 19 February, 2021;
originally announced February 2021.
-
Responsibility and verification: Importance value in temporal logics
Authors:
Corto Mascle,
Christel Baier,
Florian Funke,
Simon Jantsch,
Stefan Kiefer
Abstract:
We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing wheth…
▽ More
We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing whether the system can still fulfill the specification. We study this idea in the framework of model-checking with various classical types of linear-time specification, and propose several ways to transpose it to branching ones. We also provide tight complexity bounds in almost every case.
△ Less
Submitted 20 April, 2021; v1 submitted 12 February, 2021;
originally announced February 2021.
-
Controlling a Random Population is EXPTIME-hard
Authors:
Corto Mascle,
Mahsa Shirmohammadi,
Patrick Totzke
Abstract:
Bertrand et al. [1] (LMCS 2019) describe two-player zero-sum games in which one player tries to achieve a reachability objective in $n$ games (on the same finite arena) simultaneously by broadcasting actions, and where the opponent has full control of resolving non-deterministic choices. They show EXPTIME completeness for the question if such games can be won for every number $n$ of games.
We co…
▽ More
Bertrand et al. [1] (LMCS 2019) describe two-player zero-sum games in which one player tries to achieve a reachability objective in $n$ games (on the same finite arena) simultaneously by broadcasting actions, and where the opponent has full control of resolving non-deterministic choices. They show EXPTIME completeness for the question if such games can be won for every number $n$ of games.
We consider the almost-sure variant in which the opponent randomizes their actions, and where the player tries to achieve the reachability objective eventually with probability one. The lower bound construction in [1] does not directly carry over to this randomized setting. In this note we show EXPTIME hardness for the almost-sure problem by reduction from Countdown Games.
△ Less
Submitted 13 September, 2019;
originally announced September 2019.
-
The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas
Authors:
Corto Mascle,
Martin Zimmermann
Abstract:
HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental security policies like noninterference and observational determinism, but has also found applications beyond security, e.g., distributed protoco…
▽ More
HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental security policies like noninterference and observational determinism, but has also found applications beyond security, e.g., distributed protocols and coding theory. However, HyperLTL satisfiability is undecidable as soon as there are existential quantifiers in the scope of a universal one. To overcome this severe limitation to applicability, we investigate here restricted variants of the satisfiability problem to pinpoint the decidability border.
First, we restrict the space of admissible models and show decidability when restricting the search space to models of bounded size or to finitely representable ones. Second, we consider formulas with restricted nesting of temporal operators and show that nesting depth one yields decidability for a slightly larger class of quantifier prefixes. We provide tight complexity bounds in almost all cases.
△ Less
Submitted 13 December, 2019; v1 submitted 11 July, 2019;
originally announced July 2019.
-
On Nonnegative Integer Matrices and Short Killing Words
Authors:
Stefan Kiefer,
Corto Mascle
Abstract:
Let $n$ be a natural number and $\mathcal{M}$ a set of $n \times n$-matrices over the nonnegative integers such that the joint spectral radius of $\mathcal{M}$ is at most one. We show that if the zero matrix $0$ is a product of matrices in $\mathcal{M}$, then there are $M_1, \ldots, M_{n^5} \in \mathcal{M}$ with $M_1 \cdots M_{n^5} = 0$. This result has applications in automata theory and the theo…
▽ More
Let $n$ be a natural number and $\mathcal{M}$ a set of $n \times n$-matrices over the nonnegative integers such that the joint spectral radius of $\mathcal{M}$ is at most one. We show that if the zero matrix $0$ is a product of matrices in $\mathcal{M}$, then there are $M_1, \ldots, M_{n^5} \in \mathcal{M}$ with $M_1 \cdots M_{n^5} = 0$. This result has applications in automata theory and the theory of codes. Specifically, if $X \subset Σ^*$ is a finite incomplete code, then there exists a word $w \in Σ^*$ of length polynomial in $\sum_{x \in X} |x|$ such that $w$ is not a factor of any word in $X^*$. This proves a weak version of Restivo's conjecture.
△ Less
Submitted 26 February, 2021; v1 submitted 2 August, 2018;
originally announced August 2018.
-
From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics
Authors:
Corto Mascle,
Daniel Neider,
Maximilian Schwenger,
Paulo Tabuada,
Alexander Weinert,
Martin Zimmermann
Abstract:
Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.…
▽ More
Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions. However, a wide range of formulas are not monitorable under this approach, meaning that they have a prefix for which satisfaction and violation will always remain undetermined no matter how it is extended. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category.
Recently, a robust semantics for LTL was introduced to capture different degrees by which a property can be violated. In this paper we introduce a robust semantics for finite strings and show its potential in monitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we discuss which properties that come naturally in LTL monitoring - such as the realizability of all truth values - can be transferred to the robust setting. Lastly, we show that LTL formulas with robust semantics can be monitored by deterministic automata and report on a prototype implementation.
△ Less
Submitted 12 September, 2022; v1 submitted 21 July, 2018;
originally announced July 2018.
