52 citations · 267 across the 47 of their papers we have counts for
61 papers
A Uniform Framework for Problems on Context-Free Grammars
Javier Esparza, Peter Rossmanith, Stefan Schwoon
In a paper published in Information Processing Letters in 2000, Bouajjani et al. presented an automata-based approach to a number of elementary problems on context-free grammars. T…
Making Practical: Efficient Interactive Protocols for BDD Algorithms
Eszter Couillard, Philipp Czerner, Javier Esparza +1
We show that interactive protocols between a prover and a verifier, a well-known tool of complexity theory, can be used in practice to certify the correctness of automated reasonin…
A Simple Rewrite System for the Normalization of Linear Temporal Logic
Javier Esparza, Ruben Rubio, Salomon Sickert
In the mid 80s, Lichtenstein, Pnueli, and Zuck showed that every formula of Past LTL (the extension of Linear Temporal Logic with past operators) is equivalent to a conjunction of…
Black-box Testing Liveness Properties of Partially Observable Stochastic Systems
Javier Esparza, Vincent Grande
We study black-box testing for stochastic systems and arbitrary -regular specifications, explicitly including liveness properties. We are given a finite-state probabilistic syst…
Geometry of Reachability sets of Vector Addition Systems
Roland Guttenberg, Mikhail Raskin, Javier Esparza
Vector Addition Systems (VAS), aka Petri nets, are a popular model of concurrency. The reachability set of a VAS is the set of configurations reachable from the initial configurati…
Separators in Continuous Petri Nets
Michael Blondin, Javier Esparza
Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking cannot reach a marking ,…
Regular Model Checking Upside-Down: An Invariant-Based Approach
Javier Esparza, Michael Raskin, Christoph Welzel-Mohr
Regular model checking is a technique for the verification of infinite-state systems whose configurations can be represented as finite words over a suitable alphabet. The form we a…
Fast and Succinct Population Protocols for Presburger Arithmetic
Philipp Czerner, Roland Guttenberg, Martin Helfrich +1
In their 2006 seminal paper in Distributed Computing, Angluin et al. present a construction that, given any Presburger predicate as input, outputs a leaderless population protocol…
Abduction of trap invariants in parameterized systems
Javier Esparza, Mikhail Raskin, Christoph Welzel
In a previous paper we have presented a CEGAR approach for the verification of parameterized systems with an arbitrary number of processes organized in an array or a ring. The tech…
Population Protocols: Beyond Runtime Analysis
Javier Esparza
I survey our recent work on the verification of population protocols and their state complexity.
Computing Parameterized Invariants of Parameterized Petri Nets
Javier Esparza, Mikhail Raskin, Christoph Welzel
A fundamental advantage of Petri net models is the possibility to automatically compute useful system invariants from the syntax of the net. Classical techniques used for this are…
Decision Power of Weak Asynchronous Models of Distributed Computing
Philipp Czerner, Roland Guttenberg, Martin Helfrich +1
Esparza and Reiter have recently conducted a systematic comparative study of models of distributed computing consisting of a network of identical finite-state automata that coopera…
Lower Bounds on the State Complexity of Population Protocols
Philipp Czerner, Javier Esparza, Jérôme Leroux
Population protocols are a model of computation in which an arbitrary number of indistinguishable finite-state agents interact in pairs. The goal of the agents is to decide by stab…
Online Monitoring -Regular Properties in Unknown Markov Chains
Javier Esparza, Stefan Kiefer, Jan Kretinsky +1
We study runtime monitoring of -regular properties. We consider a simple setting in which a run of an unknown finite-state Markov chain is monitored against a fixed…
Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy
A. R. Balasubramanian, Javier Esparza, Mikhail Raskin
In rendez-vous protocols an arbitrarily large number of indistinguishable finite-state agents interact in pairs. The cut-off problem asks if there exists a number such that all…
Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs
Javier Esparza, Martin Helfrich, Stefan Jaax +1
We present a new version of Peregrine, the tool for the analysis and parameterized verification of population protocols introduced in [Blondin et al., CAV'2018]. Population protoco…
A Classification of Weak Asynchronous Models of Distributed Computing
Javier Esparza, Fabian Reiter
We conduct a systematic study of asynchronous models of distributed computing consisting of identical finite-state devices that cooperate in a network to decide if the network sati…
Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
Michael Blondin, Javier Esparza, Martin Helfrich +2
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…
Complexity of Verification and Synthesis of Threshold Automata
A. R. Balasubramanian, Javier Esparza, Marijana Lazic
Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed…
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
Salomon Sickert, Javier Esparza
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formu…
Structural Invariants for the Verification of Systems with Parameterized Architectures
Marius Bozga, Javier Esparza, Radu Iosif +2
We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components commu…
The Complexity of Verifying Population Protocols
Javier Esparza, Stefan Jaax, Mikhail Raskin +1
Population protocols [Angluin et al., PODC, 2004] are a model of distributed computation in which indistinguishable, finite-state agents interact in pairs to decide if their initia…
Succinct Population Protocols for Presburger Arithmetic
Michael Blondin, Javier Esparza, Blaise Genest +2
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,…
Parameterized Analysis of Immediate Observation Petri Nets
Javier Esparza, Mikhail Raskin, Chana Weil-Kennedy
We introduce immediate observation Petri nets, a class of interest in the study of population protocols (a model of distributed computation), and enzymatic chemical networks. In th…