arXiv subjects

Michael Blondin

Publications and source records attributed to Michael Blondin.

At least 19 recordsLinked to original sources

arXiv2026

Population Protocols over Ordered Agents

Population protocols are a distributed computation model in which a collection of anonymous, finite-state agents interact in randomly chosen pairs and update their states according to a fixed transition function. The computation is defined by the eventual stabilization of the population to a consensus that represents the output. In practice, it is natural to allow each agent to carry a unique identifier and compare it with that of another agent before interacting. We model this extension by having agents be totally ordered and interactions between two agents to be fireable only if their pair of identifiers falls in some condition set. For instance, $\mathsf{PP}[<]$ allows for two agents to interact only if the first one appears before the second one. We study population protocols over ordered agents $\mathsf{PP}[N]$ where $N$ is a set of predicates available to restrict transition firing. We also study $\textsf{IO-PP}[N]$, the immediate observation fragment of $\mathsf{PP}[N]$ where only one agent changes state per interaction. Our main result is that $\textsf{IO-PP}[<]$ recognizes exactly the unambiguous star-free languages, which admits many other characterizations, such as two-variable first-order logic or two-way deterministic partially-ordered automata. We also provide a logic and an automaton model that fits in $\mathsf{PP}[<]$. We further show that if the successor predicate appears in a set $N$ of $\mathsf{NSPACE}(n)$-computable predicates, then $\textsf{IO-PP}[N]=\mathsf{PP}[N]=\mathsf{NSPACE}(n)$. Finally, we investigate the problem of deciding whether a given population protocol always stabilizes to a consensus. While this problem is decidable for unordered population protocols, we show that this is undecidable already for $\mathsf{PP}[<]$ and $\textsf{IO-PP}[+1]$, but conditionally decidable for $\textsf{IO-PP}[<]$.

cs.DC↗

arXiv2025

Soundness of reset workflow nets

Workflow nets are a well-established variant of Petri nets for the modeling of process activities such as business processes. The standard correctness notion of workflow nets is soundness, which comes in several variants. Their decidability was shown decades ago, but their complexity was only identified recently. In this work, we are primarily interested in two popular variants: $1$-soundness and generalised soundness. Workflow nets have been extended with resets to model workflows that can, e.g., cancel actions. It has been known for a while that, for this extension, all variants of soundness, except possibly generalised soundness, are undecidable. We complete the picture by showing that generalised soundness is also undecidable for reset workflow nets. We then blur this undecidability landscape by identifying a property, coined ``$1$-in-between soundness'', which lies between $1$-soundness and generalised soundness. It reveals an unusual non-monotonic complexity behaviour: a decidable soundness property is in between two undecidable ones. This can be valuable in the algorithmic analysis of reset workflow nets, as our procedure yields an output of the form ``$1$-sound'' or ``not generalised sound'' which is always correct.

cs.FL↗

arXiv2025

Weakly acyclic diagrams: A data structure for infinite-state symbolic verification

Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checking. OBDDs allow for efficient algorithms using top-down dynamic programming. From an automata-theoretic perspective, OBDDs essentially are minimal deterministic finite automata recognizing languages whose words have a fixed length (the arity of the Boolean function). We introduce weakly acyclic diagrams (WADs), a generalization of OBDDs that maintains their algorithmic advantages, but can also represent infinite languages. We develop the theory of WADs and show that they can be used for symbolic model checking of various models of infinite-state systems.

cs.LO↗

arXiv2024

Separators in Continuous Petri Nets

Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking $\vec{m}_\text{src}$ cannot reach a marking $\vec{m}_\text{tgt}$, then there is a formula $φ$ of Presburger arithmetic such that: $φ(\vec{m}_\text{src})$ holds; $φ$ is forward invariant, i.e., $φ(\vec{m})$ and $\vec{m} \rightarrow \vec{m}'$ imply $φ(\vec{m}'$); and $\neg φ(\vec{m}_\text{tgt})$ holds. While these separators could be used as explanations and as formal certificates of unreachability, this has not yet been the case due to their worst-case size, which is at least Ackermannian, and the complexity of checking that a formula is a separator, which is at least exponential (in the formula size). We show that, in continuous Petri nets, these two problems can be overcome. We introduce locally closed separators, and prove that: (a) unreachability can be witnessed by a locally closed separator computable in polynomial time; (b) checking whether a formula is a locally closed separator is in NC (so, simpler than unreachability, which is P-complete). We further consider the more general problem of (existential) set-to-set reachability, where two sets of markings are given as convex polytopes. We show that, while our approach does not extend directly, we can efficiently certify unreachability via an altered Petri net.

cs.LO↗

arXiv2023

Population Protocols with Unordered Data

Population protocols form a well-established model of computation of passively mobile anonymous agents with constant-size memory. It is well known that population protocols compute Presburger-definable predicates, such as absolute majority and counting predicates. In this work, we initiate the study of population protocols operating over arbitrarily large data domains. More precisely, we introduce population protocols with unordered data as a formalism to reason about anonymous crowd computing over unordered sequences of data. We first show that it is possible to determine whether an unordered sequence from an infinite data domain has a datum with absolute majority. We then establish the expressive power of the immediate observation restriction of our model, namely where, in each interaction, an agent observes another agent who is unaware of the interaction.

cs.DC↗

arXiv2023

Verifying linear temporal specifications of constant-rate multi-mode systems

Constant-rate multi-mode systems (MMS) are hybrid systems with finitely many modes and real-valued variables that evolve over continuous time according to mode-specific constant rates. We introduce a variant of linear temporal logic (LTL) for MMS, and we investigate the complexity of the model-checking problem for syntactic fragments of LTL. We obtain a complexity landscape where each fragment is either P-complete, NP-complete or undecidable. These results generalize and unify several results on MMS and continuous counter systems.

cs.LO↗

arXiv2022

Verifying generalised and structural soundness of workflow nets via relaxations

Workflow nets are a well-established mathematical formalism for the analysis of business processes arising from either modeling tools or process mining. The central decision problems for workflow nets are $k$-soundness, generalised soundness and structural soundness. Most existing tools focus on $k$-soundness. In this work, we propose novel scalable semi-procedures for generalised and structural soundness. This is achieved via integral and continuous Petri net reachability relaxations. We show that our approach is competitive against state-of-the-art tools.

cs.LO↗

arXiv2022

The complexity of soundness in workflow nets

Workflow nets are a popular variant of Petri nets that allow for algorithmic formal analysis of business processes. The central decision problems concerning workflow nets deal with soundness, where the initial and final configurations are specified. Intuitively, soundness states that from every reachable configuration one can reach the final configuration. We settle the widely open complexity of the three main variants of soundness: classical, structural and generalised soundness. The first two are EXPSPACE-complete, and, surprisingly, the latter is PSPACE-complete, thus computationally simpler.

cs.LO↗

arXiv2021

Affine Extensions of Integer Vector Addition Systems with States

We study the reachability problem for affine $\mathbb{Z}$-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine $\mathbb{Z}$-VASS with the finite-monoid property (afmp-$\mathbb{Z}$-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-$\mathbb{Z}$-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-$\mathbb{Z}$-VASS reduces to reachability in a $\mathbb{Z}$-VASS whose control-states grow linearly in the size of the matrix monoid. Our construction shows that reachability relations of afmp-$\mathbb{Z}$-VASS are semilinear, and in particular enables us to show that reachability in $\mathbb{Z}$-VASS with transfers and $\mathbb{Z}$-VASS with copies is PSPACE-complete. We then focus on the reachability problem for affine $\mathbb{Z}$-VASS with monogenic monoids: (possibly infinite) matrix monoids generated by a single matrix. We show that, in a particular case, the reachability problem is decidable for this class, disproving a conjecture about affine $\mathbb{Z}$-VASS with infinite matrix monoids we raised in a preliminary version of this paper. We complement this result by presenting an affine $\mathbb{Z}$-VASS with monogenic matrix monoid and undecidable reachability relation.

cs.LO↗

arXiv2021

The Complexity of Reachability in Affine Vector Addition Systems with States

Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. It is natural to question their feasibility for VASS enriched with primitives that typically translate into undecidability. Spurred by this concern, we pinpoint the complexity of integer relaxations with respect to arbitrary classes of affine operations. More specifically, we provide a trichotomy on the complexity of integer reachability in VASS extended with affine operations (affine VASS). Namely, we show that it is NP-complete for VASS with resets, PSPACE-complete for VASS with (pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any other class. We further present a dichotomy for standard reachability in affine VASS: it is decidable for VASS with permutations, and undecidable for any other class. This yields a complete and unified complexity landscape of reachability in affine VASS. We also consider the reachability problem parameterized by a fixed affine VASS, rather than a class, and we show that the complexity landscape is arbitrary in this setting.

cs.LO↗

arXiv2021

Continuous One-Counter Automata

We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: (1) We prove that the reachability problem for COCA with global upper and lower bound tests is in NC2; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is decidable in the polynomial hierarchy for COCA with parametric counter updates and bound tests.

cs.FL↗

arXiv2020

Directed Reachability for Infinite-State Systems

Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as A* and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis.

cs.LO↗

arXiv2020

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling

We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.

cs.LO↗

arXiv2020

Forward Analysis for WSTS, Part III: Karp-Miller Trees

This paper is a sequel of "Forward Analysis for WSTS, Part I: Completions" [STACS 2009, LZI Intl. Proc. in Informatics 3, 433-444] and "Forward Analysis for WSTS, Part II: Complete WSTS" [Logical Methods in Computer Science 8(3), 2012]. In these two papers, we provided a framework to conduct forward reachability analyses of WSTS, using finite representations of downward-closed sets. We further develop this framework to obtain a generic Karp-Miller algorithm for the new class of very-WSTS. This allows us to show that coverability sets of very-WSTS can be computed as their finite ideal decompositions. Under natural effectiveness assumptions, we also show that LTL model checking for very-WSTS is decidable. The termination of our procedure rests on a new notion of acceleration levels, which we study. We characterize those domains that allow for only finitely many accelerations, based on ordinal ranks.

cs.LO↗

arXiv2020

Succinct Population Protocols for Presburger Arithmetic

Angluin et al. proved that population protocols compute exactly the predicates definable in Presburger arithmetic (PA), the first-order theory of addition. As part of this result, they presented a procedure that translates any formula $φ$ of quantifier-free PA with remainder predicates (which has the same expressive power as full PA) into a population protocol with $2^{O(\text{poly}(|φ|))}$ states that computes $φ$. More precisely, the number of states of the protocol is exponential in both the bit length of the largest coefficient in the formula, and the number of nodes of its syntax tree. In this paper, we prove that every formula $φ$ of quantifier-free PA with remainder predicates is computable by a leaderless population protocol with $O(\text{poly}(|φ|))$ states. Our proof is based on several new constructions, which may be of independent interest. Given a formula $φ$ of quantifier-free PA with remainder predicates, a first construction produces a succinct protocol (with $O(|φ|^3)$ leaders) that computes $φ$; this completes the work initiated in [STACS'18], where we constructed such protocols for a fragment of PA. For large enough inputs, we can get rid of these leaders. If the input is not large enough, then it is small, and we design another construction producing a succinct protocol with one leader that computes $φ$. Our last construction gets rid of this leader for small inputs.

cs.DC↗

arXiv2019

Expressive Power of Broadcast Consensus Protocols

Population protocols are a formal model of computation by identical, anonymous mobile agents interacting in pairs. Their computational power is rather limited: Angluin et al. have shown that they can only compute the predicates over $\mathbb{N}^k$ expressible in Presburger arithmetic. For this reason, several extensions of the model have been proposed, including the addition of devices called cover-time services, absence detectors, and clocks. All these extensions increase the expressive power to the class of predicates over $\mathbb{N}^k$ lying in the complexity class NL when the input is given in unary. However, these devices are difficult to implement, since they require that an agent atomically receives messages from all other agents in a population of unknown size; moreover, the agent must know that they have all been received. Inspired by the work of the verification community on Emerson and Namjoshi's broadcast protocols, we show that NL-power is also achieved by extending population protocols with reliable broadcasts, a simpler, standard communication primitive.

cs.DC↗

arXiv2018

Towards Efficient Verification of Population Protocols

Population protocols are a well established model of computation by anonymous, identical finite state agents. A protocol is well-specified if from every initial configuration, all fair executions reach a common consensus. The central verification question for population protocols is the well-specification problem: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is EXPSPACE-hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class WS3 of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that WS3 has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership problem for WS3 reduces to solving boolean combinations of linear constraints over N. This allowed us to develop the first software able to automatically prove well-specification for all of the infinitely many possible inputs.

cs.LO↗

arXiv2018

Automatic Analysis of Expected Termination Time for Population Protocols

Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions in which the interacting devices are chosen uniformly at random. In well designed population protocols, for every initial configuration of devices, and for every computation starting at this configuration, all devices eventually agree on a consensus value. We address the problem of automatically computing a parametric bound on the expected time the protocol needs to reach this consensus. We present the first algorithm that, when successful, outputs a function f(n) such that the expected time to consensus is bound by O(f(n)), where n is the number of devices executing the protocol. We experimentally show that our algorithm terminates and provides good bounds for many of the protocols found in the literature.

cs.LO↗