|
+
|
Regular Model Checking Upside-Down: An Invariant-Based Approach
|
2025
|
Javier Esparza
Mikhail Raskin
Christoph Welzel-Mohr
|
|
+
PDF
Chat
|
The Black Ninjas and the Sniper: On Robustness of Population Protocols
|
2024
|
Benno Lossin
Philipp Czerner
Javier Esparza
Roland Guttenberg
Tobias Prehn
|
|
+
PDF
Chat
|
Weakly acyclic diagrams: A data structure for infinite-state symbolic
verification
|
2024
|
Michael Blondin
Michaël Cadilhac
Xinyi Cui
Philipp Czerner
Javier Esparza
J. Schulz
|
|
+
PDF
Chat
|
Decidability Issues for Petri Nets -- a survey
|
2024
|
Javier Esparza
Mogens Nielsen
|
|
+
PDF
Chat
|
A Uniform Framework for Problems on Context-Free Grammars
|
2024
|
Javier Esparza
Peter Rossmanith
Stefan Schwoon
|
|
+
PDF
Chat
|
Validity of contextual formulas (extended version)
|
2024
|
Javier Esparza
Rubén Rubio
|
|
+
PDF
Chat
|
Computing Inductive Invariants of Regular Abstraction Frameworks
|
2024
|
Philipp Czerner
Javier Esparza
Valentin Krasotin
Christoph Welzel-Mohr
|
|
+
PDF
Chat
|
Efficient Normalization of Linear Temporal Logic
|
2024
|
Javier Esparza
Rubén Rubio
Salomon Sickert
|
|
+
PDF
Chat
|
Separators in Continuous Petri Nets
|
2024
|
Michael Blondin
Javier Esparza
|
|
+
PDF
Chat
|
A Resolution-Based Interactive Proof System for UNSAT
|
2024
|
Philipp Czerner
Javier Esparza
Valentin Krasotin
|
|
+
PDF
Chat
|
Fast and succinct population protocols for Presburger arithmetic
|
2023
|
Philipp Czerner
Roland Guttenberg
Martin Helfrich
Javier Esparza
|
|
+
PDF
Chat
|
Lower bounds on the state complexity of population protocols
|
2023
|
Philipp Czerner
Javier Esparza
Jérôme Leroux
|
|
+
|
Black-box Testing Liveness Properties of Partially Observable Stochastic Systems
|
2023
|
Javier Esparza
Vincent P. Grande
|
|
+
|
Making $\textsf{IP}=\textsf{PSPACE}$ Practical: Efficient Interactive Protocols for BDD Algorithms
|
2023
|
Eszter Couillard
Philipp Czerner
Javier Esparza
Rupak Majumdar
|
|
+
|
Efficient Normalization of Linear Temporal Logic
|
2023
|
Javier Esparza
Rubén Rubio
Salomon Sickert
|
|
+
PDF
Chat
|
Computing Parameterized Invariants of Parameterized Petri Nets
|
2022
|
Javier Esparza
Mikhail Raskin
Christoph Welzel
|
|
+
|
Fast and Succinct Population Protocols for Presburger Arithmetic
|
2022
|
Philipp Czerner
Roland Guttenberg
Martin Helfrich
Javier Esparza
|
|
+
|
Regular Model Checking Upside-Down: An Invariant-Based Approach
|
2022
|
Javier Esparza
Mikhail Raskin
Christoph Welzel
|
|
+
|
Separators in Continuous Petri Nets
|
2022
|
Michael Blondin
Javier Esparza
|
|
+
PDF
Chat
|
A Simple Rewrite System for the Normalization of Linear Temporal Logic
|
2022
|
Javier Esparza
Rubén Rubio
Salomon Sickert
|
|
+
PDF
Chat
|
Abduction of trap invariants in parameterized systems
|
2021
|
Javier Esparza
Mikhail Raskin
Christoph Welzel
|
|
+
|
Population Protocols: Beyond Runtime Analysis
|
2021
|
Javier Esparza
|
|
+
PDF
Chat
|
Decision Power of Weak Asynchronous Models of Distributed Computing
|
2021
|
Philipp Czerner
Roland Guttenberg
Martin Helfrich
Javier Esparza
|
|
+
PDF
Chat
|
Lower Bounds on the State Complexity of Population Protocols
|
2021
|
Philipp Czerner
Javier Esparza
|
|
+
PDF
Chat
|
The complexity of verifying population protocols
|
2021
|
Javier Esparza
Stefan Jaax
Mikhail Raskin
Chana Weil-Kennedy
|
|
+
PDF
Chat
|
Computing Parameterized Invariants of Parameterized Petri Nets
|
2021
|
Javier Esparza
Mikhail Raskin
Christoph Welzel
|
|
+
PDF
Chat
|
Population Protocols: Beyond Runtime Analysis
|
2021
|
Javier Esparza
|
|
+
|
Lower Bounds on the State Complexity of Population Protocols
|
2021
|
Philipp Czerner
Javier Esparza
Jérôme Leroux
|
|
+
|
Population Protocols: Beyond Runtime Analysis
|
2021
|
Javier Esparza
|
|
+
|
Computing Parameterized Invariants of Parameterized Petri Nets
|
2021
|
Javier Esparza
Mikhail Raskin
Christoph Welzel
|
|
+
|
Online Monitoring ω-Regular Properties in Unknown Markov Chains.
|
2020
|
Javier Esparza
Stefan Kiefer
Jan Křetínský
Maximilian Weininger
|
|
+
|
Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs
|
2020
|
Javier Esparza
Martin Helfrich
Stefan Jaax
Philipp J. Meyer
|
|
+
|
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
|
2020
|
Salomon Sickert
Javier Esparza
|
|
+
|
Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
|
2020
|
Michael Blondin
Javier Esparza
Martin Helfrich
Antonı́n Kučera
Philipp J. Meyer
|
|
+
PDF
Chat
|
Succinct Population Protocols for Presburger Arithmetic
|
2020
|
Michael Blondin
Javier Esparza
Blaise Genest
Martin Helfrich
Stefan Jaax
|
|
+
|
Flatness and Complexity of Immediate Observation Petri Nets
|
2020
|
Mikhail Raskin
Chana Weil-Kennedy
Javier Esparza
|
|
+
|
Complexity of Verification and Synthesis of Threshold Automata
|
2020
|
A. R. Balasubramanian
Javier Esparza
Marijana Lazić
|
|
+
|
A Classification of Weak Asynchronous Models of Distributed Computing
|
2020
|
Javier Esparza
Fabian Reiter
|
|
+
PDF
Chat
|
Complexity of Verification and Synthesis of Threshold Automata
|
2020
|
A. R. Balasubramanian
Javier Esparza
Marijana Lazić
|
|
+
PDF
Chat
|
Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs
|
2020
|
Javier Esparza
Martin Helfrich
Stefan Jaax
Philipp J. Meyer
|
|
+
|
Online Monitoring $ω$-Regular Properties in Unknown Markov Chains
|
2020
|
Javier Esparza
Stefan Kiefer
Jan Křetínský
Maximilian Weininger
|
|
+
|
Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs
|
2020
|
Javier Esparza
Martin Helfrich
Stefan Jaax
Philipp J. Meyer
|
|
+
|
Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
|
2020
|
Michael Blondin
Javier Esparza
Martin Helfrich
Antonı́n Kučera
Philipp J. Meyer
|
|
+
|
Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy
|
2020
|
A. R. Balasubramanian
Javier Esparza
Mikhail Raskin
|
|
+
|
Structural Invariants for the Verification of Systems with Parameterized Architectures
|
2020
|
Marius Bozga
Javier Esparza
Radu Iosif
Joseph Sifakis
Christoph Welzel
|
|
+
|
The Complexity of Verifying Population Protocols
|
2019
|
Javier Esparza
Stefan Jaax
Mikhail Raskin
Chana Weil-Kennedy
|
|
+
|
Parameterized Analysis of Immediate Observation Petri Nets
|
2019
|
Javier Esparza
Mikhail Raskin
Chana Weil-Kennedy
|
|
+
|
Expressive Power of Oblivious Consensus Protocols.
|
2019
|
Michael Blondin
Javier Esparza
Stefan Jaax
|
|
+
PDF
Chat
|
Parameterized Analysis of Immediate Observation Petri Nets
|
2019
|
Javier Esparza
Mikhail Raskin
Chana Weil-Kennedy
|
|
+
|
Expressive Power of Broadcast Consensus Protocols
|
2019
|
Michael Blondin
Javier Esparza
Stefan Jaax
|
|
+
|
Succinct Population Protocols for Presburger Arithmetic
|
2019
|
Michael Blondin
Javier Esparza
Blaise Genest
Martin Helfrich
Stefan Jaax
|
|
+
|
The Complexity of Verifying Population Protocols
|
2019
|
Javier Esparza
Stefan Jaax
Mikhail Raskin
Chana Weil-Kennedy
|
|
+
|
Parameterized Analysis of Immediate Observation Petri Nets
|
2019
|
Javier Esparza
Mikhail Raskin
Chana Weil-Kennedy
|
|
+
|
Computing the Expected Execution Time of Probabilistic Workflow Nets
|
2018
|
Philipp J. Meyer
Javier Esparza
Philip Offtermatt
|
|
+
PDF
Chat
|
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
|
2018
|
Javier Esparza
Jan Křetínský
Salomon Sickert
|
|
+
|
Automatic Analysis of Expected Termination Time for Population Protocols
|
2018
|
Michael Blondin
Javier Esparza
Antonı́n Kučera
|
|
+
PDF
Chat
|
One Theorem to Rule Them All
|
2018
|
Javier Esparza
Jan Křetínský
Salomon Sickert
|
|
+
PDF
Chat
|
One Theorem to Rule Them All: A Unified Translation of LTL into {\omega}-Automata
|
2018
|
Javier Esparza
Jan Křetínský
Salomon Sickert
|
|
+
PDF
Chat
|
Negotiation as concurrency primitive
|
2018
|
Jörg Desel
Javier Esparza
Philipp Hoffmann
|
|
+
|
Computing the concurrency threshold of sound free-choice workflow nets
|
2018
|
Philipp J. Meyer
Javier Esparza
Hagen Völzer
|
|
+
|
Large Flocks of Small Birds: On the Minimal Size of Population Protocols
|
2018
|
Michael Blondin
Javier Esparza
Stefan Jaax
|
|
+
|
Verification of Immediate Observation Population Protocols
|
2018
|
Javier Esparza
Pierre Ganty
Rupak Majumdar
Chana Weil-Kennedy
|
|
+
|
Large Flocks of Small Birds: on the Minimal Size of Population Protocols.
|
2018
|
Michael Blondin
Javier Esparza
Stefan Jaax
|
|
+
|
Automatic Analysis of Expected Termination Time for Population Protocols
|
2018
|
Michael Blondin
Javier Esparza
Antonı́n Kučera
|
|
+
|
Computing the concurrency threshold of sound free-choice workflow nets
|
2018
|
Philipp J. Meyer
Javier Esparza
Hagen Völzer
|
|
+
PDF
Chat
|
Polynomial analysis algorithms for free choice Probabilistic Workflow Nets
|
2017
|
Javier Esparza
Philipp Hoffmann
Ratul Saha
|
|
+
PDF
Chat
|
Towards Efficient Verification of Population Protocols
|
2017
|
Michael Blondin
Javier Esparza
Stefan Jaax
Philipp J. Meyer
|
|
+
|
Static analysis of deterministic negotiations
|
2017
|
Javier Esparza
Anca Muscholl
Igor Walukiewicz
|
|
+
|
Static Analysis of Deterministic Negotiations
|
2017
|
Javier Esparza
Anca Muscholl
Igor Walukiewicz
|
|
+
|
Quantitative Implementation Strategies for Safety Controllers
|
2017
|
Philipp J. Meyer
Matthias Rungger
Michael Luttenberger
Javier Esparza
Majid Zamani
|
|
+
PDF
Chat
|
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
|
2017
|
Javier Esparza
Jan Křetínský
Jean-François Raskin
Salomon Sickert
|
|
+
|
Static Analysis of Deterministic Negotiations
|
2017
|
Javier Esparza
Anca Muscholl
Igor Walukiewicz
|
|
+
|
Soundness in negotiations
|
2017
|
Javier Esparza
Denis Kuperberg
Anca Muscholl
Igor Walukiewicz
|
|
+
PDF
Chat
|
Model checking parameterized asynchronous shared-memory systems
|
2016
|
Antoine Durand-Gasselin
Javier Esparza
Pierre Ganty
Rupak Majumdar
|
|
+
|
Polynomial Analysis Algorithms for Free Choice Probabilistic Workflow Nets
|
2016
|
Javier Esparza
Philipp Hoffmann
Ratul Saha
|
|
+
PDF
Chat
|
Parameterized Verification of Asynchronous Shared-Memory Systems
|
2016
|
Javier Esparza
Pierre Ganty
Rupak Majumdar
|
|
+
|
Reduction Rules for Colored Workflow Nets
|
2016
|
Javier Esparza
Philipp Hoffmann
|
|
+
PDF
Chat
|
Reduction Rules for Colored Workflow Nets
|
2016
|
Javier Esparza
Philipp Hoffmann
|
|
+
PDF
Chat
|
Polynomial Analysis Algorithms for Free Choice Probabilistic Workflow Nets
|
2016
|
Javier Esparza
Philipp Hoffmann
Ratul Saha
|
|
+
|
Reduction Rules for Colored Workflow Nets
|
2016
|
Javier Esparza
Philipp Hoffmann
|
|
+
|
Polynomial Analysis Algorithms for Free Choice Probabilistic Workflow Nets
|
2016
|
Javier Esparza
Philipp Hoffmann
Ratul Saha
|
|
+
|
Negotiation as Concurrency Primitive
|
2016
|
Joerg Desel
Javier Esparza
Philipp Hoffmann
|
|
+
|
Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification
|
2015
|
Javier Esparza
Enrico Tronci
|
|
+
|
Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification
|
2015
|
Javier Esparza
Enrico Tronci
|
|
+
|
Model Checking Parameterized Asynchronous Shared-Memory Systems
|
2015
|
Antoine Durand-Gasselin
Javier Esparza
Pierre Ganty
Rupak Majumdar
|
|
+
PDF
Chat
|
Distributed Markov Chains
|
2014
|
Ratul Saha
Javier Esparza
Sumit Kumar Jha
Madhavan Mukund
P. S. Thiagarajan
|
|
+
|
Negotiation Games (with abstract)
|
2014
|
Javier Esparza
Philipp Hoffmann
|
|
+
|
Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Corrected version) ⋆
|
2014
|
Javier Esparza
|
|
+
|
On Negotiation as Concurrency Primitive II: Deterministic Cyclic Negotiations
|
2014
|
Javier Esparza
Jörg Desel
|
|
+
|
From LTL to Deterministic Automata: A Safraless Compositional Approach
|
2014
|
Javier Esparza
Jan Křetínský
|
|
+
|
Negotiation Games (with abstract)
|
2014
|
Javier Esparza
Philipp Hoffmann
|
|
+
|
Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Corrected version)
|
2014
|
Javier Esparza
|
|
+
|
From LTL to Deterministic Automata: A Safraless Compositional Approach
|
2014
|
Javier Esparza
Jan Křetínský
|
|
+
|
On Negotiation as Concurrency Primitive II: Deterministic Cyclic Negotiations
|
2014
|
Javier Esparza
Jörg Desel
|
|
+
|
On Negotiation as Concurrency Primitive
|
2013
|
Javier Esparza
Joerg Desel
|
|
+
PDF
Chat
|
Computation of summaries using net unfoldings
|
2013
|
Javier Esparza
Loïg Jezequel
Stefan Schwoon
|
|
+
PDF
Chat
|
On Negotiation as Concurrency Primitive
|
2013
|
Javier Esparza
Jörg Desel
|
|
+
PDF
Chat
|
Parameterized Verification of Asynchronous Shared-Memory Systems
|
2013
|
Javier Esparza
Pierre Ganty
Rupak Majumdar
|
|
+
PDF
Chat
|
Computation of summaries using net unfoldings
|
2013
|
Javier Esparza
Loïg Jezequel
Stefan Schwoon
|
|
+
|
Computation of Summaries Using Net Unfoldings
|
2013
|
Javier Esparza
Loïg Jezequel
Stefan Schwoon
|
|
+
|
On Negotiation as Concurrency Primitive
|
2013
|
Javier Esparza
Joerg Desel
|
|
+
PDF
Chat
|
A Perfect Model for Bounded Verification
|
2012
|
Javier Esparza
Pierre Ganty
Rupak Majumdar
|
|
+
|
Deterministic Automata for the (F,G)-fragment of LTL
|
2012
|
Jan Křetínský
Javier Esparza
|
|
+
|
Proving Termination of Probabilistic Programs Using Patterns
|
2012
|
Javier Esparza
Andreas Gaiser
Stefan Kiefer
|
|
+
|
Proving Termination of Probabilistic Programs Using Patterns
|
2012
|
Javier Esparza
Andreas Gaiser
Stefan Kiefer
|
|
+
|
Deterministic Automata for the (F,G)-fragment of LTL
|
2012
|
Jan Křetínský
Javier Esparza
|
|
+
|
Space-efficient scheduling of stochastically generated tasks
|
2011
|
Tomǎš Brázdil
Javier Esparza
Stefan Kiefer
Michael Luttenberger
|
|
+
|
Probabilistic Abstractions with Arbitrary Domains
|
2011
|
Javier Esparza
Andreas Gaiser
|
|
+
PDF
Chat
|
Parikhʼs theorem: A simple and direct automaton construction
|
2011
|
Javier Esparza
Pierre Ganty
Stefan Kiefer
Michael Luttenberger
|
|
+
PDF
Chat
|
Probabilistic Abstractions with Arbitrary Domains
|
2011
|
Javier Esparza
Andreas Gaiser
|
|
+
|
Probabilistic Abstractions with Arbitrary Domains
|
2011
|
Javier Esparza
Andreas Gaiser
|
|
+
|
On least fixed points of systems of positive polynomials
|
2010
|
Javier Esparza
Andreas Gaiser
Stefan Kiefer
|
|
+
|
Stochastic Branching Processes: A Computer Science Perspective
|
2010
|
Javier Esparza
|
|
+
|
Space-efficient scheduling of stochastically generated tasks
|
2010
|
Tomá vs Brázdil
Javier Esparza
Stefan Kiefer
Michael Luttenberger
|
|
+
|
COMPUTING LEAST FIXED POINTS OF PROBABILISTIC SYSTEMS OF POLYNOMIALS
|
2010
|
Javier Esparza
Andreas Gaiser
Stefan Kiefer
|
|
+
|
Computing the Least Fixed Point of Positive Polynomial Systems
|
2010
|
Javier Esparza
Stefan Kiefer
Michael Luttenberger
|
|
+
PDF
Chat
|
Space-Efficient Scheduling of Stochastically Generated Tasks
|
2010
|
Tomǎš Brázdil
Javier Esparza
Stefan Kiefer
Michael Luttenberger
|
|
+
PDF
Chat
|
Computing the Least Fixed Point of Positive Polynomial Systems
|
2010
|
Javier Esparza
Stefan Kiefer
Michael Luttenberger
|
|
+
|
Computing the Least Fixed Point of Positive Polynomial Systems
|
2010
|
Javier Esparza
Stefan Kiefer
Michael Luttenberger
|
|
+
|
Space-efficient scheduling of stochastically generated tasks
|
2010
|
Tomǎš Brázdil
Javier Esparza
Stefan Kiefer
Michael Luttenberger
|
|
+
|
FTOS-Verify: Analysis and Verification of Non-Functional Properties for Fault-Tolerant Systems
|
2009
|
Chih-Hong Cheng
Christian Buckl
Javier Esparza
Alois Knoll
|
|
+
|
Computing Least Fixed Points of Probabilistic Systems of Polynomials
|
2009
|
Javier Esparza
Andreas Gaiser
Stefan Kiefer
|
|
+
PDF
Chat
|
Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness
|
2009
|
Chih-Hong Cheng
Christian Buckl
Javier Esparza
Alois Knoll
|
|
+
|
Solving Fixed-Point Equations on omega-Continuous Semirings.
|
2009
|
Javier Esparza
Stefan Kiefer
Michael Luttenberger
|
|
+
PDF
Chat
|
Approximative Methods for Monotone Systems of Min-Max-Polynomial Equations
|
2008
|
Javier Esparza
Thomas Martin Gawlitza
Stefan Kiefer
Helmut Seidl
|
|
+
|
Newton's Method for omega-Continuous Semirings.
|
2008
|
Javier Esparza
Stefan Kiefer
Michael Luttenberger
|
|
+
|
Convergence Thresholds of Newton's Method for Monotone Polynomial Equations
|
2008
|
Javier Esparza
Stefan Kiefer
Michael Luttenberger
|
|
+
PDF
Chat
|
Model Checking Probabilistic Pushdown Automata
|
2006
|
Javier Esparza
Antonı́n Kučera
Richard Mayr
|
|
+
|
Model checking probabilistic pushdown automata
|
2004
|
Javier Esparza
Antonı́n Kučera
Richard Mayr
|
|
+
|
Zeros of the Whittaker function associated to Coulomb waves
|
1999
|
Javier Esparza
|
|
+
|
A Logical Viewpoint on Process-Algebraic Quotients
|
1999
|
Antonı́n Kučera
Javier Esparza
|
|
+
|
Zeros of the Hankel function of real order out of the principal Riemann sheet
|
1991
|
A. Cruz
Javier Esparza
J. Sesma
|