activity
20052024
most citedParikh's Theorem: A simple and direct automaton construction

52 citations · 267 across the 47 of their papers we have counts for

collaborators
Showing 2018Show all

6 papers · 1 filter

cs.LO2018

Computing the Expected Execution Time of Probabilistic Workflow Nets

Philipp J. Meyer, Javier Esparza, Philip Offtermatt

Free-Choice Workflow Petri nets, also known as Workflow Graphs, are a popular model in Business Process Modeling. In this paper we introduce Timed Probabilistic Workflow Nets (TPWN…

cs.LO2018★ 1 cited

Verification of Immediate Observation Population Protocols

Javier Esparza, Pierre Ganty, Rupak Majumdar +1

Population protocols (Angluin et al., PODC, 2004) are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their st…

cs.LO2018

Automatic Analysis of Expected Termination Time for Population Protocols

Michael Blondin, Javier Esparza, Antonín Kučera

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 infini…

cs.LO2018★ 29 cited

One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata

Javier Esparza, Jan Kretinsky, Salomon Sickert

We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield…

cs.LO2018

Computing the concurrency threshold of sound free-choice workflow nets

Philipp J. Meyer, Javier Esparza, Hagen Völzer

Workflow graphs extend classical flow charts with concurrent fork and join nodes. They constitute the core of business processing languages such as BPMN or UML Activity Diagrams. T…

cs.DC2018★ 15 cited

Large Flocks of Small Birds: On the Minimal Size of Population Protocols

Michael Blondin, Javier Esparza, Stefan Jaax

Population protocols are a well established model of distributed computation by mobile finite-state agents with very limited storage. A classical result establishes that population…