52 citations · 267 across the 47 of their papers we have counts for
8 papers · 1 filter
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…