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