Search Results

Documents authored by Esparza, Javier

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.19
Computing Inductive Invariants of Regular Abstraction Frameworks

Authors: Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
Regular transition systems (RTS) are a popular formalism for modeling infinite-state systems in general, and parameterised systems in particular. In a CONCUR 22 paper, Esparza et al. introduce a novel approach to the verification of RTS, based on inductive invariants. The approach computes the intersection of all inductive invariants of a given RTS that can be expressed as CNF formulas with a bounded number of clauses, and uses it to construct an automaton recognising an overapproximation of the reachable configurations. The paper shows that the problem of deciding if the language of this automaton intersects a given regular set of unsafe configurations is in EXPSPACE and PSPACE-hard. We introduce regular abstraction frameworks, a generalisation of the approach of Esparza et al., very similar to the regular abstractions of Hong and Lin. A framework consists of a regular language of constraints, and a transducer, called the interpretation, that assigns to each constraint the set of configurations of the RTS satisfying it. Examples of regular abstraction frameworks include the formulas of Esparza et al., octagons, bounded difference matrices, and views. We show that the generalisation of the decision problem above to regular abstraction frameworks remains in EXPSPACE, and prove a matching (non-trivial) EXPSPACE-hardness bound. EXPSPACE-hardness implies that, in the worst case, the automaton recognising the overapproximation of the reachable configurations has a double-exponential number of states. We introduce a learning algorithm that computes this automaton in a lazy manner, stopping whenever the current hypothesis is already strong enough to prove safety. We report on an implementation and show that our experimental results improve on those of Esparza et al.
Cite as

Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr. Computing Inductive Invariants of Regular Abstraction Frameworks. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{czerner_et_al:LIPIcs.CONCUR.2024.19,
  author =	{Czerner, Philipp and Esparza, Javier and Krasotin, Valentin and Welzel-Mohr, Christoph},
  title =	{{Computing Inductive Invariants of Regular Abstraction Frameworks}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.19},
  URN =		{urn:nbn:de:0030-drops-207919},
  doi =		{10.4230/LIPIcs.CONCUR.2024.19},
  annote =	{Keywords: Regular model checking, abstraction, inductive invariants}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.24
Validity of Contextual Formulas

Authors: Javier Esparza and Rubén Rubio

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
Many well-known logical identities are naturally written as equivalences between contextual formulas. A simple example is the Boole-Shannon expansion c[p] ≡ (p ∧ c[true]) ∨ (¬ p ∧ c[false]), where c denotes an arbitrary formula with possibly multiple occurrences of a "hole", called a context, and c[φ] denotes the result of "filling" all holes of c with the formula φ. Another example is the unfolding rule μX.c[X] ≡ c[μX.c[X]] of the modal μ-calculus. We consider the modal μ-calculus as overarching temporal logic and, as usual, reduce the problem whether φ₁ ≡ φ₂ holds for contextual formulas φ₁, φ₂ to the problem whether φ₁ ↔ φ₂ is valid. We show that the problem whether a contextual formula of the μ-calculus is valid for all contexts can be reduced to validity of ordinary formulas. Our first result constructs a canonical context such that a formula is valid for all contexts iff it is valid for this particular one. However, the ordinary formula is exponential in the nesting-depth of the context variables. In a second result we solve this problem, thus proving that validity of contextual formulas is EXP-complete, as for ordinary equivalences. We also prove that both results hold for CTL and LTL as well. We conclude the paper with some experimental results. In particular, we use our implementation to automatically prove the correctness of a set of six contextual equivalences of LTL recently introduced by Esparza et al. for the normalization of LTL formulas. While Esparza et al. need several pages of manual proof, our tool only needs milliseconds to do the job and to compute counterexamples for incorrect variants of the equivalences.
Cite as

Javier Esparza and Rubén Rubio. Validity of Contextual Formulas. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2024.24,
  author =	{Esparza, Javier and Rubio, Rub\'{e}n},
  title =	{{Validity of Contextual Formulas}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{24:1--24:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.24},
  URN =		{urn:nbn:de:0030-drops-207965},
  doi =		{10.4230/LIPIcs.CONCUR.2024.24},
  annote =	{Keywords: \mu-calculus, temporal logic, contextual rules}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.6
Geometry of Reachability Sets of Vector Addition Systems

Authors: Roland Guttenberg, Mikhail Raskin, and Javier Esparza

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
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 configuration. Leroux has studied the geometric properties of VAS reachability sets, and used them to derive decision procedures for important analysis problems. In this paper we continue the geometric study of reachability sets. We show that every reachability set admits a finite decomposition into disjoint almost hybridlinear sets enjoying nice geometric properties. Further, we prove that the decomposition of the reachability set of a given VAS is effectively computable. As a corollary, we derive a new proof of Hauschildt’s 1990 result showing the decidability of the question whether the reachability set of a given VAS is semilinear. As a second corollary, we prove that the complement of a reachability set, if it is infinite, always contains an infinite linear set.
Cite as

Roland Guttenberg, Mikhail Raskin, and Javier Esparza. Geometry of Reachability Sets of Vector Addition Systems. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{guttenberg_et_al:LIPIcs.CONCUR.2023.6,
  author =	{Guttenberg, Roland and Raskin, Mikhail and Esparza, Javier},
  title =	{{Geometry of Reachability Sets of Vector Addition Systems}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.6},
  URN =		{urn:nbn:de:0030-drops-190005},
  doi =		{10.4230/LIPIcs.CONCUR.2023.6},
  annote =	{Keywords: Vector Addition System, Petri net, Reachability Set, Almost hybridlinear, Partition, Geometry}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.126
Black-Box Testing Liveness Properties of Partially Observable Stochastic Systems

Authors: Javier Esparza and Vincent P. Grande

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We study black-box testing for stochastic systems and arbitrary ω-regular specifications, explicitly including liveness properties. We are given a finite-state probabilistic system that we can only execute from the initial state. We have no information on the number of reachable states, or on the probabilities; further, we can only partially observe the states. The only action we can take is to restart the system. We design restart strategies guaranteeing that, if the specification is violated with non-zero probability, then w.p.1 the number of restarts is finite, and the infinite run executed after the last restart violates the specification. This improves on previous work that required full observability. We obtain asymptotically optimal upper bounds on the expected number of steps until the last restart. We conduct experiments on a number of benchmarks, and show that our strategies allow one to find violations in Markov chains much larger than the ones considered in previous work.
Cite as

Javier Esparza and Vincent P. Grande. Black-Box Testing Liveness Properties of Partially Observable Stochastic Systems. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 126:1-126:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.ICALP.2023.126,
  author =	{Esparza, Javier and Grande, Vincent P.},
  title =	{{Black-Box Testing Liveness Properties of Partially Observable Stochastic Systems}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{126:1--126:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.126},
  URN =		{urn:nbn:de:0030-drops-181785},
  doi =		{10.4230/LIPIcs.ICALP.2023.126},
  annote =	{Keywords: Partially observable Markov chains, \omega-regular properties, black-box testing}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.23
Regular Model Checking Upside-Down: An Invariant-Based Approach

Authors: Javier Esparza, Mikhail Raskin, and Christoph Welzel

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
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. It applies to systems whose set of initial configurations is regular, and whose transition relation is captured by a length-preserving transducer. To verify safety properties, regular model checking iteratively computes automata recognizing increasingly larger regular sets of reachable configurations, and checks if they contain unsafe configurations. Since this procedure often does not terminate, acceleration, abstraction, and widening techniques have been developed to compute a regular superset of the reachable configurations. In this paper we develop a complementary procedure. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and approach it from above. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since this intersection is non-regular in general, we introduce b-bounded invariants, defined as those representable by CNF-formulas with at most b clauses. We prove that, for every b ≥ 0, the intersection of all b-bounded inductive invariants is regular, and we construct an automaton recognizing it. We show that whether this automaton accepts some unsafe configuration is in EXPSPACE for every b ≥ 0, and PSPACE-complete for b = 1. Finally, we study how large must b be to prove safety properties of a number of benchmarks.
Cite as

Javier Esparza, Mikhail Raskin, and Christoph Welzel. Regular Model Checking Upside-Down: An Invariant-Based Approach. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2022.23,
  author =	{Esparza, Javier and Raskin, Mikhail and Welzel, Christoph},
  title =	{{Regular Model Checking Upside-Down: An Invariant-Based Approach}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{23:1--23:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.23},
  URN =		{urn:nbn:de:0030-drops-170862},
  doi =		{10.4230/LIPIcs.CONCUR.2022.23},
  annote =	{Keywords: parameterized verification, structural analysis, regular languages, regular model-checking, traps}
}
Document
DOI: 10.4230/LIPIcs.SAND.2022.11
Fast and Succinct Population Protocols for Presburger Arithmetic

Authors: Philipp Czerner, Roland Guttenberg, Martin Helfrich, and Javier Esparza

Published in: LIPIcs, Volume 221, 1st Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2022)

Abstract
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 that decides the predicate. The protocol for a predicate of size m (when expressed as a Boolean combination of threshold and remainder predicates with coefficients in binary) runs in 𝒪(m ⋅ n² log n) expected number of interactions, which is almost optimal in n, the number of interacting agents. However, the number of states of the protocol is exponential in m. This is a problem for natural computing applications, where a state corresponds to a chemical species and it is difficult to implement protocols with many states. Blondin et al. described in STACS 2020 another construction that produces protocols with a polynomial number of states, but exponential expected number of interactions. We present a construction that produces protocols with 𝒪(m) states that run in expected 𝒪(m⁷ ⋅ n²) interactions, optimal in n, for all inputs of size Ω(m). For this, we introduce population computers, a carefully crafted generalization of population protocols easier to program, and show that our computers for Presburger predicates can be translated into fast and succinct population protocols.
Cite as

Philipp Czerner, Roland Guttenberg, Martin Helfrich, and Javier Esparza. Fast and Succinct Population Protocols for Presburger Arithmetic. In 1st Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 221, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{czerner_et_al:LIPIcs.SAND.2022.11,
  author =	{Czerner, Philipp and Guttenberg, Roland and Helfrich, Martin and Esparza, Javier},
  title =	{{Fast and Succinct Population Protocols for Presburger Arithmetic}},
  booktitle =	{1st Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2022)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-224-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{221},
  editor =	{Aspnes, James and Michail, Othon},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAND.2022.11},
  URN =		{urn:nbn:de:0030-drops-159535},
  doi =		{10.4230/LIPIcs.SAND.2022.11},
  annote =	{Keywords: population protocols, fast, succinct, population computers}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2021.2
State Complexity of Population Protocols (Invited Talk)

Authors: Javier Esparza

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
Population protocols were introduced by Angluin et al. in 2004 to study the theoretical properties of networks of mobile sensors with very limited computational resources. They have also been proposed as a natural computing model, with molecules, cells, or microorganisms playing the role of sensors. In a population protocol an arbitrary number of indistinguishable, finite-state agents interact randomly in pairs to collectively decide if their initial global configuration satisfies a given property. The property is formalized as a predicate that maps each initial configuration to an output, 0 or 1. Starting from an initial configuration, the agents eventually agree to the correct output almost surely, and continue producing it forever. The protocol is said to stabilize to the correct output. It is well known that population protocols can decide exactly the semilinear predicates, or, equivalently, the predicates expressible in Presburger arithmetic. Current research concentrates on investigating the amount of resources needed to decide a given predicate. The standard resources, time and memory, translate for population protocols into expected time to stabilization, usually called parallel runtime, and number of states of each agent. In this talk we concentrate on the latter. A variant of population protocols allows for a leader, a distinguished finite-state agent that is added to the initial configuration and, intuitively, helps the other agents to organize the computation. In the last years my collaborators and I have obtained upper and lower bounds for the state complexity of population protocols with and without a leader. Define the state complexity of a predicate as the minimal number of states of a protocol that decides the predicate, and STATE(η) as the maximum state complexity of the predicates of size at most η, where predicates are encoded as quantifier-free formulas of Presburger arithmetic with coefficients written in binary. Using techniques from the theory of Petri nets and Vector Addition Systems, we have shown that STATE(η) is polynomially bounded, even for leaderless protocols; this improves on the exponential bound given in 2004 by Angluin and collaborators. We have also proved that STATE(η) ∈ Ω(log log η) for leaderless protocols, even for those deciding very simple predicates of the form x ≥ c for some constant c. In the talk I report on these results, and on two very recent, still unpublished results. Modulo the pending peer-review confirmation, the first result shows the existence of leaderless protocols with a polynomial number of states and linear parallel runtime, and the second, due to Leroux, gives a Ω((log log η)^{1/3}) lower bound for protocols with a leader.
Cite as

Javier Esparza. State Complexity of Population Protocols (Invited Talk). In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{esparza:LIPIcs.FSTTCS.2021.2,
  author =	{Esparza, Javier},
  title =	{{State Complexity of Population Protocols}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.2},
  URN =		{urn:nbn:de:0030-drops-155139},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.2},
  annote =	{Keywords: Population protocols, state complexity, Petri nets}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.5
Enforcing ω-Regular Properties in Markov Chains by Restarting

Authors: Javier Esparza, Stefan Kiefer, Jan Křetínský, and Maximilian Weininger

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Restarts are used in many computer systems to improve performance. Examples include reloading a webpage, reissuing a request, or restarting a randomized search. The design of restart strategies has been extensively studied by the performance evaluation community. In this paper, we address the problem of designing universal restart strategies, valid for arbitrary finite-state Markov chains, that enforce a given ω-regular property while not knowing the chain. A strategy enforces a property φ if, with probability 1, the number of restarts is finite, and the run of the Markov chain after the last restart satisfies φ. We design a simple "cautious" strategy that solves the problem, and a more sophisticated "bold" strategy with an almost optimal number of restarts.
Cite as

Javier Esparza, Stefan Kiefer, Jan Křetínský, and Maximilian Weininger. Enforcing ω-Regular Properties in Markov Chains by Restarting. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2021.5,
  author =	{Esparza, Javier and Kiefer, Stefan and K\v{r}et{\'\i}nsk\'{y}, Jan and Weininger, Maximilian},
  title =	{{Enforcing \omega-Regular Properties in Markov Chains by Restarting}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.5},
  URN =		{urn:nbn:de:0030-drops-143824},
  doi =		{10.4230/LIPIcs.CONCUR.2021.5},
  annote =	{Keywords: Markov chains, omega-regular properties, runtime enforcement}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.10
A Classification of Weak Asynchronous Models of Distributed Computing

Authors: Javier Esparza and Fabian Reiter

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
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 satisfies a given graph-theoretical property. Models discussed in the literature differ in the detection capabilities of the agents residing at the nodes of the network (detecting the set of states of their neighbors, or counting the number of neighbors in each state), the notion of acceptance (acceptance by halting in a particular configuration, or by stable consensus), the notion of step (synchronous move, interleaving, or arbitrary timing), and the fairness assumptions (non-starving, or stochastic-like). We study the expressive power of the combinations of these features, and show that the initially twenty possible combinations fit into seven equivalence classes. The classification is the consequence of several equi-expressivity results with a clear interpretation. In particular, we show that acceptance by halting configuration only has non-trivial expressive power if it is combined with counting, and that synchronous and interleaving models have the same power as those in which an arbitrary set of nodes can move at the same time. We also identify simple graph properties that distinguish the expressive power of the seven classes.
Cite as

Javier Esparza and Fabian Reiter. A Classification of Weak Asynchronous Models of Distributed Computing. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2020.10,
  author =	{Esparza, Javier and Reiter, Fabian},
  title =	{{A Classification of Weak Asynchronous Models of Distributed Computing}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.10},
  URN =		{urn:nbn:de:0030-drops-128229},
  doi =		{10.4230/LIPIcs.CONCUR.2020.10},
  annote =	{Keywords: Asynchrony, Concurrency theory, Weak models of distributed computing}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.45
Flatness and Complexity of Immediate Observation Petri Nets

Authors: Mikhail Raskin, Chana Weil-Kennedy, and Javier Esparza

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
In a previous paper we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. In the first part of this paper we show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. In the second part we study Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the coverability and reachability problem for BIO nets, and even a certain set-parameterized version of them, are in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.
Cite as

Mikhail Raskin, Chana Weil-Kennedy, and Javier Esparza. Flatness and Complexity of Immediate Observation Petri Nets. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 45:1-45:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{raskin_et_al:LIPIcs.CONCUR.2020.45,
  author =	{Raskin, Mikhail and Weil-Kennedy, Chana and Esparza, Javier},
  title =	{{Flatness and Complexity of Immediate Observation Petri Nets}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{45:1--45:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.45},
  URN =		{urn:nbn:de:0030-drops-128574},
  doi =		{10.4230/LIPIcs.CONCUR.2020.45},
  annote =	{Keywords: Petri Nets, Reachability Analysis, Parameterized Verification, Flattability}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.MFCS.2020
LIPIcs, Volume 170, MFCS 2020, Complete Volume

Authors: Javier Esparza and Daniel Král'

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
LIPIcs, Volume 170, MFCS 2020, Complete Volume
Cite as

45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 1-1216, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Proceedings{esparza_et_al:LIPIcs.MFCS.2020,
  title =	{{LIPIcs, Volume 170, MFCS 2020, Complete Volume}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{1--1216},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020},
  URN =		{urn:nbn:de:0030-drops-126703},
  doi =		{10.4230/LIPIcs.MFCS.2020},
  annote =	{Keywords: LIPIcs, Volume 170, MFCS 2020, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.MFCS.2020.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Javier Esparza and Daniel Král'

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.MFCS.2020.0,
  author =	{Esparza, Javier and Kr\'{a}l', Daniel},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.0},
  URN =		{urn:nbn:de:0030-drops-126714},
  doi =		{10.4230/LIPIcs.MFCS.2020.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.STACS.2020.40
Succinct Population Protocols for Presburger Arithmetic

Authors: Michael Blondin, Javier Esparza, Blaise Genest, Martin Helfrich, and Stefan Jaax

Published in: LIPIcs, Volume 154, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)

Abstract
In [Dana Angluin et al., 2006], Angluin et al. proved that population protocols compute exactly the predicates definable in Presburger arithmetic (PA), the first-order theory of addition. As part of this result, they presented a procedure that translates any formula φ of quantifier-free PA with remainder predicates (which has the same expressive power as full PA) into a population protocol with 2^?(poly(|φ|)) states that computes φ. More precisely, the number of states of the protocol is exponential in both the bit length of the largest coefficient in the formula, and the number of nodes of its syntax tree. In this paper, we prove that every formula φ of quantifier-free PA with remainder predicates is computable by a leaderless population protocol with ?(poly(|φ|)) states. Our proof is based on several new constructions, which may be of independent interest. Given a formula φ of quantifier-free PA with remainder predicates, a first construction produces a succinct protocol (with ?(|φ|³) leaders) that computes φ; this completes the work initiated in [Michael Blondin et al., 2018], where we constructed such protocols for a fragment of PA. For large enough inputs, we can get rid of these leaders. If the input is not large enough, then it is small, and we design another construction producing a succinct protocol with one leader that computes φ. Our last construction gets rid of this leader for small inputs.
Cite as

Michael Blondin, Javier Esparza, Blaise Genest, Martin Helfrich, and Stefan Jaax. Succinct Population Protocols for Presburger Arithmetic. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 40:1-40:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.STACS.2020.40,
  author =	{Blondin, Michael and Esparza, Javier and Genest, Blaise and Helfrich, Martin and Jaax, Stefan},
  title =	{{Succinct Population Protocols for Presburger Arithmetic}},
  booktitle =	{37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)},
  pages =	{40:1--40:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-140-5},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{154},
  editor =	{Paul, Christophe and Bl\"{a}ser, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.40},
  URN =		{urn:nbn:de:0030-drops-119018},
  doi =		{10.4230/LIPIcs.STACS.2020.40},
  annote =	{Keywords: Population protocols, Presburger arithmetic, state complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.31
Expressive Power of Broadcast Consensus Protocols

Authors: Michael Blondin, Javier Esparza, and Stefan Jaax

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Population protocols are a formal model of computation by identical, anonymous mobile agents interacting in pairs. Their computational power is rather limited: Angluin et al. have shown that they can only compute the predicates over N^k expressible in Presburger arithmetic. For this reason, several extensions of the model have been proposed, including the addition of devices called cover-time services, absence detectors, and clocks. All these extensions increase the expressive power to the class of predicates over N^k lying in the complexity class NL when the input is given in unary. However, these devices are difficult to implement, since they require that an agent atomically receives messages from all other agents in a population of unknown size; moreover, the agent must know that they have all been received. Inspired by the work of the verification community on Emerson and Namjoshi’s broadcast protocols, we show that NL-power is also achieved by extending population protocols with reliable broadcasts, a simpler, standard communication primitive.
Cite as

Michael Blondin, Javier Esparza, and Stefan Jaax. Expressive Power of Broadcast Consensus Protocols. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.CONCUR.2019.31,
  author =	{Blondin, Michael and Esparza, Javier and Jaax, Stefan},
  title =	{{Expressive Power of Broadcast Consensus Protocols}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.31},
  URN =		{urn:nbn:de:0030-drops-109330},
  doi =		{10.4230/LIPIcs.CONCUR.2019.31},
  annote =	{Keywords: population protocols, complexity theory, counter machines, distributed computing}
}
Document
DOI: 10.4230/DagRep.8.5.60
Formal Methods and Fault-Tolerant Distributed Comp.: Forging an Alliance (Dagstuhl Seminar 18211)

Authors: Javier Esparza, Pierre Fraignaud, Anca Muscholl, and Sergio Rajsbaum

Published in: Dagstuhl Reports, Volume 8, Issue 5 (2019)

Abstract
The Dagstuhl Seminar "Formal Methods and Fault-Tolerant Distributed Computing: Forging an Alliance" took place May 22-25, 2018. Its goal was to strengthen the interaction between researchers from formal methods and from distributed computing, and help the two communities to better identify common research challenges.
Cite as

Javier Esparza, Pierre Fraignaud, Anca Muscholl, and Sergio Rajsbaum. Formal Methods and Fault-Tolerant Distributed Comp.: Forging an Alliance (Dagstuhl Seminar 18211). In Dagstuhl Reports, Volume 8, Issue 5, pp. 60-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{esparza_et_al:DagRep.8.5.60,
  author =	{Esparza, Javier and Fraignaud, Pierre and Muscholl, Anca and Rajsbaum, Sergio},
  title =	{{Formal Methods and Fault-Tolerant Distributed Comp.: Forging an Alliance (Dagstuhl Seminar 18211)}},
  pages =	{60--79},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{8},
  number =	{5},
  editor =	{Esparza, Javier and Fraignaud, Pierre and Muscholl, Anca and Rajsbaum, Sergio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.5.60},
  URN =		{urn:nbn:de:0030-drops-98933},
  doi =		{10.4230/DagRep.8.5.60},
  annote =	{Keywords: distributed computing, distributed systems, formal verification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.31
Verification of Immediate Observation Population Protocols

Authors: Javier Esparza, Pierre Ganty, Rupak Majumdar, and Chana Weil-Kennedy

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
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 states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. In a previous paper we have shown that the problem whether a given protocol is well-specified and the problem whether it computes a given predicate are decidable. However, in the same paper we prove that both problems are at least as hard as the reachability problem for Petri nets. Since all known algorithms for Petri net reachability have non-primitive recursive complexity, in this paper we restrict attention to immediate observation (IO) population protocols, a class introduced and studied in (Angluin et al., PODC, 2006). We show that both problems are solvable in exponential space for IO protocols. This is the first syntactically defined, interesting class of protocols for which an algorithm not requiring Petri net reachability is found.
Cite as

Javier Esparza, Pierre Ganty, Rupak Majumdar, and Chana Weil-Kennedy. Verification of Immediate Observation Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2018.31,
  author =	{Esparza, Javier and Ganty, Pierre and Majumdar, Rupak and Weil-Kennedy, Chana},
  title =	{{Verification of Immediate Observation Population Protocols}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.31},
  URN =		{urn:nbn:de:0030-drops-95695},
  doi =		{10.4230/LIPIcs.CONCUR.2018.31},
  annote =	{Keywords: Population protocols, Immediate Observation, Parametrized verification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.33
Automatic Analysis of Expected Termination Time for Population Protocols

Authors: Michael Blondin, Javier Esparza, and Antonín Kucera

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
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 infinite sequences of interactions in which the interacting devices are chosen uniformly at random. In well designed population protocols, for every initial configuration of devices, and for every computation starting at this configuration, all devices eventually agree on a consensus value. We address the problem of automatically computing a parametric bound on the expected time the protocol needs to reach this consensus. We present the first algorithm that, when successful, outputs a function f(n) such that the expected time to consensus is bound by O(f(n)), where n is the number of devices executing the protocol. We experimentally show that our algorithm terminates and provides good bounds for many of the protocols found in the literature.
Cite as

Michael Blondin, Javier Esparza, and Antonín Kucera. Automatic Analysis of Expected Termination Time for Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.CONCUR.2018.33,
  author =	{Blondin, Michael and Esparza, Javier and Kucera, Anton{\'\i}n},
  title =	{{Automatic Analysis of Expected Termination Time for Population Protocols}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{33:1--33:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.33},
  URN =		{urn:nbn:de:0030-drops-95711},
  doi =		{10.4230/LIPIcs.CONCUR.2018.33},
  annote =	{Keywords: population protocols, performance analysis, expected termination time}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.16
Large Flocks of Small Birds: on the Minimal Size of Population Protocols

Authors: Michael Blondin, Javier Esparza, and Stefan Jaax

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
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 protocols compute exactly predicates definable in Presburger arithmetic. We initiate the study of the minimal amount of memory required to compute a given predicate as a function of its size. We present results on the predicates x >= n for n \in N, and more generally on the predicates corresponding to systems of linear inequalities. We show that they can be computed by protocols with O(log n) states (or, more generally, logarithmic in the coefficients of the predicate), and that, surprisingly, some families of predicates can be computed by protocols with O(log log n) states. We give essentially matching lower bounds for the class of 1-aware protocols.
Cite as

Michael Blondin, Javier Esparza, and Stefan Jaax. Large Flocks of Small Birds: on the Minimal Size of Population Protocols. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 16:1-16:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.STACS.2018.16,
  author =	{Blondin, Michael and Esparza, Javier and Jaax, Stefan},
  title =	{{Large Flocks of Small Birds: on the Minimal Size of Population Protocols}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{16:1--16:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.16},
  URN =		{urn:nbn:de:0030-drops-85116},
  doi =		{10.4230/LIPIcs.STACS.2018.16},
  annote =	{Keywords: Population protocols, Presburger arithmetic}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2017.2
Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets (Invited Talk)

Authors: Javier Esparza

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
We survey recent results on the development of efficient algorithms for the quantitative analysis of business processes modeled as workflow Petri nets. The algorithms can be applied to any workflow net, but have polynomial runtime in the free-choice case.
Cite as

Javier Esparza. Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets (Invited Talk). In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{esparza:LIPIcs.TIME.2017.2,
  author =	{Esparza, Javier},
  title =	{{Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{2:1--2:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.2},
  URN =		{urn:nbn:de:0030-drops-79266},
  doi =		{10.4230/LIPIcs.TIME.2017.2},
  annote =	{Keywords: Free-choice Petri Nets, concurrency theory, quantitative verification}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.27
Model Checking Population Protocols

Authors: Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
Population protocols are a model for parameterized systems in which a set of identical, anonymous, finite-state processes interact pairwise through rendezvous synchronization. In each step, the pair of interacting processes is chosen by a random scheduler. Angluin et al. (PODC 2004) studied population protocols as a distributed computation model. They characterized the computational power in the limit (semi-linear predicates) of a subclass of protocols (the well-specified ones). However, the modeling power of protocols go beyond computation of semi-linear predicates and they can be used to study a wide range of distributed protocols, such as asynchronous leader election or consensus, stochastic evolutionary processes, or chemical reaction networks. Correspondingly, one is interested in checking specifications on these protocols that go beyond the well-specified computation of predicates. In this paper, we characterize the decidability frontier for the model checking problem for population protocols against probabilistic linear-time specifications. We show that the model checking problem is decidable for qualitative objectives, but as hard as the reachability problem for Petri nets - a well-known hard problem without known elementary algorithms. On the other hand, model checking is undecidable for quantitative properties.
Cite as

Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Model Checking Population Protocols. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.FSTTCS.2016.27,
  author =	{Esparza, Javier and Ganty, Pierre and Leroux, J\'{e}r\^{o}me and Majumdar, Rupak},
  title =	{{Model Checking Population Protocols}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{27:1--27:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.27},
  URN =		{urn:nbn:de:0030-drops-68628},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.27},
  annote =	{Keywords: parameterized systems, population protocols, probabilistic model checking, probabilistic linear-time specifications, decidability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.12
Soundness in Negotiations

Authors: Javier Esparza, Denis Kuperberg, Anca Muscholl, and Igor Walukiewicz

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
Negotiations are a formalism for describing multiparty distributed cooperation. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In a former paper, Esparza and Desel have shown that deciding soundness of a negotiation is PSPACE-complete, and in PTIME if the negotiation is deterministic. They have also provided an algorithm for an intermediate class of acyclic, non-deterministic negotiations, but left the complexity of the soundness problem open. In the first part of this paper we study two further analysis problems for sound acyclic deterministic negotiations, called the race and the omission problem, and give polynomial algorithms. We use these results to provide the first polynomial algorithm for some analysis problems of workflow nets with data previously studied by Trcka, van der Aalst, and Sidorova. In the second part we solve the open question of Esparza and Desel's paper. We show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes.
Cite as

Javier Esparza, Denis Kuperberg, Anca Muscholl, and Igor Walukiewicz. Soundness in Negotiations. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 12:1-12:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2016.12,
  author =	{Esparza, Javier and Kuperberg, Denis and Muscholl, Anca and Walukiewicz, Igor},
  title =	{{Soundness in Negotiations}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{12:1--12:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.12},
  URN =		{urn:nbn:de:0030-drops-61636},
  doi =		{10.4230/LIPIcs.CONCUR.2016.12},
  annote =	{Keywords: Negotiations, workflows, soundness, verification, concurrency}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.470
Verification of Population Protocols

Authors: Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
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 states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. While the predicates computable by well-specified protocols have been extensively studied, the two basic verification problems remain open: is a given protocol well-specified? Does a protocol compute a given predicate? We prove that both problems are decidable. Our results also prove decidability of a natural question about home spaces of Petri nets.
Cite as

Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of Population Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 470-482, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2015.470,
  author =	{Esparza, Javier and Ganty, Pierre and Leroux, J\'{e}r\^{o}me and Majumdar, Rupak},
  title =	{{Verification of Population Protocols}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{470--482},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.470},
  URN =		{urn:nbn:de:0030-drops-53770},
  doi =		{10.4230/LIPIcs.CONCUR.2015.470},
  annote =	{Keywords: Population protocols, Petri nets, parametrized verification}
}
Document
DOI: 10.4230/DagRep.4.3.153
Reachability Problems for Infinite-State Systems (Dagstuhl Seminar 14141)

Authors: Javier Esparza, Alain Finkel, Pierre McKenzie, and Joel Ouaknine

Published in: Dagstuhl Reports, Volume 4, Issue 3 (2014)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14141 "Reachability Problems for Infinite-State Systems", held from March 30th until April 4th, 2014. The seminar gathered 44 participants and the program consisted of 34 presentations. Participants were asked to contribute open questions prior and during the seminar. A list of these open questions appears in a separate section of the present report. This list generated collaborations among participants and gave rise to research publications solving (partially), for example, question 5.13, namely "what functions are computable by VASS?"
Cite as

Javier Esparza, Alain Finkel, Pierre McKenzie, and Joel Ouaknine. Reachability Problems for Infinite-State Systems (Dagstuhl Seminar 14141). In Dagstuhl Reports, Volume 4, Issue 3, pp. 153-180, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{esparza_et_al:DagRep.4.3.153,
  author =	{Esparza, Javier and Finkel, Alain and McKenzie, Pierre and Ouaknine, Joel},
  title =	{{Reachability Problems for Infinite-State Systems (Dagstuhl Seminar 14141)}},
  pages =	{153--180},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{3},
  editor =	{Esparza, Javier and Finkel, Alain and McKenzie, Pierre and Ouaknine, Joel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.3.153},
  URN =		{urn:nbn:de:0030-drops-46121},
  doi =		{10.4230/DagRep.4.3.153},
  annote =	{Keywords: Infinite-State Systems, Reachability Problems, Formal Verification, Well-Structured Transition Systems, Counter Machines, Vector Addition Systems, Timed Systems}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.STACS.2014.1
Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Invited Talk)

Authors: Javier Esparza

Published in: LIPIcs, Volume 25, 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)

Abstract
We survey some results on the automatic verification of parameterized programs without identities. These are systems composed of arbitrarily many components, all of them running exactly the same finite-state program. We discuss the complexity of deciding that no component reaches an unsafe state. The note is addressed at theoretical computer scientists in general.
Cite as

Javier Esparza. Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Invited Talk). In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 25, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{esparza:LIPIcs.STACS.2014.1,
  author =	{Esparza, Javier},
  title =	{{Keeping a Crowd Safe: On the Complexity of Parameterized Verification}},
  booktitle =	{31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)},
  pages =	{1--10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-65-1},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{25},
  editor =	{Mayr, Ernst W. and Portier, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2014.1},
  URN =		{urn:nbn:de:0030-drops-44985},
  doi =		{10.4230/LIPIcs.STACS.2014.1},
  annote =	{Keywords: Parameterized verification, automata theory}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.225
Computation of Summaries Using Net Unfoldings

Authors: Javier Esparza, Loig Jezequel, and Stefan Schwoon

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
We study the following summarization problem: given a parallel composition A=A_1||...||A_n of labelled transition systems communicating with the environment through a distinguished component A_i, efficiently compute a summary S_i such that E||A and E||S_i are trace-equivalent for every environment E. While Si can be computed using elementary automata theory, the resulting algorithm suffers from the state-explosion problem. We present a new, simple but subtle algorithm based on net unfoldings, a partial-order semantics, give some experimental results using an implementation on top of MOLE, and show that our algorithm can handle divergences and compute weighted summaries with minor modifications.
Cite as

Javier Esparza, Loig Jezequel, and Stefan Schwoon. Computation of Summaries Using Net Unfoldings. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 225-236, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.FSTTCS.2013.225,
  author =	{Esparza, Javier and Jezequel, Loig and Schwoon, Stefan},
  title =	{{Computation of Summaries Using Net Unfoldings}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{225--236},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.225},
  URN =		{urn:nbn:de:0030-drops-43759},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.225},
  annote =	{Keywords: Net unfoldings, Concurrent systems, Petri nets}
}
Document
DOI: 10.4230/LIPIcs.STACS.2010.2468
Computing Least Fixed Points of Probabilistic Systems of Polynomials

Authors: Javier Esparza, Andreas Gaiser, and Stefan Kiefer

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

Abstract
We study systems of equations of the form $X_1 = f_1(X_1, \ldots, X_n), \ldots, X_n = f_n(X_1, \ldots, X_n)$ where each $f_i$ is a polynomial with nonnegative coefficients that add up to~$1$. The least nonnegative solution, say~$\mu$, of such equation systems is central to problems from various areas, like physics, biology, computational linguistics and probabilistic program verification. We give a simple and strongly polynomial algorithm to decide whether $\mu=(1,\ldots,1)$ holds. Furthermore, we present an algorithm that computes reliable sequences of lower and upper bounds on~$\mu$, converging linearly to~$\mu$. Our algorithm has these features despite using inexact arithmetic for efficiency. We report on experiments that show the performance of our algorithms.
Cite as

Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing Least Fixed Points of Probabilistic Systems of Polynomials. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 359-370, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.STACS.2010.2468,
  author =	{Esparza, Javier and Gaiser, Andreas and Kiefer, Stefan},
  title =	{{Computing Least Fixed Points of Probabilistic Systems of Polynomials}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{359--370},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2468},
  URN =		{urn:nbn:de:0030-drops-24685},
  doi =		{10.4230/LIPIcs.STACS.2010.2468},
  annote =	{Keywords: Computing fixed points, numerical approximation, stochastic models, branching processes}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2306
On the Memory Consumption of Probabilistic Pushdown Automata

Authors: Tomas Brazdil, Javier Esparza, and Stefan Kiefer

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

Abstract
We investigate the problem of evaluating memory consumption for systems modelled by probabilistic pushdown automata (pPDA). The space needed by a runof a pPDA is the maximal height reached by the stack during the run. Theproblem is motivated by the investigation of depth-first computations that playan important role for space-efficient schedulings of multithreaded programs. We study the computation of both the distribution of the memory consumption and its expectation. For the distribution, we show that a naive method incurs anexponential blow-up, and that it can be avoided using linear equation systems.We also suggest a possibly even faster approximation method.Given~$\varepsilon>0$, these methods allow to compute bounds on the memoryconsumption that are exceeded with a probability of at most~$\varepsilon$. For the expected memory consumption, we show that whether it is infinite can be decided in polynomial time for stateless pPDA (pBPA) and in polynomial space for pPDA. We also provide an iterative method for approximating theexpectation. We show how to compute error bounds of our approximation methodand analyze its convergence speed. We prove that our method convergeslinearly, i.e., the number of accurate bits of the approximation is a linear function of the number of iterations.
Cite as

Tomas Brazdil, Javier Esparza, and Stefan Kiefer. On the Memory Consumption of Probabilistic Pushdown Automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 49-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.FSTTCS.2009.2306,
  author =	{Brazdil, Tomas and Esparza, Javier and Kiefer, Stefan},
  title =	{{On the Memory Consumption of Probabilistic Pushdown Automata}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{49--60},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2306},
  URN =		{urn:nbn:de:0030-drops-23067},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2306},
  annote =	{Keywords: Pushdown automata, probabilistic systems, verification}
}
Document
DOI: 10.4230/LIPIcs.STACS.2008.1351
Convergence Thresholds of Newton's Method for Monotone Polynomial Equations

Authors: Javier Esparza, Stefan Kiefer, and Michael Luttenberger

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract
Monotone systems of polynomial equations (MSPEs) are systems of fixed-point equations $X_1 = f_1(X_1, ldots, X_n),$ $ldots, X_n = f_n(X_1, ldots, X_n)$ where each $f_i$ is a polynomial with positive real coefficients. The question of computing the least non-negative solution of a given MSPE $vec X = vec f(vec X)$ arises naturally in the analysis of stochastic models such as stochastic context-free grammars, probabilistic pushdown automata, and back-button processes. Etessami and Yannakakis have recently adapted Newton's iterative method to MSPEs. In a previous paper we have proved the existence of a threshold $k_{vec f}$ for strongly connected MSPEs, such that after $k_{vec f}$ iterations of Newton's method each new iteration computes at least 1 new bit of the solution. However, the proof was purely existential. In this paper we give an upper bound for $k_{vec f}$ as a function of the minimal component of the least fixed-point $muvec f$ of $vec f(vec X)$. Using this result we show that $k_{vec f}$ is at most single exponential resp. linear for strongly connected MSPEs derived from probabilistic pushdown automata resp. from back-button processes. Further, we prove the existence of a threshold for arbitrary MSPEs after which each new iteration computes at least $1/w2^h$ new bits of the solution, where $w$ and $h$ are the width and height of the DAG of strongly connected components.
Cite as

Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Convergence Thresholds of Newton's Method for Monotone Polynomial Equations. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 289-300, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.STACS.2008.1351,
  author =	{Esparza, Javier and Kiefer, Stefan and Luttenberger, Michael},
  title =	{{Convergence Thresholds of Newton's Method for Monotone Polynomial Equations}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{289--300},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1351},
  URN =		{urn:nbn:de:0030-drops-13516},
  doi =		{10.4230/LIPIcs.STACS.2008.1351},
  annote =	{Keywords: Newton's Method, Fixed-Point Equations, Formal Verification of Software, Probabilistic Pushdown Systems}
}
Document
DOI: 10.4230/DagSemProc.06081.6
Reachability analysis of multithreaded software with asynchronous communication

Authors: Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejcek

Published in: Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)

Abstract
We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) and DPN (dynamic pushdown networks). We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem, which considers only those computation sequences where the (index of the) thread accessing the shared memory is changed at most a fixed given number of times. We provide efficient algorithms for both forward and backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations. This talk is based on joint work with Ahmed Bouajjani, Javier Esparza, and Jan Strejcek that appeared in FSTTCS 2005.
Cite as

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejcek. Reachability analysis of multithreaded software with asynchronous communication. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bouajjani_et_al:DagSemProc.06081.6,
  author =	{Bouajjani, Ahmed and Esparza, Javier and Schwoon, Stefan and Strejcek, Jan},
  title =	{{Reachability analysis of multithreaded software with asynchronous communication}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.6},
  URN =		{urn:nbn:de:0030-drops-7263},
  doi =		{10.4230/DagSemProc.06081.6},
  annote =	{Keywords: Model checking, pushdown systems, concurrency}
}
Document
DOI: 10.4230/DagSemRep.271
Verification of Infinite-state Systems (Dagstuhl Seminar 00141)

Authors: Ahmed Bouajjani and Javier Esparza

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Ahmed Bouajjani and Javier Esparza. Verification of Infinite-state Systems (Dagstuhl Seminar 00141). Dagstuhl Seminar Report 271, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2000)

Copy BibTex To Clipboard

@TechReport{bouajjani_et_al:DagSemRep.271,
  author =	{Bouajjani, Ahmed and Esparza, Javier},
  title =	{{Verification of Infinite-state Systems (Dagstuhl Seminar 00141)}},
  pages =	{1--24},
  ISSN =	{1619-0203},
  year =	{2000},
  type = 	{Dagstuhl Seminar Report},
  number =	{271},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.271},
  URN =		{urn:nbn:de:0030-drops-151568},
  doi =		{10.4230/DagSemRep.271},
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact