
Population Protocols: Beyond Runtime Analysis
I survey our recent work on the verification of population protocols and...
read it

Abduction of trap invariants in parameterized systems
In a previous paper we have presented a CEGAR approach for the verificat...
read it

Computing Parameterized Invariants of Parameterized Petri Nets
A fundamental advantage of Petri net models is the possibility to automa...
read it

Lower Bounds on the State Complexity of Population Protocols
Population protocols are a model of computation in which an arbitrary nu...
read it

Finding CutOffs in Leaderless RendezVous Protocols is Easy
In rendezvous protocols an arbitrarily large number of indistinguishabl...
read it

Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs
We present a new version of Peregrine, the tool for the analysis and par...
read it

Complexity of Verification and Synthesis of Threshold Automata
Threshold automata are a formalism for modeling and analyzing faulttole...
read it

A Classification of Weak Asynchronous Models of Distributed Computing
We conduct a systematic study of asynchronous models of distributed comp...
read it

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
We present a sound and complete method for the verification of qualitati...
read it

An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theore...
read it

Structural Invariants for the Verification of Systems with Parameterized Architectures
We consider parameterized concurrent systems consisting of a finite but ...
read it

The Complexity of Verifying Population Protocols
Population protocols [Angluin et al., PODC, 2004] are a model of distrib...
read it

Succinct Population Protocols for Presburger Arithmetic
Angluin et al. proved that population protocols compute exactly the pred...
read it

Parameterized Analysis of Immediate Observation Petri Nets
We introduce immediate observation Petri nets, a class of interest in th...
read it

Expressive Power of Oblivious Consensus Protocols
Population protocols are a formal model of computation by identical, ano...
read it

Computing the Expected Execution Time of Probabilistic Workflow Nets
FreeChoice Workflow Petri nets, also known as Workflow Graphs, are a po...
read it

Verification of Immediate Observation Population Protocols
Population protocols (Angluin et al., PODC, 2004) are a formal model of ...
read it

Automatic Analysis of Expected Termination Time for Population Protocols
Population protocols are a formal model of sensor networks consisting of...
read it

One Theorem to Rule Them All: A Unified Translation of LTL into ωAutomata
We present a unified translation of LTL formulas into deterministic Rabi...
read it

Computing the concurrency threshold of sound freechoice workflow nets
Workflow graphs extend classical flow charts with concurrent fork and jo...
read it

Large Flocks of Small Birds: On the Minimal Size of Population Protocols
Population protocols are a well established model of distributed computa...
read it
Javier Esparza
is this you? claim profile