Publications

Download full bibliography (as BibTex): PaVeS publications

Our previous work in the field of parametrized synthesis and verification: previous work

2022

• 1.

  Bertrand, N., Gramoli, V., Konnov, I., Lazic, M., Tholoniat, P., Widder, J.: Brief Announcement: Holistic Verification of Blockchain Consensus. PODC. pp. 424–426. ACM (2022)
  consensus myown parametrizedverification
  URL: Link

  URLBibTeXEndNote

  @inproceedings{DBLP:conf/podc/0001G0LTW22,
  author = {Bertrand, Nathalie and Gramoli, Vincent and Konnov, Igor and Lazic, Marijana and Tholoniat, Pierre and Widder, Josef},
  booktitle = {PODC},
  keywords = {consensus myown parametrizedverification},
  pages = {424--426},
  publisher = {ACM},
  title = {Brief Announcement: Holistic Verification of Blockchain Consensus},
  year = 2022
  }
  

  %0 Conference Paper
  %1 DBLP:conf/podc/0001G0LTW22
  %A Bertrand, Nathalie
  %A Gramoli, Vincent
  %A Konnov, Igor
  %A Lazic, Marijana
  %A Tholoniat, Pierre
  %A Widder, Josef
  %B PODC
  %D 2022
  %I ACM
  %P 424--426
  %R 10.4230/LIPIcs.DISC.2022.10
  %T Brief Announcement: Holistic Verification of Blockchain Consensus
  %U https://drops.dagstuhl.de/opus/volltexte/2022/17201/
  

• 1.

  Casteigts, A., Raskin, M., Renken, M., Zamaraev, V.: Sharp Thresholds in Random Simple Temporal Graphs. 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). pp. 319–326 (2022)
  myown
  URL: Link

  AbstractURLBibTeXEndNote

  A graph whose edges only appear at certain points in time is called a temporal graph (among other names). Such a graph is temporally connected if each ordered pair of vertices is connected by a path which traverses edges in chronological order (i.e., a temporal path). In this paper, we consider a simple model of random temporal graph, obtained from an Erdös-Rényi random graph G ~ Gn,p by considering a random permutation π of the edges and interpreting the ranks in π as presence times. We give a thorough study of the temporal connectivity of such graphs and derive implications for the existence of several kinds of sparse spanners. It turns out that temporal reachability in this model exhibits a surprisingly regular sequence of thresholds. In particular, we show that, at p = log \($n$\)/n, any fixed pair of vertices can a.a.s. reach each other; at 2 log \($n$\)/n, at least one vertex (and in fact, any fixed vertex) can a.a.s. reach all others; and at 3 log \($n$\)/n, all the vertices can a.a.s. reach each other, i.e., the graph is temporally connected. Furthermore, the graph admits a temporal spanner of size 2n + o(n) as soon as it becomes temporally connected, which is nearly optimal as 2n - 4 is a lower bound. This result is quite significant because temporal graphs do not admit spanners of size O(n) in general (Kempe, Kleinberg, Kumar, STOC 2000). In fact, they do not even always admit spanners of size o(\($n$\) 2) (Axiotis, Fotakis, ICALP 2016). Thus, our result implies that the obstructions found in these works, and more generally, any non-negligible obstruction is statistically insignificant: nearly optimal spanners always exist in random temporal graphs. All the above thresholds are sharp. Carrying the study of temporal spanners a step further, we show that pivotal spanners-i.e., spanners of size 2n - 2 made of two spanning trees glued at a single vertex (one descending in time, the other ascending subsequently)-exist a.a.s. at 4 log \($n$\)/ n, this threshold being also sharp. Finally, we show that optimal spanners (of size 2n - 4) also exist a.a.s. at p = 4 log \($n$\)/n, Whether this value is a sharp threshold is open, we conjecture that it is. For completeness, we compare the above results to existing results in related areas, including edge-ordered graphs, gossip theory, and population protocols, showing that our results can be interpreted in these settings as well, and that in some cases, they improve known results therein. Finally, we discuss an intriguing connection between our results and Janson's celebrated results on percolation in weighted graphs.

  @inproceedings{9719741,
  abstract = {A graph whose edges only appear at certain points in time is called a temporal graph (among other names). Such a graph is temporally connected if each ordered pair of vertices is connected by a path which traverses edges in chronological order (i.e., a temporal path). In this paper, we consider a simple model of random temporal graph, obtained from an Erdös-Rényi random graph G ~ Gn,p by considering a random permutation π of the edges and interpreting the ranks in π as presence times. We give a thorough study of the temporal connectivity of such graphs and derive implications for the existence of several kinds of sparse spanners. It turns out that temporal reachability in this model exhibits a surprisingly regular sequence of thresholds. In particular, we show that, at p = log \($n$\)/n, any fixed pair of vertices can a.a.s. reach each other; at 2 log \($n$\)/n, at least one vertex (and in fact, any fixed vertex) can a.a.s. reach all others; and at 3 log \($n$\)/n, all the vertices can a.a.s. reach each other, i.e., the graph is temporally connected. Furthermore, the graph admits a temporal spanner of size 2n + o(n) as soon as it becomes temporally connected, which is nearly optimal as 2n - 4 is a lower bound. This result is quite significant because temporal graphs do not admit spanners of size O(n) in general (Kempe, Kleinberg, Kumar, STOC 2000). In fact, they do not even always admit spanners of size o(\($n$\) 2) (Axiotis, Fotakis, ICALP 2016). Thus, our result implies that the obstructions found in these works, and more generally, any non-negligible obstruction is statistically insignificant: nearly optimal spanners always exist in random temporal graphs. All the above thresholds are sharp. Carrying the study of temporal spanners a step further, we show that pivotal spanners-i.e., spanners of size 2n - 2 made of two spanning trees glued at a single vertex (one descending in time, the other ascending subsequently)-exist a.a.s. at 4 log \($n$\)/ n, this threshold being also sharp. Finally, we show that optimal spanners (of size 2n - 4) also exist a.a.s. at p = 4 log \($n$\)/n, Whether this value is a sharp threshold is open, we conjecture that it is. For completeness, we compare the above results to existing results in related areas, including edge-ordered graphs, gossip theory, and population protocols, showing that our results can be interpreted in these settings as well, and that in some cases, they improve known results therein. Finally, we discuss an intriguing connection between our results and Janson's celebrated results on percolation in weighted graphs.},
  author = {Casteigts, Arnaud and Raskin, Michael and Renken, Malte and Zamaraev, Viktor},
  booktitle = {2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS)},
  keywords = {myown},
  month = {feb},
  pages = {319-326},
  title = {Sharp Thresholds in Random Simple Temporal Graphs},
  year = 2022
  }
  

  %0 Conference Paper
  %1 9719741
  %A Casteigts, Arnaud
  %A Raskin, Michael
  %A Renken, Malte
  %A Zamaraev, Viktor
  %B 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS)
  %D 2022
  %P 319-326
  %R 10.1109/FOCS52979.2021.00040
  %T Sharp Thresholds in Random Simple Temporal Graphs
  %U https://ieeexplore.ieee.org/document/9719741/
  %X A graph whose edges only appear at certain points in time is called a temporal graph (among other names). Such a graph is temporally connected if each ordered pair of vertices is connected by a path which traverses edges in chronological order (i.e., a temporal path). In this paper, we consider a simple model of random temporal graph, obtained from an Erdös-Rényi random graph G ~ Gn,p by considering a random permutation π of the edges and interpreting the ranks in π as presence times. We give a thorough study of the temporal connectivity of such graphs and derive implications for the existence of several kinds of sparse spanners. It turns out that temporal reachability in this model exhibits a surprisingly regular sequence of thresholds. In particular, we show that, at p = log \($n$\)/n, any fixed pair of vertices can a.a.s. reach each other; at 2 log \($n$\)/n, at least one vertex (and in fact, any fixed vertex) can a.a.s. reach all others; and at 3 log \($n$\)/n, all the vertices can a.a.s. reach each other, i.e., the graph is temporally connected. Furthermore, the graph admits a temporal spanner of size 2n + o(n) as soon as it becomes temporally connected, which is nearly optimal as 2n - 4 is a lower bound. This result is quite significant because temporal graphs do not admit spanners of size O(n) in general (Kempe, Kleinberg, Kumar, STOC 2000). In fact, they do not even always admit spanners of size o(\($n$\) 2) (Axiotis, Fotakis, ICALP 2016). Thus, our result implies that the obstructions found in these works, and more generally, any non-negligible obstruction is statistically insignificant: nearly optimal spanners always exist in random temporal graphs. All the above thresholds are sharp. Carrying the study of temporal spanners a step further, we show that pivotal spanners-i.e., spanners of size 2n - 2 made of two spanning trees glued at a single vertex (one descending in time, the other ascending subsequently)-exist a.a.s. at 4 log \($n$\)/ n, this threshold being also sharp. Finally, we show that optimal spanners (of size 2n - 4) also exist a.a.s. at p = 4 log \($n$\)/n, Whether this value is a sharp threshold is open, we conjecture that it is. For completeness, we compare the above results to existing results in related areas, including edge-ordered graphs, gossip theory, and population protocols, showing that our results can be interpreted in these settings as well, and that in some cases, they improve known results therein. Finally, we discuss an intriguing connection between our results and Janson's celebrated results on percolation in weighted graphs.
  

• 1.

  Bertrand, N., Gramoli, V., Konnov, I., Lazic, M., Tholoniat, P., Widder, J.: Holistic Verification of Blockchain Consensus. DISC. pp. 10:1–10:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
  consensus myown parametrizedverification
  URL: Link

  URLBibTeXEndNote

  @inproceedings{DBLP:conf/wdag/0001G0LTW22,
  author = {Bertrand, Nathalie and Gramoli, Vincent and Konnov, Igor and Lazic, Marijana and Tholoniat, Pierre and Widder, Josef},
  booktitle = {DISC},
  keywords = {consensus myown parametrizedverification},
  pages = {10:1--10:24},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  series = {LIPIcs},
  title = {Holistic Verification of Blockchain Consensus},
  volume = 246,
  year = 2022
  }
  

  %0 Conference Paper
  %1 DBLP:conf/wdag/0001G0LTW22
  %A Bertrand, Nathalie
  %A Gramoli, Vincent
  %A Konnov, Igor
  %A Lazic, Marijana
  %A Tholoniat, Pierre
  %A Widder, Josef
  %B DISC
  %D 2022
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %P 10:1--10:24
  %R 10.4230/LIPIcs.DISC.2022.10
  %T Holistic Verification of Blockchain Consensus
  %U https://drops.dagstuhl.de/opus/volltexte/2022/17201/
  %V 246
  

• 1.

  Esparza, J., Raskin, M., Welzel, C.: Regular Model Checking Upside-Down: An Invariant-Based Approach. Presented at the (2022)
  complexity myown parametrizedverification reachability verification
  URL: Link

  URLBibTeXEndNote

  @inproceedings{https://doi.org/10.4230/lipics.concur.2022.23,
  author = {Esparza, Javier and Raskin, Mikhail and Welzel, Christoph},
  keywords = {complexity myown parametrizedverification reachability verification},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title = {Regular Model Checking Upside-Down: An Invariant-Based Approach},
  year = 2022
  }
  

  %0 Conference Paper
  %1 https://doi.org/10.4230/lipics.concur.2022.23
  %A Esparza, Javier
  %A Raskin, Mikhail
  %A Welzel, Christoph
  %D 2022
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %R 10.4230/LIPICS.CONCUR.2022.23
  %T Regular Model Checking Upside-Down: An Invariant-Based Approach
  %U https://drops.dagstuhl.de/opus/volltexte/2022/17086/
  

• 1.

  Czerner, P.: Leaderless Population Protocols Decide Double-exponential Thresholds. CoRR. abs/2204.02115, (2022)
  imported
  URL: Link

  URLBibTeXEndNote

  @article{Czerner22,
  author = {Czerner, Philipp},
  journal = {CoRR},
  keywords = {imported},
  month = {April},
  title = {Leaderless Population Protocols Decide Double-exponential Thresholds},
  volume = {abs/2204.02115},
  year = 2022
  }
  

  %0 Journal Article
  %1 Czerner22
  %A Czerner, Philipp
  %D 2022
  %J CoRR
  %R 10.48550/arXiv.2204.02115
  %T Leaderless Population Protocols Decide Double-exponential Thresholds
  %U https://doi.org/10.48550/arXiv.2204.02115
  %V abs/2204.02115
  

• 1.

  Helfrich, M., vCeška, M., Kvretínsk’y, J., Martivcek, Štefan: Abstraction-Based Segmental Simulation of Chemical Reaction Networks. In: Petre, I. and Puaun, A. (eds.) Computational Methods in Systems Biology. pp. 41–60. Springer International Publishing (2022)
  myown

  AbstractBibTeXEndNote

  Simulating chemical reaction networks is often computationally demanding, in particular due to stiffness. We propose a novel simulation scheme where long runs are not simulated as a whole but assembled from shorter precomputed segments of simulation runs. On the one hand, this speeds up the simulation process to obtain multiple runs since we can reuse the segments. On the other hand, questions on diversity and genuineness of our runs arise. However, we ensure that we generate runs close to their true distribution by generating an appropriate abstraction of the original system and utilizing it in the simulation process. Interestingly, as a by-product, we also obtain a yet more efficient simulation scheme, yielding runs over the system's abstraction. These provide a very faithful approximation of concrete runs on the desired level of granularity, at a low cost. Our experiments demonstrate the speedups in the simulations while preserving key dynamical as well as quantitative properties.

  @inproceedings{10.1007/978-3-031-15034-0_3,
  abstract = {Simulating chemical reaction networks is often computationally demanding, in particular due to stiffness. We propose a novel simulation scheme where long runs are not simulated as a whole but assembled from shorter precomputed segments of simulation runs. On the one hand, this speeds up the simulation process to obtain multiple runs since we can reuse the segments. On the other hand, questions on diversity and genuineness of our runs arise. However, we ensure that we generate runs close to their true distribution by generating an appropriate abstraction of the original system and utilizing it in the simulation process. Interestingly, as a by-product, we also obtain a yet more efficient simulation scheme, yielding runs over the system's abstraction. These provide a very faithful approximation of concrete runs on the desired level of granularity, at a low cost. Our experiments demonstrate the speedups in the simulations while preserving key dynamical as well as quantitative properties.},
  author = {Helfrich, Martin and vCeška, Milan and Kvretínsk'y, Jan and Martivcek, Štefan},
  booktitle = {Computational Methods in Systems Biology},
  editor = {Petre, Ion and Puaun, Andrei},
  keywords = {myown},
  pages = {41--60},
  publisher = {Springer International Publishing},
  title = {Abstraction-Based Segmental Simulation of Chemical Reaction Networks},
  year = 2022
  }
  

  %0 Conference Paper
  %1 10.1007/978-3-031-15034-0_3
  %A Helfrich, Martin
  %A vCeška, Milan
  %A Kvretínsk'y, Jan
  %A Martivcek, Štefan
  %B Computational Methods in Systems Biology
  %D 2022
  %E Petre, Ion
  %E Puaun, Andrei
  %I Springer International Publishing
  %P 41--60
  %R 10.1007/978-3-031-15034-0_3
  %T Abstraction-Based Segmental Simulation of Chemical Reaction Networks
  %X Simulating chemical reaction networks is often computationally demanding, in particular due to stiffness. We propose a novel simulation scheme where long runs are not simulated as a whole but assembled from shorter precomputed segments of simulation runs. On the one hand, this speeds up the simulation process to obtain multiple runs since we can reuse the segments. On the other hand, questions on diversity and genuineness of our runs arise. However, we ensure that we generate runs close to their true distribution by generating an appropriate abstraction of the original system and utilizing it in the simulation process. Interestingly, as a by-product, we also obtain a yet more efficient simulation scheme, yielding runs over the system's abstraction. These provide a very faithful approximation of concrete runs on the desired level of granularity, at a low cost. Our experiments demonstrate the speedups in the simulations while preserving key dynamical as well as quantitative properties.
  %@ 978-3-031-15034-0
  

• 1.

  Czerner, P., Guttenberg, R., Helfrich, M., Esparza, J.: Fast and Succinct Population Protocols for Presburger Arithmetic. In: Aspnes, J. and Michail, O. (eds.) 1st Symposium on Algorithmic Foundations of Dynamic Networks, SAND 2022, March 28-30, 2022, Virtual Conference. pp. 11:1–11:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
  imported
  URL: Link

  URLBibTeXEndNote

  @inproceedings{CzernerGHE22,
  author = {Czerner, Philipp and Guttenberg, Roland and Helfrich, Martin and Esparza, Javier},
  booktitle = {1st Symposium on Algorithmic Foundations of Dynamic Networks, SAND 2022, March 28-30, 2022, Virtual Conference},
  editor = {Aspnes, James and Michail, Othon},
  keywords = {imported},
  month = {April},
  pages = {11:1--11:17},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  series = {LIPIcs},
  title = {Fast and Succinct Population Protocols for Presburger Arithmetic},
  volume = 221,
  year = 2022
  }
  

  %0 Conference Paper
  %1 CzernerGHE22
  %A Czerner, Philipp
  %A Guttenberg, Roland
  %A Helfrich, Martin
  %A Esparza, Javier
  %B 1st Symposium on Algorithmic Foundations of Dynamic Networks, SAND 2022, March 28-30, 2022, Virtual Conference
  %D 2022
  %E Aspnes, James
  %E Michail, Othon
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %P 11:1--11:17
  %R 10.4230/LIPIcs.SAND.2022.11
  %T Fast and Succinct Population Protocols for Presburger Arithmetic
  %U https://doi.org/10.4230/LIPIcs.SAND.2022.11
  %V 221
  

• 1.

  Esparza, J., Raskin, M., Welzel, C.: Regular Model Checking Upside-Down: An Invariant-Based Approach. (2022)
  complexity myown parametrizedverification reachability verification
  URL: Link
  cite arxiv:2205.03060Comment: Submitted to CONCUR’22

  AbstractURLBibTeXEndNote

  Regular model checking is a well-established 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 set of reachable configurations. In this paper we develop a complementary approach. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and compute increasingly smaller regular supersets of it. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since the intersection is in general non-regular, we introduce \($b$\)-bounded invariants, defined as those representable by CNF-formulas with at most \($b$\) clauses. We prove that, for every \($b \geq 0$\), the intersection of all \($b$\)-bounded inductive invariants is regular, and show how to construct an automaton recognizing it. We study the complexity of deciding if this automaton accepts some unsafe configuration. We show that the problem is in textscEXPSPACE for every \($b \geq 0$\), and textscPSPACE-complete for \($b=1$\). Finally, we study how large must \($b$\) be to prove safety properties of a number of benchmarks.

  @article{esparza2022regular,
  abstract = {Regular model checking is a well-established 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 set of reachable configurations. In this paper we develop a complementary approach. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and compute increasingly smaller regular supersets of it. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since the intersection is in general non-regular, we introduce \($b$\)-bounded invariants, defined as those representable by CNF-formulas with at most \($b$\) clauses. We prove that, for every \($b \geq 0$\), the intersection of all \($b$\)-bounded inductive invariants is regular, and show how to construct an automaton recognizing it. We study the complexity of deciding if this automaton accepts some unsafe configuration. We show that the problem is in textscEXPSPACE for every \($b \geq 0$\), and textscPSPACE-complete for \($b=1$\). Finally, we study how large must \($b$\) be to prove safety properties of a number of benchmarks.},
  author = {Esparza, Javier and Raskin, Mikhail and Welzel, Christoph},
  keywords = {complexity myown parametrizedverification reachability verification},
  note = {cite arxiv:2205.03060Comment: Submitted to CONCUR'22},
  title = {Regular Model Checking Upside-Down: An Invariant-Based Approach},
  year = 2022
  }
  

  %0 Journal Article
  %1 esparza2022regular
  %A Esparza, Javier
  %A Raskin, Mikhail
  %A Welzel, Christoph
  %D 2022
  %T Regular Model Checking Upside-Down: An Invariant-Based Approach
  %U http://arxiv.org/abs/2205.03060
  %X Regular model checking is a well-established 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 set of reachable configurations. In this paper we develop a complementary approach. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and compute increasingly smaller regular supersets of it. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since the intersection is in general non-regular, we introduce \($b$\)-bounded invariants, defined as those representable by CNF-formulas with at most \($b$\) clauses. We prove that, for every \($b \geq 0$\), the intersection of all \($b$\)-bounded inductive invariants is regular, and show how to construct an automaton recognizing it. We study the complexity of deciding if this automaton accepts some unsafe configuration. We show that the problem is in textscEXPSPACE for every \($b \geq 0$\), and textscPSPACE-complete for \($b=1$\). Finally, we study how large must \($b$\) be to prove safety properties of a number of benchmarks.
  

• 1.

  Balasubramanian, A.R.: Complexity of Coverability in Depth-Bounded Processes. Presented at the (2022)
  Pi-calculus complexity
  URL: Link

  URLBibTeXEndNote

  @inproceedings{https://doi.org/10.4230/lipics.concur.2022.17,
  author = {Balasubramanian, A. R.},
  keywords = {Pi-calculus complexity},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title = {Complexity of Coverability in Depth-Bounded Processes},
  year = 2022
  }
  

  %0 Conference Paper
  %1 https://doi.org/10.4230/lipics.concur.2022.17
  %A Balasubramanian, A. R.
  %D 2022
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %R 10.4230/LIPICS.CONCUR.2022.17
  %T Complexity of Coverability in Depth-Bounded Processes
  %U https://drops.dagstuhl.de/opus/volltexte/2022/17080/
  

• 1.

  Balasubramanian, A.R., Guillou, L., Weil-Kennedy, C.: Parameterized Analysis of Reconfigurable Broadcast Networks. In: Bouyer, P. and Schröder, L. (eds.) Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. pp. 61–80. Springer (2022)
  broadcastnetworks parameterizedverification
  URL: Link

  URLBibTeXEndNote

  @inproceedings{DBLP:conf/fossacs/Balasubramanian22,
  author = {Balasubramanian, A. R. and Guillou, Lucie and Weil-Kennedy, Chana},
  booktitle = {Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings},
  editor = {Bouyer, Patricia and Schröder, Lutz},
  keywords = {broadcastnetworks parameterizedverification},
  pages = {61--80},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Parameterized Analysis of Reconfigurable Broadcast Networks},
  volume = 13242,
  year = 2022
  }
  

  %0 Conference Paper
  %1 DBLP:conf/fossacs/Balasubramanian22
  %A Balasubramanian, A. R.
  %A Guillou, Lucie
  %A Weil-Kennedy, Chana
  %B Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings
  %D 2022
  %E Bouyer, Patricia
  %E Schröder, Lutz
  %I Springer
  %P 61--80
  %R 10.1007/978-3-030-99253-8\_4
  %T Parameterized Analysis of Reconfigurable Broadcast Networks
  %U https://doi.org/10.1007/978-3-030-99253-8_4
  %V 13242
  

• 1.

  Balasubramanian, A.R.: Coefficient Synthesis for Threshold Automata. In: Lin, A.W., Zetzsche, G., and Potapov, I. (eds.) Reachability Problems - 16th International Conference, RP 2022, Kaiserslautern, Germany, October 17-21, 2022, Proceedings. pp. 125–139. Springer (2022)
  coefficientsynthesis thresholdautomata
  URL: Link

  URLBibTeXEndNote

  @inproceedings{DBLP:conf/rp/Balasubramanian22,
  author = {Balasubramanian, A. R.},
  booktitle = {Reachability Problems - 16th International Conference, RP 2022, Kaiserslautern, Germany, October 17-21, 2022, Proceedings},
  editor = {Lin, Anthony W. and Zetzsche, Georg and Potapov, Igor},
  keywords = {coefficientsynthesis thresholdautomata},
  pages = {125--139},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Coefficient Synthesis for Threshold Automata},
  volume = 13608,
  year = 2022
  }
  

  %0 Conference Paper
  %1 DBLP:conf/rp/Balasubramanian22
  %A Balasubramanian, A. R.
  %B Reachability Problems - 16th International Conference, RP 2022, Kaiserslautern, Germany, October 17-21, 2022, Proceedings
  %D 2022
  %E Lin, Anthony W.
  %E Zetzsche, Georg
  %E Potapov, Igor
  %I Springer
  %P 125--139
  %R 10.1007/978-3-031-19135-0\_9
  %T Coefficient Synthesis for Threshold Automata
  %U https://doi.org/10.1007/978-3-031-19135-0_9
  %V 13608
  

2021

• 1.

  Balasubramanian, A.R., Weil-Kennedy, C.: Reconfigurable Broadcast Networks and Asynchronous Shared-Memory Systems are Equivalent, http://arxiv.org/abs/2109.08315, (2021)
  complexity parameterizedverification
  URL: Link
  cite arxiv:2109.08315Comment: In Proceedings GandALF 2021, arXiv:2109.07798. A long version of this paper, containing all proofs, appears at arXiv:2108.07510

  AbstractURLBibTeXEndNote

  We show the equivalence of two distributed computing models, namely reconfigurable broadcast networks (RBN) and asynchronous shared-memory systems (ASMS), that were introduced independently. Both RBN and ASMS are systems in which a collection of anonymous, finite-state processes run the same protocol. In RBN, the processes communicate by selective broadcast: a process can broadcast a message which is received by all of its neighbors, and the set of neighbors of a process can change arbitrarily over time. In ASMS, the processes communicate by shared memory: a process can either write to or read from a shared register. Our main result is that RBN and ASMS can simulate each other, i.e. they are equivalent with respect to parameterized reachability, where we are given two (possibly infinite) sets of configurations C and C' defined by upper and lower bounds on the number of processes in each state and we would like to decide if some configuration in C can reach some configuration in C'. Using this simulation equivalence, we transfer results of RBN to ASMS and vice versa. Finally, we show that RBN and ASMS can simulate a third distributed model called immediate observation (IO) nets. Moreover, for a slightly stronger notion of simulation (which is satisfied by all the simulations given in this paper), we show that IO nets cannot simulate RBN.

  @misc{balasubramanian2021reconfigurable,
  abstract = {We show the equivalence of two distributed computing models, namely reconfigurable broadcast networks (RBN) and asynchronous shared-memory systems (ASMS), that were introduced independently. Both RBN and ASMS are systems in which a collection of anonymous, finite-state processes run the same protocol. In RBN, the processes communicate by selective broadcast: a process can broadcast a message which is received by all of its neighbors, and the set of neighbors of a process can change arbitrarily over time. In ASMS, the processes communicate by shared memory: a process can either write to or read from a shared register. Our main result is that RBN and ASMS can simulate each other, i.e. they are equivalent with respect to parameterized reachability, where we are given two (possibly infinite) sets of configurations C and C' defined by upper and lower bounds on the number of processes in each state and we would like to decide if some configuration in C can reach some configuration in C'. Using this simulation equivalence, we transfer results of RBN to ASMS and vice versa. Finally, we show that RBN and ASMS can simulate a third distributed model called immediate observation (IO) nets. Moreover, for a slightly stronger notion of simulation (which is satisfied by all the simulations given in this paper), we show that IO nets cannot simulate RBN.},
  author = {Balasubramanian, A. R. and Weil-Kennedy, Chana},
  keywords = {complexity parameterizedverification},
  note = {cite arxiv:2109.08315Comment: In Proceedings GandALF 2021, arXiv:2109.07798. A long version of this paper, containing all proofs, appears at arXiv:2108.07510},
  title = {Reconfigurable Broadcast Networks and Asynchronous Shared-Memory Systems are Equivalent},
  year = 2021
  }
  

  %0 Generic
  %1 balasubramanian2021reconfigurable
  %A Balasubramanian, A. R.
  %A Weil-Kennedy, Chana
  %D 2021
  %R 10.4204/EPTCS.346.2
  %T Reconfigurable Broadcast Networks and Asynchronous Shared-Memory Systems are Equivalent
  %U http://arxiv.org/abs/2109.08315
  %X We show the equivalence of two distributed computing models, namely reconfigurable broadcast networks (RBN) and asynchronous shared-memory systems (ASMS), that were introduced independently. Both RBN and ASMS are systems in which a collection of anonymous, finite-state processes run the same protocol. In RBN, the processes communicate by selective broadcast: a process can broadcast a message which is received by all of its neighbors, and the set of neighbors of a process can change arbitrarily over time. In ASMS, the processes communicate by shared memory: a process can either write to or read from a shared register. Our main result is that RBN and ASMS can simulate each other, i.e. they are equivalent with respect to parameterized reachability, where we are given two (possibly infinite) sets of configurations C and C' defined by upper and lower bounds on the number of processes in each state and we would like to decide if some configuration in C can reach some configuration in C'. Using this simulation equivalence, we transfer results of RBN to ASMS and vice versa. Finally, we show that RBN and ASMS can simulate a third distributed model called immediate observation (IO) nets. Moreover, for a slightly stronger notion of simulation (which is satisfied by all the simulations given in this paper), we show that IO nets cannot simulate RBN.
  

• 1.

  Blondin, M., Haase, C., Mazowiecki, F., Raskin, M.: Affine Extensions of Integer Vector Addition Systems with States. Logical Methods in Computer Science. Volume 17, Issue 3, (2021)
  myown
  URL: Link

  URLBibTeXEndNote

  @article{Blondin_2021,
  author = {Blondin, Michael and Haase, Christoph and Mazowiecki, Filip and Raskin, Mikhail},
  journal = {Logical Methods in Computer Science},
  keywords = {myown},
  month = {jul},
  publisher = {Centre pour la Communication Scientifique Directe (CCSD)},
  title = {Affine Extensions of Integer Vector Addition Systems with States},
  volume = {Volume 17, Issue 3},
  year = 2021
  }
  

  %0 Journal Article
  %1 Blondin_2021
  %A Blondin, Michael
  %A Haase, Christoph
  %A Mazowiecki, Filip
  %A Raskin, Mikhail
  %D 2021
  %I Centre pour la Communication Scientifique Directe (CCSD)
  %J Logical Methods in Computer Science
  %R 10.46298/lmcs-17(3:1)2021
  %T Affine Extensions of Integer Vector Addition Systems with States
  %U https://doi.org/10.46298%2Flmcs-17%283%3A1%292021
  %V Volume 17, Issue 3
  

• 1.

  Czerner, P., Guttenberg, R., Helfrich, M., Esparza, J.: Decision Power of Weak Asynchronous Models of Distributed Computing. In: Miller, A., Censor-Hillel, K., and Korhonen, J.H. (eds.) PODC ’21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021. pp. 115–125. ACM (2021)
  imported

  BibTeXEndNote

  @inproceedings{CzernerGHE21,
  author = {Czerner, Philipp and Guttenberg, Roland and Helfrich, Martin and Esparza, Javier},
  booktitle = {PODC '21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021},
  editor = {Miller, Avery and Censor-Hillel, Keren and Korhonen, Janne H.},
  keywords = {imported},
  month = {July},
  pages = {115--125},
  publisher = {ACM},
  title = {Decision Power of Weak Asynchronous Models of Distributed Computing},
  year = 2021
  }
  

  %0 Conference Paper
  %1 CzernerGHE21
  %A Czerner, Philipp
  %A Guttenberg, Roland
  %A Helfrich, Martin
  %A Esparza, Javier
  %B PODC '21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021
  %D 2021
  %E Miller, Avery
  %E Censor-Hillel, Keren
  %E Korhonen, Janne H.
  %I ACM
  %P 115--125
  %R 10.1145/3465084.3467918
  %T Decision Power of Weak Asynchronous Models of Distributed Computing
  

• 1.

  Balasubramanian, A.R., Thejaswini, K.S.: Adaptive Synchronisation of Pushdown Automata. Presented at the (2021)
  pushdownautomata synchronisation
  URL: Link

  URLBibTeXEndNote

  @inproceedings{https://doi.org/10.4230/lipics.concur.2021.17,
  author = {Balasubramanian, A. R. and Thejaswini, K. S.},
  keywords = {pushdownautomata synchronisation},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title = {Adaptive Synchronisation of Pushdown Automata},
  year = 2021
  }
  

  %0 Conference Paper
  %1 https://doi.org/10.4230/lipics.concur.2021.17
  %A Balasubramanian, A. R.
  %A Thejaswini, K. S.
  %D 2021
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %R 10.4230/LIPICS.CONCUR.2021.17
  %T Adaptive Synchronisation of Pushdown Automata
  %U https://drops.dagstuhl.de/opus/volltexte/2021/14394/
  

• 1.

  Balasubramanian, A.R.: Complexity of Coverability in Bounded Path Broadcast Networks. Presented at the (2021)
  broadcastnetworks complexity parameterizedverification
  URL: Link

  URLBibTeXEndNote

  @inproceedings{https://doi.org/10.4230/lipics.fsttcs.2021.35,
  author = {Balasubramanian, A. R.},
  keywords = {broadcastnetworks complexity parameterizedverification},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title = {Complexity of Coverability in Bounded Path Broadcast Networks},
  year = 2021
  }
  

  %0 Conference Paper
  %1 https://doi.org/10.4230/lipics.fsttcs.2021.35
  %A Balasubramanian, A. R.
  %D 2021
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %R 10.4230/LIPICS.FSTTCS.2021.35
  %T Complexity of Coverability in Bounded Path Broadcast Networks
  %U https://drops.dagstuhl.de/opus/volltexte/2021/15546/
  

• 1.

  Raskin, M.: Population Protocols with Unreliable Communication. Algorithms for Sensor Systems. pp. 140–154. Springer International Publishing (2021)
  myown
  URL: Link

  URLBibTeXEndNote

  @incollection{Raskin_2021,
  author = {Raskin, Mikhail},
  booktitle = {Algorithms for Sensor Systems},
  keywords = {myown},
  pages = {140--154},
  publisher = {Springer International Publishing},
  title = {Population Protocols with Unreliable Communication},
  year = 2021
  }
  

  %0 Book Section
  %1 Raskin_2021
  %A Raskin, Mikhail
  %B Algorithms for Sensor Systems
  %D 2021
  %I Springer International Publishing
  %P 140--154
  %R 10.1007/978-3-030-89240-1_10
  %T Population Protocols with Unreliable Communication
  %U https://doi.org/10.1007%2F978-3-030-89240-1_10
  

• 1.

  Blondin, M., Raskin, M.: The Complexity of Reachability in Affine Vector Addition Systems with States. Logical Methods in Computer Science. Volume 17, Issue 3, (2021)
  myown
  URL: Link

  URLBibTeXEndNote

  @article{Blondin_2021,
  author = {Blondin, Michael and Raskin, Mikhail},
  journal = {Logical Methods in Computer Science},
  keywords = {myown},
  month = {jul},
  publisher = {Centre pour la Communication Scientifique Directe (CCSD)},
  title = {The Complexity of Reachability in Affine Vector Addition Systems with States},
  volume = {Volume 17, Issue 3},
  year = 2021
  }
  

  %0 Journal Article
  %1 Blondin_2021
  %A Blondin, Michael
  %A Raskin, Mikhail
  %D 2021
  %I Centre pour la Communication Scientifique Directe (CCSD)
  %J Logical Methods in Computer Science
  %R 10.46298/lmcs-17(3:3)2021
  %T The Complexity of Reachability in Affine Vector Addition Systems with States
  %U https://doi.org/10.46298%2Flmcs-17%283%3A3%292021
  %V Volume 17, Issue 3
  

• 1.

  Balasubramanian, A.: Parameterized verification of coverability in infinite state broadcast networks. Information and Computation. 278, 104592 (2021)
  broadcastnetworks parameterizedverification
  URL: Link

  URLBibTeXEndNote

  @article{Balasubramanian_2021,
  author = {Balasubramanian, A.R.},
  journal = {Information and Computation},
  keywords = {broadcastnetworks parameterizedverification},
  month = {jun},
  pages = 104592,
  publisher = {Elsevier BV},
  title = {Parameterized verification of coverability in infinite state broadcast networks},
  volume = 278,
  year = 2021
  }
  

  %0 Journal Article
  %1 Balasubramanian_2021
  %A Balasubramanian, A.R.
  %D 2021
  %I Elsevier BV
  %J Information and Computation
  %P 104592
  %R 10.1016/j.ic.2020.104592
  %T Parameterized verification of coverability in infinite state broadcast networks
  %U https://doi.org/10.1016%2Fj.ic.2020.104592
  %V 278
  

• 1.

  Esparza, J., Raskin, M., Welzel, C.: Abduction of trap invariants in parameterized systems. (2021)
  myown parametrized parametrizedverification verification
  URL: Link
  cite arxiv:2108.09101Comment: Full version of the article In Proceedings GandALF 2021

  AbstractURLBibTeXEndNote

  In a previous paper we have presented a CEGAR approach for the verification of parameterized systems with an arbitrary number of processes organized in an array or a ring. The technique is based on the iterative computation of parameterized invariants, i.e., infinite families of invariants for the infinitely many instances of the system. Safety properties are proved by checking that every global configuration of the system satisfying all parameterized invariants also satisfies the property; we have shown that this check can be reduced to the satisfiability problem for Monadic Second Order on words, which is decidable. A strong limitation of the approach is that processes can only have a fixed number of variables with a fixed finite range. In particular, they cannot use variables with range [0,N-1], where N is the number of processes, which appear in many standard distributed algorithms. In this paper, we extend our technique to this case. While conducting the check whether a safety property is inductive assuming a computed set of invariants becomes undecidable, we show how to reduce it to checking satisfiability of a first-order formula. We report on experiments showing that automatic first-order theorem provers can still perform this check for a collection of non-trivial examples. Additionally, we can give small sets of readable invariants for these checks.

  @article{esparza2021abduction,
  abstract = {In a previous paper we have presented a CEGAR approach for the verification of parameterized systems with an arbitrary number of processes organized in an array or a ring. The technique is based on the iterative computation of parameterized invariants, i.e., infinite families of invariants for the infinitely many instances of the system. Safety properties are proved by checking that every global configuration of the system satisfying all parameterized invariants also satisfies the property; we have shown that this check can be reduced to the satisfiability problem for Monadic Second Order on words, which is decidable. A strong limitation of the approach is that processes can only have a fixed number of variables with a fixed finite range. In particular, they cannot use variables with range [0,N-1], where N is the number of processes, which appear in many standard distributed algorithms. In this paper, we extend our technique to this case. While conducting the check whether a safety property is inductive assuming a computed set of invariants becomes undecidable, we show how to reduce it to checking satisfiability of a first-order formula. We report on experiments showing that automatic first-order theorem provers can still perform this check for a collection of non-trivial examples. Additionally, we can give small sets of readable invariants for these checks.},
  author = {Esparza, Javier and Raskin, Mikhail and Welzel, Christoph},
  keywords = {myown parametrized parametrizedverification verification},
  note = {cite arxiv:2108.09101Comment: Full version of the article In Proceedings GandALF 2021},
  title = {Abduction of trap invariants in parameterized systems},
  year = 2021
  }
  

  %0 Journal Article
  %1 esparza2021abduction
  %A Esparza, Javier
  %A Raskin, Mikhail
  %A Welzel, Christoph
  %D 2021
  %R 10.4204/EPTCS.346.1
  %T Abduction of trap invariants in parameterized systems
  %U http://arxiv.org/abs/2108.09101
  %X In a previous paper we have presented a CEGAR approach for the verification of parameterized systems with an arbitrary number of processes organized in an array or a ring. The technique is based on the iterative computation of parameterized invariants, i.e., infinite families of invariants for the infinitely many instances of the system. Safety properties are proved by checking that every global configuration of the system satisfying all parameterized invariants also satisfies the property; we have shown that this check can be reduced to the satisfiability problem for Monadic Second Order on words, which is decidable. A strong limitation of the approach is that processes can only have a fixed number of variables with a fixed finite range. In particular, they cannot use variables with range [0,N-1], where N is the number of processes, which appear in many standard distributed algorithms. In this paper, we extend our technique to this case. While conducting the check whether a safety property is inductive assuming a computed set of invariants becomes undecidable, we show how to reduce it to checking satisfiability of a first-order formula. We report on experiments showing that automatic first-order theorem provers can still perform this check for a collection of non-trivial examples. Additionally, we can give small sets of readable invariants for these checks.
  

• 1.

  Meyer, P.K.J.: Constraint-based Analysis of Distributed Systems, (2021)
  petrinets populationprotocols verification workflownets
  #submitted #pdh #thesis

  AbstractBibTeXEndNote

  We develop constraint-based procedures to analyze safety, liveness and quantitative properties of certain models of distributed systems, especially Petri nets, population protocols and workflow nets. These procedures are incomplete in general, but have a lower complexity than the general problem and succeed on many practical instances or relevant subclasses of the model. We also show new complexity and decidability results for quantitative properties of workflow nets.

  @phdthesis{phd/dnb/Meyer21,
  abstract = {We develop constraint-based procedures to analyze safety, liveness and quantitative properties of certain models of distributed systems, especially Petri nets, population protocols and workflow nets. These procedures are incomplete in general, but have a lower complexity than the general problem and succeed on many practical instances or relevant subclasses of the model. We also show new complexity and decidability results for quantitative properties of workflow nets.},
  author = {Meyer, Philipp K. J.},
  keywords = {petrinets populationprotocols verification workflownets},
  note = {#submitted #pdh #thesis},
  school = {Technical University of Munich, Germany},
  title = {Constraint-based Analysis of Distributed Systems},
  type = {Publication},
  year = 2021
  }
  

  %0 Thesis
  %1 phd/dnb/Meyer21
  %A Meyer, Philipp K. J.
  %D 2021
  %T Constraint-based Analysis of Distributed Systems
  %X We develop constraint-based procedures to analyze safety, liveness and quantitative properties of certain models of distributed systems, especially Petri nets, population protocols and workflow nets. These procedures are incomplete in general, but have a lower complexity than the general problem and succeed on many practical instances or relevant subclasses of the model. We also show new complexity and decidability results for quantitative properties of workflow nets.
  

• 1.

  Balasubramanian, A.R., Lang, T., Ramanayake, R.: Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics. Accepted at LICS’21. (2021)
  complexity hypersequents substructurallogics
  URL: Link
  Preprint: <a href=”https://arxiv.org/abs/2104.09716”>Link</a><br>#conference

  URLBibTeXEndNote

  @article{balasubramanian2021decidability,
  author = {Balasubramanian, A. R. and Lang, Timo and Ramanayake, Revantha},
  journal = {Accepted at LICS'21},
  keywords = {complexity hypersequents substructurallogics},
  note = {Preprint: Link
  #conference},
  title = {Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics.},
  year = 2021
  }
  

  %0 Journal Article
  %1 balasubramanian2021decidability
  %A Balasubramanian, A. R.
  %A Lang, Timo
  %A Ramanayake, Revantha
  %D 2021
  %J Accepted at LICS'21
  %T Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics.
  %U http://easyconferences.eu/lics2021/accepted-papers/
  

• 1.

  Bertrand, N., Konnov, I., Lazi’c, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. International Journal on Software Tools for Technology Transfer. (2021)
  randomizedconsensus verification
  URL: Link

  AbstractURLBibTeXEndNote

  Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round \\($\$\)r-1\\($\$\). For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or's and Bracha's seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.

  @article{Bertrand2021,
  abstract = {Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round \\($\$\)r-1\\($\$\). For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or's and Bracha's seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.},
  author = {Bertrand, Nathalie and Konnov, Igor and Lazi'c, Marijana and Widder, Josef},
  journal = {International Journal on Software Tools for Technology Transfer},
  keywords = {randomizedconsensus verification},
  month = {feb},
  title = {Verification of randomized consensus algorithms under round-rigid adversaries},
  year = 2021
  }
  

  %0 Journal Article
  %1 Bertrand2021
  %A Bertrand, Nathalie
  %A Konnov, Igor
  %A Lazi'c, Marijana
  %A Widder, Josef
  %D 2021
  %J International Journal on Software Tools for Technology Transfer
  %R 10.1007/s10009-020-00603-x
  %T Verification of randomized consensus algorithms under round-rigid adversaries
  %U https://doi.org/10.1007/s10009-020-00603-x
  %X Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round \\($\$\)r-1\\($\$\). For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or's and Bracha's seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.
  

• 1.

  Esparza, J., Raskin, M., Welzel, C.: Computing Parameterized Invariants of Parameterized Petri Nets, (2021)
  invariants parameterized petrinets
  Preprint: <a href="https://arxiv.org/abs/2103.10280">Link</a><br>#informal

  BibTeXEndNote

  @misc{esparza2021computing,
  author = {Esparza, Javier and Raskin, Mikhail and Welzel, Christoph},
  keywords = {invariants parameterized petrinets},
  note = {Preprint: Link
  #informal},
  title = {Computing Parameterized Invariants of Parameterized Petri Nets},
  year = 2021
  }
  

  %0 Generic
  %1 esparza2021computing
  %A Esparza, Javier
  %A Raskin, Mikhail
  %A Welzel, Christoph
  %D 2021
  %T Computing Parameterized Invariants of Parameterized Petri Nets
  

• 1.

  Czerner, P., Jaax, S.: Running Time Analysis of Broadcast Consensus Protocols. In: Kiefer, S. and Tasson, C. (eds.) Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. pp. 164–183. Springer (2021)
  broadcastprotocols complexitytheory distributedcomputing
  URL: Link
  #conference

  AbstractURLBibTeXEndNote

  Broadcast consensus protocols (BCPs) are a model of computation, in which anonymous, identical, finite-state agents compute by sending/receiving global broadcasts. BCPs are known to compute all number predicates in NL=NSPACE(log n) where n is the number of agents. They can be considered an extension of the well-established model of population protocols. This paper investigates execution time characteristics of BCPs. We show that every predicate computable by population protocols is computable by a BCP with expected O(n log n) interactions, which is asymptotically optimal. We further show that every log-space, randomized Turing machine can be simulated by a BCP with O(n log n ⋅ T) interactions in expectation, where T is the expected runtime of the Turing machine. This allows us to characterise polynomial-time BCPs as computing exactly the number predicates in ZPL, i.e. predicates decidable by log-space bounded randomised Turing machine with zero-error in expected polynomial time where the input is encoded as unary.

  @inproceedings{DBLP:conf/fossacs/CzernerJ21,
  abstract = {Broadcast consensus protocols (BCPs) are a model of computation, in which anonymous, identical, finite-state agents compute by sending/receiving global broadcasts. BCPs are known to compute all number predicates in NL=NSPACE(log n) where n is the number of agents. They can be considered an extension of the well-established model of population protocols. This paper investigates execution time characteristics of BCPs. We show that every predicate computable by population protocols is computable by a BCP with expected O(n log n) interactions, which is asymptotically optimal. We further show that every log-space, randomized Turing machine can be simulated by a BCP with O(n log n ⋅ T) interactions in expectation, where T is the expected runtime of the Turing machine. This allows us to characterise polynomial-time BCPs as computing exactly the number predicates in ZPL, i.e. predicates decidable by log-space bounded randomised Turing machine with zero-error in expected polynomial time where the input is encoded as unary.},
  author = {Czerner, Philipp and Jaax, Stefan},
  booktitle = {Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings},
  editor = {Kiefer, Stefan and Tasson, Christine},
  keywords = {broadcastprotocols complexitytheory distributedcomputing},
  note = {#conference},
  pages = {164--183},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Running Time Analysis of Broadcast Consensus Protocols},
  volume = 12650,
  year = 2021
  }
  

  %0 Conference Paper
  %1 DBLP:conf/fossacs/CzernerJ21
  %A Czerner, Philipp
  %A Jaax, Stefan
  %B Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings
  %D 2021
  %E Kiefer, Stefan
  %E Tasson, Christine
  %I Springer
  %P 164--183
  %R 10.1007/978-3-030-71995-1_9
  %T Running Time Analysis of Broadcast Consensus Protocols
  %U https://doi.org/10.1007/978-3-030-71995-1_9
  %V 12650
  %X Broadcast consensus protocols (BCPs) are a model of computation, in which anonymous, identical, finite-state agents compute by sending/receiving global broadcasts. BCPs are known to compute all number predicates in NL=NSPACE(log n) where n is the number of agents. They can be considered an extension of the well-established model of population protocols. This paper investigates execution time characteristics of BCPs. We show that every predicate computable by population protocols is computable by a BCP with expected O(n log n) interactions, which is asymptotically optimal. We further show that every log-space, randomized Turing machine can be simulated by a BCP with O(n log n ⋅ T) interactions in expectation, where T is the expected runtime of the Turing machine. This allows us to characterise polynomial-time BCPs as computing exactly the number predicates in ZPL, i.e. predicates decidable by log-space bounded randomised Turing machine with zero-error in expected polynomial time where the input is encoded as unary.
  

• 1.

  Balasubramanian, A.R., Thejaswini, K.S.: Adaptive Synchronisation of Pushdown Automata, https://arxiv.org/abs/2102.06897, (2021)
  pushdownautomata synchronisation
  URL: Link
  #informal

  AbstractURLBibTeXEndNote

  We introduce the notion of adaptive synchronisation for pushdown automata, in which there is an external observer who has no knowledge about the current state of the pushdown automaton, but can observe the contents of the stack. The observer would then like to decide if it is possible to bring the automaton from any state into some predetermined state by giving inputs to it in an adaptive manner, i.e., the next input letter to be given can depend on how the contents of the stack changed after the current input letter. We show that for non-deterministic pushdown automata, this problem is 2-EXPTIME-complete and for deterministic pushdown automata, we show EXPTIME-completeness. To prove the lower bounds, we first introduce (different variants of) subset-synchronisation and show that these problems are polynomial-time equivalent with the adaptive synchronisation problem. We then prove hardness results for the subset-synchronisation problems. For proving the upper bounds, we consider the problem of deciding if a given alternating pushdown system has an accepting run with at most k leaves and we provide an n^O(k^2) time algorithm for this problem.

  @misc{balasubramanian2021adaptive,
  abstract = {We introduce the notion of adaptive synchronisation for pushdown automata, in which there is an external observer who has no knowledge about the current state of the pushdown automaton, but can observe the contents of the stack. The observer would then like to decide if it is possible to bring the automaton from any state into some predetermined state by giving inputs to it in an adaptive manner, i.e., the next input letter to be given can depend on how the contents of the stack changed after the current input letter. We show that for non-deterministic pushdown automata, this problem is 2-EXPTIME-complete and for deterministic pushdown automata, we show EXPTIME-completeness. To prove the lower bounds, we first introduce (different variants of) subset-synchronisation and show that these problems are polynomial-time equivalent with the adaptive synchronisation problem. We then prove hardness results for the subset-synchronisation problems. For proving the upper bounds, we consider the problem of deciding if a given alternating pushdown system has an accepting run with at most k leaves and we provide an n^O(k^2) time algorithm for this problem.},
  author = {Balasubramanian, A. R. and Thejaswini, K. S.},
  keywords = {pushdownautomata synchronisation},
  note = {#informal},
  title = {Adaptive Synchronisation of Pushdown Automata},
  year = 2021
  }
  

  %0 Generic
  %1 balasubramanian2021adaptive
  %A Balasubramanian, A. R.
  %A Thejaswini, K. S.
  %D 2021
  %T Adaptive Synchronisation of Pushdown Automata
  %U https://arxiv.org/abs/2102.06897
  %X We introduce the notion of adaptive synchronisation for pushdown automata, in which there is an external observer who has no knowledge about the current state of the pushdown automaton, but can observe the contents of the stack. The observer would then like to decide if it is possible to bring the automaton from any state into some predetermined state by giving inputs to it in an adaptive manner, i.e., the next input letter to be given can depend on how the contents of the stack changed after the current input letter. We show that for non-deterministic pushdown automata, this problem is 2-EXPTIME-complete and for deterministic pushdown automata, we show EXPTIME-completeness. To prove the lower bounds, we first introduce (different variants of) subset-synchronisation and show that these problems are polynomial-time equivalent with the adaptive synchronisation problem. We then prove hardness results for the subset-synchronisation problems. For proving the upper bounds, we consider the problem of deciding if a given alternating pushdown system has an accepting run with at most k leaves and we provide an n^O(k^2) time algorithm for this problem.
  

• 1.

  van Ditmarsch, H., Goubault, Éric, Lazić, M., Ledent, J., Rajsbaum, S.: A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks. Journal of Logical and Algebraic Methods in Programming. 100662 (2021)
  analysis logic
  URL: Link
  #journal

  AbstractURLBibTeXEndNote

  In this paper we study the solvability of the equality negation task in a simple wait-free model where two processes communicate by reading and writing shared variables or exchanging messages. In this task, the two processes start with a private input value in the set 0,1,2, and after communicating, each one must decide a binary output value, so that the outputs of the processes are the same if and only if the input values of the processes are different. This task is already known to be unsolvable; our goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by Goubault, Ledent and Rajsbaum in GandALF 2018. We show that in fact, there is no epistemic logic formula that explains why the task is unsolvable. Furthermore, we observe that this task is a particular case of an epistemic covering task. We thus establish a connection between the existing DEL framework and the theory of covering spaces in topology, and prove that the same result holds for any epistemic covering task: no epistemic formula explains the unsolvability.

  @article{VANDITMARSCH2021100662,
  abstract = {In this paper we study the solvability of the equality negation task in a simple wait-free model where two processes communicate by reading and writing shared variables or exchanging messages. In this task, the two processes start with a private input value in the set 0,1,2, and after communicating, each one must decide a binary output value, so that the outputs of the processes are the same if and only if the input values of the processes are different. This task is already known to be unsolvable; our goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by Goubault, Ledent and Rajsbaum in GandALF 2018. We show that in fact, there is no epistemic logic formula that explains why the task is unsolvable. Furthermore, we observe that this task is a particular case of an epistemic covering task. We thus establish a connection between the existing DEL framework and the theory of covering spaces in topology, and prove that the same result holds for any epistemic covering task: no epistemic formula explains the unsolvability.},
  author = {van Ditmarsch, Hans and Goubault, Éric and Lazić, Marijana and Ledent, Jérémy and Rajsbaum, Sergio},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  keywords = {analysis logic},
  note = {#journal},
  pages = 100662,
  title = {A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks},
  year = 2021
  }
  

  %0 Journal Article
  %1 VANDITMARSCH2021100662
  %A van Ditmarsch, Hans
  %A Goubault, Éric
  %A Lazić, Marijana
  %A Ledent, Jérémy
  %A Rajsbaum, Sergio
  %D 2021
  %J Journal of Logical and Algebraic Methods in Programming
  %P 100662
  %R https://doi.org/10.1016/j.jlamp.2021.100662
  %T A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks
  %U https://www.sciencedirect.com/science/article/pii/S2352220821000250
  %X In this paper we study the solvability of the equality negation task in a simple wait-free model where two processes communicate by reading and writing shared variables or exchanging messages. In this task, the two processes start with a private input value in the set 0,1,2, and after communicating, each one must decide a binary output value, so that the outputs of the processes are the same if and only if the input values of the processes are different. This task is already known to be unsolvable; our goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by Goubault, Ledent and Rajsbaum in GandALF 2018. We show that in fact, there is no epistemic logic formula that explains why the task is unsolvable. Furthermore, we observe that this task is a particular case of an epistemic covering task. We thus establish a connection between the existing DEL framework and the theory of covering spaces in topology, and prove that the same result holds for any epistemic covering task: no epistemic formula explains the unsolvability.
  

• 1.

  Bertrand, N., Lazi’c, M., Widder, J.: A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries. In: Henglein, F., Shoham, S., and Vizel, Y. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 219–239. Springer International Publishing (2021)
  distributedalgorithms
  URL: Link
  #conference

  AbstractURLBibTeXEndNote

  Weak adversaries are a way to model the uncertainty due to asynchrony in randomized distributed algorithms. They are a standard notion in correctness proofs for distributed algorithms, and express the property that the adversary (scheduler), which has to decide which messages to deliver to which process, has no means of inferring the outcome of random choices, and the content of the messages.In this paper, we introduce a model for randomized distributed algorithms that allows us to formalize the notion of weak adversaries. It applies to randomized distributed algorithms that proceed in rounds and are tolerant to process failures. For this wide class of algorithms, we prove that for verification purposes, the class of weak adversaries can be restricted to simple ones, so-called round-rigid adversaries, that keep the processes tightly synchronized. As recently a verification method for round-rigid adversaries has been introduced, our new reduction theorem paves the way to the parameterized verification of randomized distributed algorithms under the more realistic weak adversaries.

  @inproceedings{10.1007/978-3-030-67067-2_11,
  abstract = {Weak adversaries are a way to model the uncertainty due to asynchrony in randomized distributed algorithms. They are a standard notion in correctness proofs for distributed algorithms, and express the property that the adversary (scheduler), which has to decide which messages to deliver to which process, has no means of inferring the outcome of random choices, and the content of the messages.In this paper, we introduce a model for randomized distributed algorithms that allows us to formalize the notion of weak adversaries. It applies to randomized distributed algorithms that proceed in rounds and are tolerant to process failures. For this wide class of algorithms, we prove that for verification purposes, the class of weak adversaries can be restricted to simple ones, so-called round-rigid adversaries, that keep the processes tightly synchronized. As recently a verification method for round-rigid adversaries has been introduced, our new reduction theorem paves the way to the parameterized verification of randomized distributed algorithms under the more realistic weak adversaries.},
  author = {Bertrand, Nathalie and Lazi'c, Marijana and Widder, Josef},
  booktitle = {Verification, Model Checking, and Abstract Interpretation},
  editor = {Henglein, Fritz and Shoham, Sharon and Vizel, Yakir},
  keywords = {distributedalgorithms},
  note = {#conference},
  pages = {219--239},
  publisher = {Springer International Publishing},
  title = {A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries},
  year = 2021
  }
  

  %0 Conference Paper
  %1 10.1007/978-3-030-67067-2_11
  %A Bertrand, Nathalie
  %A Lazi'c, Marijana
  %A Widder, Josef
  %B Verification, Model Checking, and Abstract Interpretation
  %D 2021
  %E Henglein, Fritz
  %E Shoham, Sharon
  %E Vizel, Yakir
  %I Springer International Publishing
  %P 219--239
  %R 10.1007/978-3-030-67067-2_11
  %T A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries
  %U https://link.springer.com/chapter/10.1007%2F978-3-030-67067-2_11
  %X Weak adversaries are a way to model the uncertainty due to asynchrony in randomized distributed algorithms. They are a standard notion in correctness proofs for distributed algorithms, and express the property that the adversary (scheduler), which has to decide which messages to deliver to which process, has no means of inferring the outcome of random choices, and the content of the messages.In this paper, we introduce a model for randomized distributed algorithms that allows us to formalize the notion of weak adversaries. It applies to randomized distributed algorithms that proceed in rounds and are tolerant to process failures. For this wide class of algorithms, we prove that for verification purposes, the class of weak adversaries can be restricted to simple ones, so-called round-rigid adversaries, that keep the processes tightly synchronized. As recently a verification method for round-rigid adversaries has been introduced, our new reduction theorem paves the way to the parameterized verification of randomized distributed algorithms under the more realistic weak adversaries.
  %@ 978-3-030-67067-2
  

• 1.

  Kupferman, O., Sickert, S.: Certifying Inexpressibility. Accepted at FoSSaCS’21. (2021)
  expressibility verification
  URL: Link
  Preprint: <a href="https://arxiv.org/pdf/2101.08756.pdf">Link</a><br>#submitted #conference

  AbstractURLBibTeXEndNote

  Different classes of automata on infinite words have different expressive power. Deciding whether a given language L⊆Σ^ω can be expressed by an automaton of a desired class can be reduced to deciding a game between Prover and Refuter: in each turn of the game, Refuter provides a letter in Σ, and Prover responds with an annotation of the current state of the run (for example, in the case of Buchi automata, whether the state is accepting or rejecting, and in the case of parity automata, what the color of the state is). Prover wins if the sequence of annotations she generates is correct: it is an accepting run iff the word generated by Refuter is in L. We show how a winning strategy for Refuter can serve as a simple and easy-to-understand certificate to inexpressibility, and how it induces additional forms of certificates. Our framework handles all classes of deterministic automata, including ones with structural restrictions like weak automata. In addition, it can be used for refuting separation of two languages by an automaton of the desired class, and for finding automata that approximate L and belong to the desired class.

  @article{kupferman2021certifying,
  abstract = {Different classes of automata on infinite words have different expressive power. Deciding whether a given language L⊆Σ^ω can be expressed by an automaton of a desired class can be reduced to deciding a game between Prover and Refuter: in each turn of the game, Refuter provides a letter in Σ, and Prover responds with an annotation of the current state of the run (for example, in the case of Buchi automata, whether the state is accepting or rejecting, and in the case of parity automata, what the color of the state is). Prover wins if the sequence of annotations she generates is correct: it is an accepting run iff the word generated by Refuter is in L. We show how a winning strategy for Refuter can serve as a simple and easy-to-understand certificate to inexpressibility, and how it induces additional forms of certificates. Our framework handles all classes of deterministic automata, including ones with structural restrictions like weak automata. In addition, it can be used for refuting separation of two languages by an automaton of the desired class, and for finding automata that approximate L and belong to the desired class.},
  author = {Kupferman, Orna and Sickert, Salomon},
  journal = {Accepted at FoSSaCS’21},
  keywords = {expressibility verification},
  note = {Preprint: Link
  #submitted #conference},
  title = {Certifying Inexpressibility},
  year = 2021
  }
  

  %0 Journal Article
  %1 kupferman2021certifying
  %A Kupferman, Orna
  %A Sickert, Salomon
  %D 2021
  %J Accepted at FoSSaCS’21
  %T Certifying Inexpressibility
  %U https://etaps.org/user-profile/list-articles/449-fossacs-2021-accepted-papers
  %X Different classes of automata on infinite words have different expressive power. Deciding whether a given language L⊆Σ^ω can be expressed by an automaton of a desired class can be reduced to deciding a game between Prover and Refuter: in each turn of the game, Refuter provides a letter in Σ, and Prover responds with an annotation of the current state of the run (for example, in the case of Buchi automata, whether the state is accepting or rejecting, and in the case of parity automata, what the color of the state is). Prover wins if the sequence of annotations she generates is correct: it is an accepting run iff the word generated by Refuter is in L. We show how a winning strategy for Refuter can serve as a simple and easy-to-understand certificate to inexpressibility, and how it induces additional forms of certificates. Our framework handles all classes of deterministic automata, including ones with structural restrictions like weak automata. In addition, it can be used for refuting separation of two languages by an automaton of the desired class, and for finding automata that approximate L and belong to the desired class.
  

• 1.

  Balasubramanian, A.R., Esparza, J., Raskin, M.A.: Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy. Accepted at FoSSaCS’21. (2021)
  parametrizedverification populationprotocols reachability thresholds
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/2010.09471">Link</a><br>#submitted #conference

  URLBibTeXEndNote

  @article{journals/corr/abs-2010-09471,
  author = {Balasubramanian, A. R. and Esparza, Javier and Raskin, Mikhail A.},
  journal = {Accepted at FoSSaCS’21},
  keywords = {parametrizedverification populationprotocols reachability thresholds},
  note = {Preprint: Link
  #submitted #conference},
  title = {Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy.},
  year = 2021
  }
  

  %0 Journal Article
  %1 journals/corr/abs-2010-09471
  %A Balasubramanian, A. R.
  %A Esparza, Javier
  %A Raskin, Mikhail A.
  %D 2021
  %J Accepted at FoSSaCS’21
  %T Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy.
  %U https://etaps.org/user-profile/list-articles/449-fossacs-2021-accepted-papers
  

• 1.

  Esparza, J., Jaax, S., Raskin, M.A., Weil-Kennedy, C.: The Complexity of Verifying Population Protocols. Distributed Computing. (2021)
  complexity myown parametrizedverification populationprotocols verification
  Preprint: <a href="https://arxiv.org/abs/1912.06578">Link</a><br> #journal

  AbstractBibTeXEndNote

  Population protocols [Angluin et al., PODC, 2004] are a model of distributed computation in which indistinguishable, finite-state agents interact in pairs to decide if their initial configuration, i.e., the initial number of agents in each state, satisfies a given property. In a seminal paper Angluin et al. classified population protocols according to their communication mechanism, and conducted an exhaustive study of the expressive power of each class, that is, of the properties they can decide [Angluin et al., Distributed Computing, 2007]. In this paper we study the correctness problem for population protocols, i.e., whether a given protocol decides a given property. A previous paper [Esparza et al., Acta Informatica, 2017] has shown that the problem is decidable for the main population protocol model, but at least as hard as the reachability problem for Petri nets, which has recently been proved to have non-elementary complexity. Motivated by this result, we study the computational complexity of the correctness problem for all other classes introduced by Angluin et al., some of which are less powerful than the main model. Our main results show that for the class of observation models the complexity of the problem is much lower, ranging from Πp2 to PSPACE.

  @article{esparza2019complexity,
  abstract = {Population protocols [Angluin et al., PODC, 2004] are a model of distributed computation in which indistinguishable, finite-state agents interact in pairs to decide if their initial configuration, i.e., the initial number of agents in each state, satisfies a given property. In a seminal paper Angluin et al. classified population protocols according to their communication mechanism, and conducted an exhaustive study of the expressive power of each class, that is, of the properties they can decide [Angluin et al., Distributed Computing, 2007]. In this paper we study the correctness problem for population protocols, i.e., whether a given protocol decides a given property. A previous paper [Esparza et al., Acta Informatica, 2017] has shown that the problem is decidable for the main population protocol model, but at least as hard as the reachability problem for Petri nets, which has recently been proved to have non-elementary complexity. Motivated by this result, we study the computational complexity of the correctness problem for all other classes introduced by Angluin et al., some of which are less powerful than the main model. Our main results show that for the class of observation models the complexity of the problem is much lower, ranging from Πp2 to PSPACE.},
  author = {Esparza, Javier and Jaax, Stefan and Raskin, Mikhail A. and Weil-Kennedy, Chana},
  journal = {Distributed Computing},
  keywords = {complexity myown parametrizedverification populationprotocols verification},
  note = {Preprint: Link
  #journal},
  title = {The Complexity of Verifying Population Protocols.},
  year = 2021
  }
  

  %0 Journal Article
  %1 esparza2019complexity
  %A Esparza, Javier
  %A Jaax, Stefan
  %A Raskin, Mikhail A.
  %A Weil-Kennedy, Chana
  %D 2021
  %J Distributed Computing
  %T The Complexity of Verifying Population Protocols.
  %X Population protocols [Angluin et al., PODC, 2004] are a model of distributed computation in which indistinguishable, finite-state agents interact in pairs to decide if their initial configuration, i.e., the initial number of agents in each state, satisfies a given property. In a seminal paper Angluin et al. classified population protocols according to their communication mechanism, and conducted an exhaustive study of the expressive power of each class, that is, of the properties they can decide [Angluin et al., Distributed Computing, 2007]. In this paper we study the correctness problem for population protocols, i.e., whether a given protocol decides a given property. A previous paper [Esparza et al., Acta Informatica, 2017] has shown that the problem is decidable for the main population protocol model, but at least as hard as the reachability problem for Petri nets, which has recently been proved to have non-elementary complexity. Motivated by this result, we study the computational complexity of the correctness problem for all other classes introduced by Angluin et al., some of which are less powerful than the main model. Our main results show that for the class of observation models the complexity of the problem is much lower, ranging from Πp2 to PSPACE.
  

• 1.

  Czerner, P., Esparza, J.: Lower Bounds on the State Complexity of Population Protocols. In: Miller, A., Censor-Hillel, K., and Korhonen, J.H. (eds.) PODC ’21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021. pp. 45–54. ACM (2021)
  imported

  BibTeXEndNote

  @inproceedings{CzernerE21,
  author = {Czerner, Philipp and Esparza, Javier},
  booktitle = {PODC '21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021},
  editor = {Miller, Avery and Censor-Hillel, Keren and Korhonen, Janne H.},
  keywords = {imported},
  month = {July},
  pages = {45--54},
  publisher = {ACM},
  title = {Lower Bounds on the State Complexity of Population Protocols},
  year = 2021
  }
  

  %0 Conference Paper
  %1 CzernerE21
  %A Czerner, Philipp
  %A Esparza, Javier
  %B PODC '21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021
  %D 2021
  %E Miller, Avery
  %E Censor-Hillel, Keren
  %E Korhonen, Janne H.
  %I ACM
  %P 45--54
  %R 10.1145/3465084.3467912
  %T Lower Bounds on the State Complexity of Population Protocols
  

2020

• 1.

  Blondin, M., Esparza, J., Genest, B., Helfrich, M., Jaax, S.: Succinct Population Protocols for Presburger Arithmetic. In: Paul, C. and Bläser, M. (eds.) STACS. pp. 40:1–40:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
  myown populationprotocols succinct synthesis
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/1910.04600">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  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 f of quantifier-free PA with remainder predicates (which has the same expressive power as full PA) into a population protocol with 2^O(poly(|f|)) states that computes f. 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 f of quantifier-free PA with remainder predicates is computable by a leaderless population protocol with O(poly(|f|)) states. Our proof is based on several new constructions, which may be of independent interest. Given a formula f of quantifier-free PA with remainder predicates, a first construction produces a succinct protocol (with O(|f|³) leaders) that computes f; 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 f. Our last construction gets rid of this leader for small inputs.

  @inproceedings{conf/stacs/BlondinEGHJ20,
  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 f of quantifier-free PA with remainder predicates (which has the same expressive power as full PA) into a population protocol with 2^O(poly(|f|)) states that computes f. 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 f of quantifier-free PA with remainder predicates is computable by a leaderless population protocol with O(poly(|f|)) states. Our proof is based on several new constructions, which may be of independent interest. Given a formula f of quantifier-free PA with remainder predicates, a first construction produces a succinct protocol (with O(|f|³) leaders) that computes f; 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 f. Our last construction gets rid of this leader for small inputs.},
  author = {Blondin, Michael and Esparza, Javier and Genest, Blaise and Helfrich, Martin and Jaax, Stefan},
  booktitle = {STACS},
  crossref = {conf/stacs/2020},
  editor = {Paul, Christophe and Bläser, Markus},
  keywords = {myown populationprotocols succinct synthesis},
  note = {Preprint: Link
  #conference},
  pages = {40:1-40:15},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  series = {LIPIcs},
  title = {Succinct Population Protocols for Presburger Arithmetic.},
  volume = 154,
  year = 2020
  }
  

  %0 Conference Paper
  %1 conf/stacs/BlondinEGHJ20
  %A Blondin, Michael
  %A Esparza, Javier
  %A Genest, Blaise
  %A Helfrich, Martin
  %A Jaax, Stefan
  %B STACS
  %D 2020
  %E Paul, Christophe
  %E Bläser, Markus
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %P 40:1-40:15
  %R 10.4230/LIPIcs.STACS.2020.40
  %T Succinct Population Protocols for Presburger Arithmetic.
  %U https://drops.dagstuhl.de/opus/volltexte/2020/11901/
  %V 154
  %X 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 f of quantifier-free PA with remainder predicates (which has the same expressive power as full PA) into a population protocol with 2^O(poly(|f|)) states that computes f. 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 f of quantifier-free PA with remainder predicates is computable by a leaderless population protocol with O(poly(|f|)) states. Our proof is based on several new constructions, which may be of independent interest. Given a formula f of quantifier-free PA with remainder predicates, a first construction produces a succinct protocol (with O(|f|³) leaders) that computes f; 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 f. Our last construction gets rid of this leader for small inputs.
  %@ 978-3-95977-140-5
  

• 1.

  Raskin, M., Weil-Kennedy, C.: Efficient Restrictions of Immediate Observation Petri Nets. Reachability Problems (2020)
  immediateobservation myown reachability
  Preprint: <a href="http://arxiv.org/abs/2007.09189">Link</a><br>#conference

  AbstractBibTeXEndNote

  In a previous paper we introduced immediate observation Petri nets, a subclass of Petri nets with application domains in distributed protocols (population protocols) and theoretical chemistry (chemical reaction networks). IO nets enjoy many useful properties, but like the general case of conservative Petri nets they have a PSPACE-complete reachability problem. In this paper we explore two restrictions of the reachability problem for IO nets which lower the complexity of the problem drastically. The complexity is NP-complete for the first restriction with applications in distributed protocols, and it is polynomial for the second restriction with applications in chemical settings.

  @conference{raskin2020efficient,
  abstract = {In a previous paper we introduced immediate observation Petri nets, a subclass of Petri nets with application domains in distributed protocols (population protocols) and theoretical chemistry (chemical reaction networks). IO nets enjoy many useful properties, but like the general case of conservative Petri nets they have a PSPACE-complete reachability problem. In this paper we explore two restrictions of the reachability problem for IO nets which lower the complexity of the problem drastically. The complexity is NP-complete for the first restriction with applications in distributed protocols, and it is polynomial for the second restriction with applications in chemical settings.},
  author = {Raskin, Michael and Weil-Kennedy, Chana},
  booktitle = {Reachability Problems},
  keywords = {immediateobservation myown reachability},
  note = {Preprint: Link
  #conference},
  title = {Efficient Restrictions of Immediate Observation Petri Nets},
  year = 2020
  }
  

  %0 Generic
  %1 raskin2020efficient
  %A Raskin, Michael
  %A Weil-Kennedy, Chana
  %B Reachability Problems
  %D 2020
  %T Efficient Restrictions of Immediate Observation Petri Nets
  %X In a previous paper we introduced immediate observation Petri nets, a subclass of Petri nets with application domains in distributed protocols (population protocols) and theoretical chemistry (chemical reaction networks). IO nets enjoy many useful properties, but like the general case of conservative Petri nets they have a PSPACE-complete reachability problem. In this paper we explore two restrictions of the reachability problem for IO nets which lower the complexity of the problem drastically. The complexity is NP-complete for the first restriction with applications in distributed protocols, and it is polynomial for the second restriction with applications in chemical settings.
  

• 1.

  Esparza, J., Reiter, F.: A Classification of Weak Asynchronous Models of Distributed Computing. In: Konnov, I. and Kovács, L. (eds.) 31st International Conference on Concurrency Theory (CONCUR 2020). pp. 10:1–10:16. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020)
  asyncronous classification distributedalgorithms myown
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/2007.03291">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  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.

  @inproceedings{esparza2020classification,
  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.},
  address = {Dagstuhl, Germany},
  annote = {Keywords: Asynchrony, Concurrency theory, Weak models of distributed computing},
  author = {Esparza, Javier and Reiter, Fabian},
  booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
  editor = {Konnov, Igor and Kovács, Laura},
  keywords = {asyncronous classification distributedalgorithms myown},
  note = {Preprint: Link
  #conference},
  pages = {10:1--10:16},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {A Classification of Weak Asynchronous Models of Distributed Computing},
  volume = 171,
  year = 2020
  }
  

  %0 Conference Paper
  %1 esparza2020classification
  %A Esparza, Javier
  %A Reiter, Fabian
  %B 31st International Conference on Concurrency Theory (CONCUR 2020)
  %C Dagstuhl, Germany
  %D 2020
  %E Konnov, Igor
  %E Kovács, Laura
  %I Schloss Dagstuhl--Leibniz-Zentrum für Informatik
  %P 10:1--10:16
  %R 10.4230/LIPIcs.CONCUR.2020.10
  %T A Classification of Weak Asynchronous Models of Distributed Computing
  %U https://drops.dagstuhl.de/opus/volltexte/2020/12822
  %V 171
  %X 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.
  %Z Keywords: Asynchrony, Concurrency theory, Weak models of distributed computing
  %@ 978-3-95977-160-3
  

• 1.

  Bozga, M., Esparza, J., Iosif, R., Sifakis, J., Welzel, C.: Structural Invariants for the Verification of Systems with Parameterized Architectures. In: Biere, A. and Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I. pp. 228–246. Springer (2020)
  invariants myown parameterizedverification verification
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/2002.07672">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata.

  @inproceedings{bozga2020structural,
  abstract = {We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata.},
  author = {Bozga, Marius and Esparza, Javier and Iosif, Radu and Sifakis, Joseph and Welzel, Christoph},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I},
  editor = {Biere, Armin and Parker, David},
  keywords = {invariants myown parameterizedverification verification},
  note = {Preprint: Link
  #conference},
  pages = {228--246},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Structural Invariants for the Verification of Systems with Parameterized Architectures},
  volume = 12078,
  year = 2020
  }
  

  %0 Conference Paper
  %1 bozga2020structural
  %A Bozga, Marius
  %A Esparza, Javier
  %A Iosif, Radu
  %A Sifakis, Joseph
  %A Welzel, Christoph
  %B Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I
  %D 2020
  %E Biere, Armin
  %E Parker, David
  %I Springer
  %P 228--246
  %R 10.1007/978-3-030-45190-5_13
  %T Structural Invariants for the Verification of Systems with Parameterized Architectures
  %U https://doi.org/10.1007/978-3-030-45190-5_13
  %V 12078
  %X We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata.
  

• 1.

  Konnov, I., Lazic, M., Stoilkovska, I., Widder, J.: Tutorial: Parameterized Verification with Byzantine Model Checker. In: Gotsman, A. and Sokolova, A. (eds.) FORTE. pp. 189–207. Springer (2020)
  parametrizedverification verification
  URL: Link
  #conference

  URLBibTeXEndNote

  @inproceedings{conf/forte/0001LSW20,
  author = {Konnov, Igor and Lazic, Marijana and Stoilkovska, Ilina and Widder, Josef},
  booktitle = {FORTE},
  crossref = {conf/forte/2020},
  editor = {Gotsman, Alexey and Sokolova, Ana},
  keywords = {parametrizedverification verification},
  note = {#conference},
  pages = {189-207},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Tutorial: Parameterized Verification with Byzantine Model Checker},
  volume = 12136,
  year = 2020
  }
  

  %0 Conference Paper
  %1 conf/forte/0001LSW20
  %A Konnov, Igor
  %A Lazic, Marijana
  %A Stoilkovska, Ilina
  %A Widder, Josef
  %B FORTE
  %D 2020
  %E Gotsman, Alexey
  %E Sokolova, Ana
  %I Springer
  %P 189-207
  %T Tutorial: Parameterized Verification with Byzantine Model Checker
  %U https://link.springer.com/chapter/10.1007/978-3-030-50086-3_11
  %V 12136
  %@ 978-3-030-50086-3
  

• 1.

  Balasubramanian, A.R.: Parameterized Complexity of Safety of Threshold Automata. In: Saxena, N. and Simon, S. (eds.) 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). pp. 37:1–37:15. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020)
  complexity parametrized thresholdautomata
  URL: Link
  #conference

  URLBibTeXEndNote

  @inproceedings{balasubramanian:LIPIcs:2020:13278,
  address = {Dagstuhl, Germany},
  annote = {Keywords: Threshold automata, distributed algorithms, parameterized complexity},
  author = {Balasubramanian, A. R.},
  booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  editor = {Saxena, Nitin and Simon, Sunil},
  keywords = {complexity parametrized thresholdautomata},
  note = {#conference},
  pages = {37:1--37:15},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {Parameterized Complexity of Safety of Threshold Automata},
  volume = 182,
  year = 2020
  }
  

  %0 Conference Paper
  %1 balasubramanian:LIPIcs:2020:13278
  %A Balasubramanian, A. R.
  %B 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)
  %C Dagstuhl, Germany
  %D 2020
  %E Saxena, Nitin
  %E Simon, Sunil
  %I Schloss Dagstuhl--Leibniz-Zentrum für Informatik
  %P 37:1--37:15
  %R 10.4230/LIPIcs.FSTTCS.2020.37
  %T Parameterized Complexity of Safety of Threshold Automata
  %U https://drops.dagstuhl.de/opus/volltexte/2020/13278
  %V 182
  %Z Keywords: Threshold automata, distributed algorithms, parameterized complexity
  %@ 978-3-95977-174-0
  

• 1.

  Jaax, S.: Population Protocols: Expressiveness, Succinctness and Automatic Verification., http://mediatum.ub.tum.de/doc/1538836/1538836.pdf, (2020)
  expressiveness populationprotocols succinctness verification
  URL: Link
  #pdh #thesis

  URLBibTeXEndNote

  @phdthesis{phd/dnb/Jaax20,
  author = {Jaax, Stefan},
  keywords = {expressiveness populationprotocols succinctness verification},
  note = {#pdh #thesis},
  school = {Technical University of Munich, Germany},
  title = {Population Protocols: Expressiveness, Succinctness and Automatic Verification.},
  type = {Publication},
  year = 2020
  }
  

  %0 Thesis
  %1 phd/dnb/Jaax20
  %A Jaax, Stefan
  %D 2020
  %T Population Protocols: Expressiveness, Succinctness and Automatic Verification.
  %U http://mediatum.ub.tum.de/doc/1538836/1538836.pdf
  

• 1.

  Esparza, J., Helfrich, M., Jaax, S., Meyer, P.J.: Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs. In: Hung, D.V. and Sokolsky, O. (eds.) Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. pp. 550–556. Springer (2020)
  peregrine populationprotocols stagegraphs
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/2007.07638">Link</a><br>#conference

  URLBibTeXEndNote

  @inproceedings{esparza2020peregrine,
  author = {Esparza, Javier and Helfrich, Martin and Jaax, Stefan and Meyer, Philipp J.},
  booktitle = {Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings},
  editor = {Hung, Dang Van and Sokolsky, Oleg},
  keywords = {peregrine populationprotocols stagegraphs},
  note = {Preprint: Link
  #conference},
  pages = {550--556},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs},
  volume = 12302,
  year = 2020
  }
  

  %0 Conference Paper
  %1 esparza2020peregrine
  %A Esparza, Javier
  %A Helfrich, Martin
  %A Jaax, Stefan
  %A Meyer, Philipp J.
  %B Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings
  %D 2020
  %E Hung, Dang Van
  %E Sokolsky, Oleg
  %I Springer
  %P 550--556
  %R 10.1007/978-3-030-59152-6\_32
  %T Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs
  %U https://doi.org/10.1007/978-3-030-59152-6_32
  %V 12302
  

• 1.

  D’Antoni, L., Helfrich, M., Kret’insk’y, J., Ramneantu, E., Weininger, M.: Automata Tutor v3. In: Lahiri, S.K. and Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. pp. 3–14. Springer (2020)
  tool
  URL: Link

  URLBibTeXEndNote

  @inproceedings{DAntoniHKRW20,
  author = {D'Antoni, Loris and Helfrich, Martin and Kret'insk'y, Jan and Ramneantu, Emanuel and Weininger, Maximilian},
  booktitle = {Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II},
  editor = {Lahiri, Shuvendu K. and Wang, Chao},
  keywords = {tool},
  month = {October},
  pages = {3-14},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Automata Tutor v3},
  volume = 12225,
  year = 2020
  }
  

  %0 Conference Paper
  %1 DAntoniHKRW20
  %A D'Antoni, Loris
  %A Helfrich, Martin
  %A Kret'insk'y, Jan
  %A Ramneantu, Emanuel
  %A Weininger, Maximilian
  %B Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II
  %D 2020
  %E Lahiri, Shuvendu K.
  %E Wang, Chao
  %I Springer
  %P 3-14
  %R 10.1007/978-3-030-53291-8_1
  %T Automata Tutor v3
  %U https://link.springer.com/chapter/10.1007/978-3-030-53291-8_1
  %V 12225
  %@ 978-3-030-53291-8
  

• 1.

  Blondin, M., Esparza, J., Helfrich, M., Kucera, A., Meyer, P.J.: Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. In: Lahiri, S.K. and Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. pp. 372–397. Springer (2020)
  liveness_parametrizedverification_populationprotocols_replicated_systems_verification
  URL: Link

  URLBibTeXEndNote

  @inproceedings{BlondinEH0M20,
  author = {Blondin, Michael and Esparza, Javier and Helfrich, Martin and Kucera, Antoní­n and Meyer, Philipp J.},
  booktitle = {Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II},
  editor = {Lahiri, Shuvendu K. and Wang, Chao},
  keywords = {liveness_parametrizedverification_populationprotocols_replicated_systems_verification},
  month = {October},
  pages = {372-397},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling},
  volume = 12225,
  year = 2020
  }
  

  %0 Conference Paper
  %1 BlondinEH0M20
  %A Blondin, Michael
  %A Esparza, Javier
  %A Helfrich, Martin
  %A Kucera, Antoní­n
  %A Meyer, Philipp J.
  %B Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II
  %D 2020
  %E Lahiri, Shuvendu K.
  %E Wang, Chao
  %I Springer
  %P 372-397
  %R 10.1007/978-3-030-53291-8_20
  %T Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
  %U https://link.springer.com/chapter/10.1007/978-3-030-53291-8_20
  %V 12225
  %@ 978-3-030-53291-8
  

• 1.

  Blondin, M., Esparza, J., Genest, B., Helfrich, M., Jaax, S.: Succinct Population Protocols for Presburger Arithmetic. In: Paul, C. and Bläser, M. (eds.) 37th International Symposium on Theoretical Aspects of Computer Science, STACS 2020, March 10-13, 2020, Montpellier, France. pp. 40:1–40:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
  myown_populationprotocols_succinct_synthesis
  URL: Link

  URLBibTeXEndNote

  @inproceedings{BlondinEGHJ20,
  author = {Blondin, Michael and Esparza, Javier and Genest, Blaise and Helfrich, Martin and Jaax, Stefan},
  booktitle = {37th International Symposium on Theoretical Aspects of Computer Science, STACS 2020, March 10-13, 2020, Montpellier, France},
  editor = {Paul, Christophe and Bläser, Markus},
  keywords = {myown_populationprotocols_succinct_synthesis},
  month = {March},
  pages = {40:1-40:15},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  series = {LIPIcs},
  title = {Succinct Population Protocols for Presburger Arithmetic},
  volume = 154,
  year = 2020
  }
  

  %0 Conference Paper
  %1 BlondinEGHJ20
  %A Blondin, Michael
  %A Esparza, Javier
  %A Genest, Blaise
  %A Helfrich, Martin
  %A Jaax, Stefan
  %B 37th International Symposium on Theoretical Aspects of Computer Science, STACS 2020, March 10-13, 2020, Montpellier, France
  %D 2020
  %E Paul, Christophe
  %E Bläser, Markus
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %P 40:1-40:15
  %R 10.4230/LIPIcs.STACS.2020.40
  %T Succinct Population Protocols for Presburger Arithmetic
  %U https://drops.dagstuhl.de/opus/volltexte/2020/11901/
  %V 154
  %@ 978-3-95977-140-5
  

• 1.

  Raskin, M.: Constructive expressive power of population protocols, (2020)
  expressivepower myown populationprotocols
  Preprint: <a href="http://arxiv.org/abs/2002.07303">Link</a><br>#informal

  AbstractBibTeXEndNote

  Population protocols are a model of distributed computation intended for the study of networks of independent computing agents with dynamic communication structure. Each agent has a finite number of states, and communication opportunities occur nondeterministically, allowing the agents involved to change their states based on each other's states. Population protocols are often studied in terms of reaching a consensus on whether the input configuration satisfied some predicate. In the present paper we propose an alternative point of view. Instead of studying the properties of inputs that a protocol can recognise, we study the properties of outputs that a protocol eventually ensures. We define constructive expressive power. We show that for general population protocols and immediate observation population protocols the constructive expressive power coincides with the normal expressive power. Immediate observation protocols also preserve their relatively low verification complexity in the constructive expressive power setting.

  @misc{raskin2020constructive,
  abstract = {Population protocols are a model of distributed computation intended for the study of networks of independent computing agents with dynamic communication structure. Each agent has a finite number of states, and communication opportunities occur nondeterministically, allowing the agents involved to change their states based on each other's states. Population protocols are often studied in terms of reaching a consensus on whether the input configuration satisfied some predicate. In the present paper we propose an alternative point of view. Instead of studying the properties of inputs that a protocol can recognise, we study the properties of outputs that a protocol eventually ensures. We define constructive expressive power. We show that for general population protocols and immediate observation population protocols the constructive expressive power coincides with the normal expressive power. Immediate observation protocols also preserve their relatively low verification complexity in the constructive expressive power setting.},
  author = {Raskin, Mikhail},
  keywords = {expressivepower myown populationprotocols},
  note = {Preprint: Link
  #informal},
  title = {Constructive expressive power of population protocols},
  year = 2020
  }
  

  %0 Generic
  %1 raskin2020constructive
  %A Raskin, Mikhail
  %D 2020
  %T Constructive expressive power of population protocols
  %X Population protocols are a model of distributed computation intended for the study of networks of independent computing agents with dynamic communication structure. Each agent has a finite number of states, and communication opportunities occur nondeterministically, allowing the agents involved to change their states based on each other's states. Population protocols are often studied in terms of reaching a consensus on whether the input configuration satisfied some predicate. In the present paper we propose an alternative point of view. Instead of studying the properties of inputs that a protocol can recognise, we study the properties of outputs that a protocol eventually ensures. We define constructive expressive power. We show that for general population protocols and immediate observation population protocols the constructive expressive power coincides with the normal expressive power. Immediate observation protocols also preserve their relatively low verification complexity in the constructive expressive power setting.
  

• 1.

  Casteigts, A., Raskin, M., Renken, M., Zamaraev, V.: Sharp Thresholds in Random Simple Temporal Graphs. CoRR. abs/2011.03738, (2020)
  randomgraphs stochasticpopulationprotocols temporalgraphs
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/2011.03738">Link</a><br>#informal

  URLBibTeXEndNote

  @article{journals/corr/abs-2011-03738,
  author = {Casteigts, Arnaud and Raskin, Michael and Renken, Malte and Zamaraev, Viktor},
  journal = {CoRR},
  keywords = {randomgraphs stochasticpopulationprotocols temporalgraphs},
  note = {Preprint: Link
  #informal},
  title = {Sharp Thresholds in Random Simple Temporal Graphs.},
  volume = {abs/2011.03738},
  year = 2020
  }
  

  %0 Journal Article
  %1 journals/corr/abs-2011-03738
  %A Casteigts, Arnaud
  %A Raskin, Michael
  %A Renken, Malte
  %A Zamaraev, Viktor
  %D 2020
  %J CoRR
  %T Sharp Thresholds in Random Simple Temporal Graphs.
  %U http://dblp.uni-trier.de/db/journals/corr/corr2011.html#abs-2011-03738
  %V abs/2011.03738
  

• 1.

  Esparza, J., Kvret’insk’y, J., Sickert, S.: A Unified Translation of Linear Temporal Logic to ω-Automata. J. ACM. 67, (2020)
  LTL OmegaAutomata myown
  URL: Link
  #journal

  AbstractURLBibTeXEndNote

  We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic Büchi automata (LDBA), and nondeterministic Büchi automata (NBA). The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive Boolean combination of languages that can be translated into ω-automata by elementary means. In particular, Safra’s, ranking, and breakpoint constructions used in other translations are not needed. We further give evidence that this theoretical clean and compositional approach does not lead to large automata per se and in fact in the case of DRAs yields significantly smaller automata compared to the previously known approach using determinisation of NBAs.

  @article{10.1145/3417995,
  abstract = {We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic Büchi automata (LDBA), and nondeterministic Büchi automata (NBA). The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive Boolean combination of languages that can be translated into ω-automata by elementary means. In particular, Safra’s, ranking, and breakpoint constructions used in other translations are not needed. We further give evidence that this theoretical clean and compositional approach does not lead to large automata per se and in fact in the case of DRAs yields significantly smaller automata compared to the previously known approach using determinisation of NBAs.},
  address = {New York, NY, USA},
  author = {Esparza, Javier and Kvret'insk'y, Jan and Sickert, Salomon},
  journal = {J. ACM},
  keywords = {LTL OmegaAutomata myown},
  month = {oct},
  note = {#journal},
  number = 6,
  publisher = {Association for Computing Machinery},
  title = {A Unified Translation of Linear Temporal Logic to ω-Automata},
  volume = 67,
  year = 2020
  }
  

  %0 Journal Article
  %1 10.1145/3417995
  %A Esparza, Javier
  %A Kvret'insk'y, Jan
  %A Sickert, Salomon
  %C New York, NY, USA
  %D 2020
  %I Association for Computing Machinery
  %J J. ACM
  %N 6
  %R 10.1145/3417995
  %T A Unified Translation of Linear Temporal Logic to ω-Automata
  %U https://doi.org/10.1145/3417995
  %V 67
  %X We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic Büchi automata (LDBA), and nondeterministic Büchi automata (NBA). The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive Boolean combination of languages that can be translated into ω-automata by elementary means. In particular, Safra’s, ranking, and breakpoint constructions used in other translations are not needed. We further give evidence that this theoretical clean and compositional approach does not lead to large automata per se and in fact in the case of DRAs yields significantly smaller automata compared to the previously known approach using determinisation of NBAs.
  

• 1.

  Seidl, H., Müller, C., Finkbeiner, B.: How to Win First-Order Safety Games. In: Beyer, D. and Zufferey, D. (eds.) VMCAI. pp. 426–448. Springer (2020)
  gametheory myown safety
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/1908.05964">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Functional correctness or noninterference of these systems have conveniently been formulated as safety or hypersafety properties, respectively. In this article, we take the step from verification to synthesis—tackling the question whether it is possible to automatically synthesize predicates to enforce safety or hypersafety properties like noninterference. For that, we generalize FO transition systems to FO safety games. For FO games with monadic predicates only, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal first-order invariants, since these are sufficient to express a large class of properties—for example noninterference. We identify a non-trivial sub-class where invariants can be proven inductive and FO winning strategies be effectively constructed. We also show how the extraction of weakest FO winning strategies can be reduced to SO quantifier elimination itself. We demonstrate the usefulness of our approach by automatically synthesizing nontrivial FO specifications of messages in a leader election protocol as well as for paper assignment in a conference management system to exclude unappreciated disclosure of reports.

  @inproceedings{conf/vmcai/SeidlMF20,
  abstract = {First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Functional correctness or noninterference of these systems have conveniently been formulated as safety or hypersafety properties, respectively. In this article, we take the step from verification to synthesis—tackling the question whether it is possible to automatically synthesize predicates to enforce safety or hypersafety properties like noninterference. For that, we generalize FO transition systems to FO safety games. For FO games with monadic predicates only, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal first-order invariants, since these are sufficient to express a large class of properties—for example noninterference. We identify a non-trivial sub-class where invariants can be proven inductive and FO winning strategies be effectively constructed. We also show how the extraction of weakest FO winning strategies can be reduced to SO quantifier elimination itself. We demonstrate the usefulness of our approach by automatically synthesizing nontrivial FO specifications of messages in a leader election protocol as well as for paper assignment in a conference management system to exclude unappreciated disclosure of reports.},
  author = {Seidl, Helmut and Müller, Christian and Finkbeiner, Bernd},
  booktitle = {VMCAI},
  crossref = {conf/vmcai/2020},
  editor = {Beyer, Dirk and Zufferey, Damien},
  keywords = {gametheory myown safety},
  note = {Preprint: Link
  #conference},
  pages = {426-448},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {How to Win First-Order Safety Games.},
  volume = 11990,
  year = 2020
  }
  

  %0 Conference Paper
  %1 conf/vmcai/SeidlMF20
  %A Seidl, Helmut
  %A Müller, Christian
  %A Finkbeiner, Bernd
  %B VMCAI
  %D 2020
  %E Beyer, Dirk
  %E Zufferey, Damien
  %I Springer
  %P 426-448
  %T How to Win First-Order Safety Games.
  %U https://link.springer.com/chapter/10.1007%2F978-3-030-39322-9_20
  %V 11990
  %X First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Functional correctness or noninterference of these systems have conveniently been formulated as safety or hypersafety properties, respectively. In this article, we take the step from verification to synthesis—tackling the question whether it is possible to automatically synthesize predicates to enforce safety or hypersafety properties like noninterference. For that, we generalize FO transition systems to FO safety games. For FO games with monadic predicates only, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal first-order invariants, since these are sufficient to express a large class of properties—for example noninterference. We identify a non-trivial sub-class where invariants can be proven inductive and FO winning strategies be effectively constructed. We also show how the extraction of weakest FO winning strategies can be reduced to SO quantifier elimination itself. We demonstrate the usefulness of our approach by automatically synthesizing nontrivial FO specifications of messages in a leader election protocol as well as for paper assignment in a conference management system to exclude unappreciated disclosure of reports.
  %@ 978-3-030-39322-9
  

• 1.

  Blondin, M., Raskin, M.A.: The Complexity of Reachability in Affine Vector Addition Systems with States. In: Hermanns, H., Zhang, L., Kobayashi, N., and Miller, D. (eds.) LICS. pp. 224–236. ACM (2020)
  VAS complexity myown rachability
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/1909.02579">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. It is natural to question their feasibility for VASS enriched with primitives that typically translate into undecidability. Spurred by this concern, we pinpoint the complexity of integer relaxations w.r.t. arbitrary classes of affine operations. More specifically, we provide a trichotomy on the complexity of integer reachability in VASS extended with affine operations (affine VASS). Namely, we show that it is NP-complete for VASS with resets, PSPACE-complete for VASS with (pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any other class. We further present a dichotomy for standard reachability in affine VASS: it is decidable for VASS with permutations, and undecidable for any other class. This yields a complete and unified complexity landscape of reachability in affine VASS.

  @inproceedings{conf/lics/BlondinR20,
  abstract = {Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. It is natural to question their feasibility for VASS enriched with primitives that typically translate into undecidability. Spurred by this concern, we pinpoint the complexity of integer relaxations w.r.t. arbitrary classes of affine operations. More specifically, we provide a trichotomy on the complexity of integer reachability in VASS extended with affine operations (affine VASS). Namely, we show that it is NP-complete for VASS with resets, PSPACE-complete for VASS with (pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any other class. We further present a dichotomy for standard reachability in affine VASS: it is decidable for VASS with permutations, and undecidable for any other class. This yields a complete and unified complexity landscape of reachability in affine VASS.},
  author = {Blondin, Michael and Raskin, Mikhail A.},
  booktitle = {LICS},
  crossref = {conf/lics/2020},
  editor = {Hermanns, Holger and Zhang, Lijun and Kobayashi, Naoki and Miller, Dale},
  keywords = {VAS complexity myown rachability},
  note = {Preprint: Link
  #conference},
  pages = {224-236},
  publisher = {ACM},
  title = {The Complexity of Reachability in Affine Vector Addition Systems with States.},
  year = 2020
  }
  

  %0 Conference Paper
  %1 conf/lics/BlondinR20
  %A Blondin, Michael
  %A Raskin, Mikhail A.
  %B LICS
  %D 2020
  %E Hermanns, Holger
  %E Zhang, Lijun
  %E Kobayashi, Naoki
  %E Miller, Dale
  %I ACM
  %P 224-236
  %T The Complexity of Reachability in Affine Vector Addition Systems with States.
  %U https://dl.acm.org/doi/abs/10.1145/3373718.3394741
  %X Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. It is natural to question their feasibility for VASS enriched with primitives that typically translate into undecidability. Spurred by this concern, we pinpoint the complexity of integer relaxations w.r.t. arbitrary classes of affine operations. More specifically, we provide a trichotomy on the complexity of integer reachability in VASS extended with affine operations (affine VASS). Namely, we show that it is NP-complete for VASS with resets, PSPACE-complete for VASS with (pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any other class. We further present a dichotomy for standard reachability in affine VASS: it is decidable for VASS with permutations, and undecidable for any other class. This yields a complete and unified complexity landscape of reachability in affine VASS.
  %@ 978-1-4503-7104-9
  

• 1.

  Balasubramanian, A.R., Esparza, J., Lazic, M.: Complexity of Verification and Synthesis of Threshold Automata. CoRR. abs/2007.06248, (2020)
  complexity myown preprint synthesis thresholdautomata verification
  Preprint: <a href="https://arxiv.org/abs/2007.06248">Link</a><br>#informal

  AbstractBibTeXEndNote

  Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed by a fixed but arbitrary number of processes. We conduct the first systematic study of the complexity of verification and synthesis problems for threshold automata. We prove that the coverability, reachability, safety, and liveness problems are NP-complete, and that the bounded synthesis problem is Σ^2_p complete. A key to our results is a novel characterization of the reachability relation of a threshold automaton as an existential Presburger formula. The characterization also leads to novel verification and synthesis algorithms. We report on an implementation, and provide experimental results.

  @article{journals/corr/abs-2007-06248,
  abstract = {Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed by a fixed but arbitrary number of processes. We conduct the first systematic study of the complexity of verification and synthesis problems for threshold automata. We prove that the coverability, reachability, safety, and liveness problems are NP-complete, and that the bounded synthesis problem is Σ^2_p complete. A key to our results is a novel characterization of the reachability relation of a threshold automaton as an existential Presburger formula. The characterization also leads to novel verification and synthesis algorithms. We report on an implementation, and provide experimental results.},
  author = {Balasubramanian, A. R. and Esparza, Javier and Lazic, Marijana},
  journal = {CoRR},
  keywords = {complexity myown preprint synthesis thresholdautomata verification},
  note = {Preprint: Link
  #informal},
  title = {Complexity of Verification and Synthesis of Threshold Automata.},
  volume = {abs/2007.06248},
  year = 2020
  }
  

  %0 Journal Article
  %1 journals/corr/abs-2007-06248
  %A Balasubramanian, A. R.
  %A Esparza, Javier
  %A Lazic, Marijana
  %D 2020
  %J CoRR
  %T Complexity of Verification and Synthesis of Threshold Automata.
  %V abs/2007.06248
  %X Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed by a fixed but arbitrary number of processes. We conduct the first systematic study of the complexity of verification and synthesis problems for threshold automata. We prove that the coverability, reachability, safety, and liveness problems are NP-complete, and that the bounded synthesis problem is Σ^2_p complete. A key to our results is a novel characterization of the reachability relation of a threshold automaton as an existential Presburger formula. The characterization also leads to novel verification and synthesis algorithms. We report on an implementation, and provide experimental results.
  

• 1.

  Balasubramanian, A.R., Walukiewicz, I.: Characterizing Consensus in the Heard-Of Model. In: Konnov, I. and Kovács, L. (eds.) 31st International Conference on Concurrency Theory (CONCUR 2020). pp. 9:1–9:18. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020)
  HeardOfmodel consensusproblem myown verification
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/2004.09621">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragment of this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm.

  @inproceedings{balasubramanian_et_al:LIPIcs:2020:12821,
  abstract = {The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragment of this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm.},
  address = {Dagstuhl, Germany},
  annote = {Keywords: consensus problem, Heard-Of model, verification},
  author = {Balasubramanian, A. R. and Walukiewicz, Igor},
  booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
  editor = {Konnov, Igor and Kovács, Laura},
  keywords = {HeardOfmodel consensusproblem myown verification},
  note = {Preprint: Link
  #conference},
  pages = {9:1--9:18},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {Characterizing Consensus in the Heard-Of Model},
  volume = 171,
  year = 2020
  }
  

  %0 Conference Paper
  %1 balasubramanian_et_al:LIPIcs:2020:12821
  %A Balasubramanian, A. R.
  %A Walukiewicz, Igor
  %B 31st International Conference on Concurrency Theory (CONCUR 2020)
  %C Dagstuhl, Germany
  %D 2020
  %E Konnov, Igor
  %E Kovács, Laura
  %I Schloss Dagstuhl--Leibniz-Zentrum für Informatik
  %P 9:1--9:18
  %R 10.4230/LIPIcs.CONCUR.2020.9
  %T Characterizing Consensus in the Heard-Of Model
  %U https://drops.dagstuhl.de/opus/volltexte/2020/12821
  %V 171
  %X The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragment of this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm.
  %Z Keywords: consensus problem, Heard-Of model, verification
  %@ 978-3-95977-160-3
  

• 1.

  Balasubramanian, A.R.: Complexity of controlled bad sequences over finite sets of Nd. In: Hermanns, H., Zhang, L., Kobayashi, N., and Miller, D. (eds.) LICS. pp. 130–140. ACM (2020)
  complexity myown
  URL: Link
  Preprint: <a href=https://arxiv.org/abs/1909.01667>Link</a><br>#conference

  AbstractURLBibTeXEndNote

  We provide upper and lower bounds for the length of controlled bad sequences over the majoring and the minoring orderings of finite sets of N^d. The results are obtained by bounding the length of such sequences by functions from the Cichon hierarchy. This allows us to translate these results to bounds over the fast-growing complexity classes. The obtained bounds are proven to be tight for the majoring ordering, which solves a problem left open by Abriola, Figueira and Senno (Theor. Comp. Sci, Vol. 603). Finally, we use the results on controlled bad sequences to prove upper bounds for the emptiness problem of some classes of automata.

  @inproceedings{conf/lics/Balasubramanian20,
  abstract = {We provide upper and lower bounds for the length of controlled bad sequences over the majoring and the minoring orderings of finite sets of N^d. The results are obtained by bounding the length of such sequences by functions from the Cichon hierarchy. This allows us to translate these results to bounds over the fast-growing complexity classes. The obtained bounds are proven to be tight for the majoring ordering, which solves a problem left open by Abriola, Figueira and Senno (Theor. Comp. Sci, Vol. 603). Finally, we use the results on controlled bad sequences to prove upper bounds for the emptiness problem of some classes of automata.},
  author = {Balasubramanian, A. R.},
  booktitle = {LICS},
  crossref = {conf/lics/2020},
  editor = {Hermanns, Holger and Zhang, Lijun and Kobayashi, Naoki and Miller, Dale},
  keywords = {complexity myown},
  note = {Preprint: Link
  #conference},
  pages = {130-140},
  publisher = {ACM},
  title = {Complexity of controlled bad sequences over finite sets of Nd.},
  year = 2020
  }
  

  %0 Conference Paper
  %1 conf/lics/Balasubramanian20
  %A Balasubramanian, A. R.
  %B LICS
  %D 2020
  %E Hermanns, Holger
  %E Zhang, Lijun
  %E Kobayashi, Naoki
  %E Miller, Dale
  %I ACM
  %P 130-140
  %T Complexity of controlled bad sequences over finite sets of Nd.
  %U https://dl.acm.org/doi/abs/10.1145/3373718.3394753
  %X We provide upper and lower bounds for the length of controlled bad sequences over the majoring and the minoring orderings of finite sets of N^d. The results are obtained by bounding the length of such sequences by functions from the Cichon hierarchy. This allows us to translate these results to bounds over the fast-growing complexity classes. The obtained bounds are proven to be tight for the majoring ordering, which solves a problem left open by Abriola, Figueira and Senno (Theor. Comp. Sci, Vol. 603). Finally, we use the results on controlled bad sequences to prove upper bounds for the emptiness problem of some classes of automata.
  %@ 978-1-4503-7104-9
  

• 1.

  Courcelle, B., Durand, I., Raskin, M.: A unified algorithm for colouring graphs of bounded clique-width. (2020)
  finiteautomata graphexploration myown
  Preprint: <a href="http://arxiv.org/abs/2008.07468">Link</a><br>#informal

  AbstractBibTeXEndNote

  Clique-width is one of the graph complexity measures leading to polynomial special-case algorithms for generally NP-complete problems, e.g. graph colourability. The best two currently known algorithms for verifying c-colourability of graphs represented as clique-width terms are optimised towards two different extreme cases, a constant number of colours and a very large number of colours. We present a way to unify these approaches in a single relatively simple algorithm that achieves the state of the art complexity in both cases. The unified algorithm also provides a speed-up for a large number of colours.

  @article{courcelle2020unified,
  abstract = {Clique-width is one of the graph complexity measures leading to polynomial special-case algorithms for generally NP-complete problems, e.g. graph colourability. The best two currently known algorithms for verifying c-colourability of graphs represented as clique-width terms are optimised towards two different extreme cases, a constant number of colours and a very large number of colours. We present a way to unify these approaches in a single relatively simple algorithm that achieves the state of the art complexity in both cases. The unified algorithm also provides a speed-up for a large number of colours.},
  author = {Courcelle, Bruno and Durand, Irène and Raskin, Michael},
  keywords = {finiteautomata graphexploration myown},
  note = {Preprint: Link
  #informal},
  title = {A unified algorithm for colouring graphs of bounded clique-width.},
  year = 2020
  }
  

  %0 Journal Article
  %1 courcelle2020unified
  %A Courcelle, Bruno
  %A Durand, Irène
  %A Raskin, Michael
  %D 2020
  %T A unified algorithm for colouring graphs of bounded clique-width.
  %X Clique-width is one of the graph complexity measures leading to polynomial special-case algorithms for generally NP-complete problems, e.g. graph colourability. The best two currently known algorithms for verifying c-colourability of graphs represented as clique-width terms are optimised towards two different extreme cases, a constant number of colours and a very large number of colours. We present a way to unify these approaches in a single relatively simple algorithm that achieves the state of the art complexity in both cases. The unified algorithm also provides a speed-up for a large number of colours.
  

• 1.

  Sickert, S., Esparza, J.: An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 831–844. Association for Computing Machinery, Saarbr{ü}cken, Germany (2020)
  AlternatingAutomata DeterministicForm LinearLogic Normal Temporal Weak
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/2005.00472">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form Λni =1 GFφi ∨FGψi, where φi and ψi contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.

  @inproceedings{10.1145/3373718.3394743,
  abstract = {In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form Λni =1 GFφi ∨FGψi, where φi and ψi contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.},
  address = {New York, NY, USA},
  author = {Sickert, Salomon and Esparza, Javier},
  booktitle = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science},
  keywords = {AlternatingAutomata DeterministicForm LinearLogic Normal Temporal Weak},
  note = {Preprint: Link
  #conference},
  pages = {831–844},
  publisher = {Association for Computing Machinery},
  series = {LICS '20},
  title = {An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata},
  year = 2020
  }
  

  %0 Conference Paper
  %1 10.1145/3373718.3394743
  %A Sickert, Salomon
  %A Esparza, Javier
  %B Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
  %C New York, NY, USA
  %D 2020
  %I Association for Computing Machinery
  %P 831–844
  %R 10.1145/3373718.3394743
  %T An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
  %U https://doi.org/10.1145/3373718.3394743
  %X In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form Λni =1 GFφi ∨FGψi, where φi and ψi contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.
  %@ 9781450371049
  

• 1.

  Blondin, M., Esparza, J., Helfrich, M., Kucera, A., Meyer, P.J.: Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. In: Lahiri, S.K. and Wang, C. (eds.) CAV (2). pp. 372–397. Springer (2020)
  liveness parametrizedverification populationprotocols replicated systems verification
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/2005.03555">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.

  @inproceedings{conf/cav/BlondinEH0M20,
  abstract = {We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.},
  author = {Blondin, Michael and Esparza, Javier and Helfrich, Martin and Kucera, Antonín and Meyer, Philipp J.},
  booktitle = {CAV (2)},
  crossref = {conf/cav/2020-2},
  editor = {Lahiri, Shuvendu K. and Wang, Chao},
  keywords = {liveness parametrizedverification populationprotocols replicated systems verification},
  note = {Preprint: Link
  #conference},
  pages = {372-397},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling.},
  volume = 12225,
  year = 2020
  }
  

  %0 Conference Paper
  %1 conf/cav/BlondinEH0M20
  %A Blondin, Michael
  %A Esparza, Javier
  %A Helfrich, Martin
  %A Kucera, Antonín
  %A Meyer, Philipp J.
  %B CAV (2)
  %D 2020
  %E Lahiri, Shuvendu K.
  %E Wang, Chao
  %I Springer
  %P 372-397
  %T Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling.
  %U https://link.springer.com/chapter/10.1007/978-3-030-53291-8_20
  %V 12225
  %X We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.
  %@ 978-3-030-53291-8
  

• 1.

  Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Inf. 57, 3–36 (2020)
  LTL myown sy synthesis
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/1903.12576">Link</a><br>#journal

  AbstractURLBibTeXEndNote

  The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.

  @article{journals/acta/LuttenbergerMS20,
  abstract = {The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.},
  author = {Luttenberger, Michael and Meyer, Philipp J. and Sickert, Salomon},
  journal = {Acta Inf.},
  keywords = {LTL myown sy synthesis},
  note = {Preprint: Link
  #journal},
  number = {1-2},
  pages = {3-36},
  title = {Practical synthesis of reactive systems from LTL specifications via parity games.},
  volume = 57,
  year = 2020
  }
  

  %0 Journal Article
  %1 journals/acta/LuttenbergerMS20
  %A Luttenberger, Michael
  %A Meyer, Philipp J.
  %A Sickert, Salomon
  %D 2020
  %J Acta Inf.
  %N 1-2
  %P 3-36
  %R 10.1007/s00236-019-00349-3
  %T Practical synthesis of reactive systems from LTL specifications via parity games.
  %U https://doi.org/10.1007/s00236-019-00349-3
  %V 57
  %X The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.
  

• 1.

  Jaax, S., Kiefer, S.: On Affine Reachability Problems. In: Esparza, J. and Král’, D. (eds.) MFCS. pp. 48:1–48:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
  affine-reachability scalar-reachability vector-reachability
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/1905.05114">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  We analyze affine reachability problems in dimensions 1 and 2. We show that the reachability problem for 1-register machines over the integers with affine updates is PSPACE-hard, hence PSPACE-complete, strengthening a result by Finkel et al. that required polynomial updates. Building on recent results on two-dimensional integer matrices, we prove NP-completeness of the mortality problem for 2-dimensional integer matrices with determinants +1 and 0. Motivated by tight connections with 1-dimensional affine reachability problems without control states, we also study the complexity of a number of reachability problems in finitely generated semigroups of 2-dimensional upper-triangular integer matrices.

  @inproceedings{DBLP:conf/mfcs/JaaxK20,
  abstract = {We analyze affine reachability problems in dimensions 1 and 2. We show that the reachability problem for 1-register machines over the integers with affine updates is PSPACE-hard, hence PSPACE-complete, strengthening a result by Finkel et al. that required polynomial updates. Building on recent results on two-dimensional integer matrices, we prove NP-completeness of the mortality problem for 2-dimensional integer matrices with determinants +1 and 0. Motivated by tight connections with 1-dimensional affine reachability problems without control states, we also study the complexity of a number of reachability problems in finitely generated semigroups of 2-dimensional upper-triangular integer matrices.},
  author = {Jaax, Stefan and Kiefer, Stefan},
  booktitle = {MFCS},
  editor = {Esparza, Javier and Král', Daniel},
  keywords = {affine-reachability scalar-reachability vector-reachability},
  note = {Preprint: Link
  #conference},
  pages = {48:1--48:14},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  series = {LIPIcs},
  title = {On Affine Reachability Problems},
  volume = 170,
  year = 2020
  }
  

  %0 Conference Paper
  %1 DBLP:conf/mfcs/JaaxK20
  %A Jaax, Stefan
  %A Kiefer, Stefan
  %B MFCS
  %D 2020
  %E Esparza, Javier
  %E Král', Daniel
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %P 48:1--48:14
  %R 10.4230/LIPIcs.MFCS.2020.48
  %T On Affine Reachability Problems
  %U https://doi.org/10.4230/LIPIcs.MFCS.2020.48
  %V 170
  %X We analyze affine reachability problems in dimensions 1 and 2. We show that the reachability problem for 1-register machines over the integers with affine updates is PSPACE-hard, hence PSPACE-complete, strengthening a result by Finkel et al. that required polynomial updates. Building on recent results on two-dimensional integer matrices, we prove NP-completeness of the mortality problem for 2-dimensional integer matrices with determinants +1 and 0. Motivated by tight connections with 1-dimensional affine reachability problems without control states, we also study the complexity of a number of reachability problems in finitely generated semigroups of 2-dimensional upper-triangular integer matrices.
  

• 1.

  D’Antoni, L., Helfrich, M., Kretinsky, J., Ramneantu, E., Weininger, M.: Automata Tutor v3. In: Lahiri, S.K. and Wang, C. (eds.) CAV (2). pp. 3–14. Springer (2020)
  tool
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/2005.01419">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  Computer science class enrollments have rapidly risen in the past decade. With current class sizes, standard approaches to grading and providing personalized feedback are no longer possible and new techniques become both feasible and necessary. In this paper, we present the third version of Automata Tutor, a tool for helping teachers and students in large courses on automata and formal languages. The second version of Automata Tutor supported automatic grading and feedback for finite-automata constructions and has already been used by thousands of users in dozens of countries. This new version of Automata Tutor supports automated grading and feedback generation for a greatly extended variety of new problems, including problems that ask students to create regular expressions, context-free grammars, pushdown automata and Turing machines corresponding to a given description, and problems about converting between equivalent models - e.g., from regular expressions to nondeterministic finite automata. Moreover, for several problems, this new version also enables teachers and students to automatically generate new problem instances. We also present the results of a survey run on a class of 950 students, which shows very positive results about the usability and usefulness of the tool.

  @inproceedings{conf/cav/DAntoniHKRW20,
  abstract = {Computer science class enrollments have rapidly risen in the past decade. With current class sizes, standard approaches to grading and providing personalized feedback are no longer possible and new techniques become both feasible and necessary. In this paper, we present the third version of Automata Tutor, a tool for helping teachers and students in large courses on automata and formal languages. The second version of Automata Tutor supported automatic grading and feedback for finite-automata constructions and has already been used by thousands of users in dozens of countries. This new version of Automata Tutor supports automated grading and feedback generation for a greatly extended variety of new problems, including problems that ask students to create regular expressions, context-free grammars, pushdown automata and Turing machines corresponding to a given description, and problems about converting between equivalent models - e.g., from regular expressions to nondeterministic finite automata. Moreover, for several problems, this new version also enables teachers and students to automatically generate new problem instances. We also present the results of a survey run on a class of 950 students, which shows very positive results about the usability and usefulness of the tool.},
  author = {D'Antoni, Loris and Helfrich, Martin and Kretinsky, Jan and Ramneantu, Emanuel and Weininger, Maximilian},
  booktitle = {CAV (2)},
  crossref = {conf/cav/2020-2},
  editor = {Lahiri, Shuvendu K. and Wang, Chao},
  keywords = {tool},
  note = {Preprint: Link
  #conference},
  pages = {3-14},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Automata Tutor v3.},
  volume = 12225,
  year = 2020
  }
  

  %0 Conference Paper
  %1 conf/cav/DAntoniHKRW20
  %A D'Antoni, Loris
  %A Helfrich, Martin
  %A Kretinsky, Jan
  %A Ramneantu, Emanuel
  %A Weininger, Maximilian
  %B CAV (2)
  %D 2020
  %E Lahiri, Shuvendu K.
  %E Wang, Chao
  %I Springer
  %P 3-14
  %T Automata Tutor v3.
  %U https://link.springer.com/chapter/10.1007/978-3-030-53291-8_1
  %V 12225
  %X Computer science class enrollments have rapidly risen in the past decade. With current class sizes, standard approaches to grading and providing personalized feedback are no longer possible and new techniques become both feasible and necessary. In this paper, we present the third version of Automata Tutor, a tool for helping teachers and students in large courses on automata and formal languages. The second version of Automata Tutor supported automatic grading and feedback for finite-automata constructions and has already been used by thousands of users in dozens of countries. This new version of Automata Tutor supports automated grading and feedback generation for a greatly extended variety of new problems, including problems that ask students to create regular expressions, context-free grammars, pushdown automata and Turing machines corresponding to a given description, and problems about converting between equivalent models - e.g., from regular expressions to nondeterministic finite automata. Moreover, for several problems, this new version also enables teachers and students to automatically generate new problem instances. We also present the results of a survey run on a class of 950 students, which shows very positive results about the usability and usefulness of the tool.
  %@ 978-3-030-53291-8
  

• 1.

  Durand, I., Courcelle, B., Raskin, M.: On defining linear orders by automata. Moscow Journal of Combinatorics and Number Theory. 9, 253–291 (2020)
  automata expressivepower myown
  URL: Link
  Preprint: <a href="https://hal.archives-ouvertes.fr/hal-02397982/">Link</a><br>#journal

  AbstractURLBibTeXEndNote

  We define linear orders ≤Z on product sets Z := X1 × X2 × ... × Xn and on subsets Z of X1 × X2 where each composing set Xi is [0, p] or N, and ordered in the natural way. We require that (Z, ≤Z) be isomor-phic to (N, ≤) if it is infinite. We want linear orderings of Z such that, in two consecutive tuples z = (z1, ..., zn) and z = (z 1 , ..., z n), we have |zi − z i | ≤ 1 for each i. Furthermore, we define their distance d(z, z) as the number of indices i such that zi = z i. We will consider orderings where the distance of two consecutive tuples is at most 2. We are interested in algorithms that determine the tuple in Z following z by using local information, where "local" is meant with respect to graphs associated with Z, and that work as well for finite and infinite components Xi, without knowing whether the components Xi are finite or not. We will formalize these algorithms by deterministic graph-walking automata.

  @article{irenedurand2020defining,
  abstract = {We define linear orders ≤Z on product sets Z := X1 × X2 × ... × Xn and on subsets Z of X1 × X2 where each composing set Xi is [0, p] or N, and ordered in the natural way. We require that (Z, ≤Z) be isomor-phic to (N, ≤) if it is infinite. We want linear orderings of Z such that, in two consecutive tuples z = (z1, ..., zn) and z = (z 1 , ..., z n), we have |zi − z i | ≤ 1 for each i. Furthermore, we define their distance d(z, z) as the number of indices i such that zi = z i. We will consider orderings where the distance of two consecutive tuples is at most 2. We are interested in algorithms that determine the tuple in Z following z by using local information, where "local" is meant with respect to graphs associated with Z, and that work as well for finite and infinite components Xi, without knowing whether the components Xi are finite or not. We will formalize these algorithms by deterministic graph-walking automata.},
  author = {Durand, Irène and Courcelle, Bruno and Raskin, Michael},
  journal = {Moscow Journal of Combinatorics and Number Theory},
  keywords = {automata expressivepower myown},
  note = {Preprint: Link
  #journal},
  number = 3,
  pages = {253-291},
  title = {On defining linear orders by automata},
  volume = 9,
  year = 2020
  }
  

  %0 Journal Article
  %1 irenedurand2020defining
  %A Durand, Irène
  %A Courcelle, Bruno
  %A Raskin, Michael
  %D 2020
  %J Moscow Journal of Combinatorics and Number Theory
  %N 3
  %P 253-291
  %R 10.2140/moscow.2020.9.253
  %T On defining linear orders by automata
  %U https://msp.org/moscow/2020/9-3/p03.xhtml
  %V 9
  %X We define linear orders ≤Z on product sets Z := X1 × X2 × ... × Xn and on subsets Z of X1 × X2 where each composing set Xi is [0, p] or N, and ordered in the natural way. We require that (Z, ≤Z) be isomor-phic to (N, ≤) if it is infinite. We want linear orderings of Z such that, in two consecutive tuples z = (z1, ..., zn) and z = (z 1 , ..., z n), we have |zi − z i | ≤ 1 for each i. Furthermore, we define their distance d(z, z) as the number of indices i such that zi = z i. We will consider orderings where the distance of two consecutive tuples is at most 2. We are interested in algorithms that determine the tuple in Z following z by using local information, where "local" is meant with respect to graphs associated with Z, and that work as well for finite and infinite components Xi, without knowing whether the components Xi are finite or not. We will formalize these algorithms by deterministic graph-walking automata.
  

• 1.

  Raskin, M., Weil-Kennedy, C., Esparza, J.: Flatness and Complexity of Immediate Observation Petri Nets. 31st International Conference on Concurrency Theory (CONCUR 2020). Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
  flatness immediateobservation myown reachability
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/2001.09966">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  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.

  @inproceedings{raskin2020flatness,
  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.},
  author = {Raskin, Mikhail and Weil-Kennedy, Chana and Esparza, Javier},
  booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
  keywords = {flatness immediateobservation myown reachability},
  note = {Preprint: Link
  #conference},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title = {Flatness and Complexity of Immediate Observation Petri Nets},
  year = 2020
  }
  

  %0 Conference Paper
  %1 raskin2020flatness
  %A Raskin, Mikhail
  %A Weil-Kennedy, Chana
  %A Esparza, Javier
  %B 31st International Conference on Concurrency Theory (CONCUR 2020)
  %D 2020
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %R 10.4230/LIPICS.CONCUR.2020.45
  %T Flatness and Complexity of Immediate Observation Petri Nets
  %U https://drops.dagstuhl.de/opus/volltexte/2020/12857/
  %X 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.
  

2019

• 1.

  Esparza, J.: Coffee and Cigarettes. In: Reisig, W. and Rozenberg, G. (eds.) Carl Adam Petri: Ideas, Personality, Impact. pp. 97–103. Springer (2019)
  petrinets
  URL: Link

  AbstractURLBibTeXEndNote

  Drawing inspiration for his chapter title from a Jim Jarmusch film, the author describes an encounter with Carl Adam Petri that captures his unusual style and his deep and original thinking.

  @incollection{books/sp/19/Esparza19,
  abstract = {Drawing inspiration for his chapter title from a Jim Jarmusch film, the author describes an encounter with Carl Adam Petri that captures his unusual style and his deep and original thinking.},
  author = {Esparza, Javier},
  booktitle = {Carl Adam Petri: Ideas, Personality, Impact},
  crossref = {books/sp/RR2019},
  editor = {Reisig, Wolfgang and Rozenberg, Grzegorz},
  keywords = {petrinets},
  pages = {97-103},
  publisher = {Springer},
  title = {Coffee and Cigarettes.},
  year = 2019
  }
  

  %0 Book Section
  %1 books/sp/19/Esparza19
  %A Esparza, Javier
  %B Carl Adam Petri: Ideas, Personality, Impact
  %D 2019
  %E Reisig, Wolfgang
  %E Rozenberg, Grzegorz
  %I Springer
  %P 97-103
  %R 10.1007/978-3-319-96154-5_13
  %T Coffee and Cigarettes.
  %U https://doi.org/10.1007/978-3-319-96154-5_13
  %X Drawing inspiration for his chapter title from a Jim Jarmusch film, the author describes an encounter with Carl Adam Petri that captures his unusual style and his deep and original thinking.
  %@ 978-3-319-96154-5
  

• 1.

  Esparza, J., Raskin, M., Weil-Kennedy, C.: Parameterized Analysis of Immediate Observation Petri Nets. In: Donatelli, S. and Haar, S. (eds.) Petri Nets. pp. 365–385. Springer (2019)
  immediateobservation populationprotocols
  URL: Link
  #conference

  AbstractURLBibTeXEndNote

  We introduce immediate observation Petri nets, a class of interest in the study of population protocols (a model of distributed computation), and enzymatic chemical networks. In these areas, relevant analysis questions translate into parameterized Petri net problems: whether an infinite set of Petri nets with the same underlying net, but different initial markings, satisfy a given property. We study the parameterized reachability, coverability, and liveness problems for immediate observation Petri nets. We show that all three problems are in PSPACE for infinite sets of initial markings defined by counting constraints, a class sufficiently rich for the intended application. This is remarkable, since the problems are already PSPACE-hard when the set of markings is a singleton, i.e., in the non-parameterized case. We use these results to prove that the correctness problem for immediate observation population protocols is PSPACE-complete, answering a question left open in a previous paper.

  @inproceedings{conf/apn/EsparzaRW19,
  abstract = {We introduce immediate observation Petri nets, a class of interest in the study of population protocols (a model of distributed computation), and enzymatic chemical networks. In these areas, relevant analysis questions translate into parameterized Petri net problems: whether an infinite set of Petri nets with the same underlying net, but different initial markings, satisfy a given property. We study the parameterized reachability, coverability, and liveness problems for immediate observation Petri nets. We show that all three problems are in PSPACE for infinite sets of initial markings defined by counting constraints, a class sufficiently rich for the intended application. This is remarkable, since the problems are already PSPACE-hard when the set of markings is a singleton, i.e., in the non-parameterized case. We use these results to prove that the correctness problem for immediate observation population protocols is PSPACE-complete, answering a question left open in a previous paper.},
  author = {Esparza, Javier and Raskin, Mikhail and Weil-Kennedy, Chana},
  booktitle = {Petri Nets},
  crossref = {conf/apn/2019},
  editor = {Donatelli, Susanna and Haar, Stefan},
  keywords = {immediateobservation populationprotocols},
  note = {#conference},
  pages = {365-385},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Parameterized Analysis of Immediate Observation Petri Nets.},
  volume = 11522,
  year = 2019
  }
  

  %0 Conference Paper
  %1 conf/apn/EsparzaRW19
  %A Esparza, Javier
  %A Raskin, Mikhail
  %A Weil-Kennedy, Chana
  %B Petri Nets
  %D 2019
  %E Donatelli, Susanna
  %E Haar, Stefan
  %I Springer
  %P 365-385
  %R 10.1007/978-3-030-21571-2_20
  %T Parameterized Analysis of Immediate Observation Petri Nets.
  %U https://doi.org/10.1007/978-3-030-21571-2_20
  %V 11522
  %X We introduce immediate observation Petri nets, a class of interest in the study of population protocols (a model of distributed computation), and enzymatic chemical networks. In these areas, relevant analysis questions translate into parameterized Petri net problems: whether an infinite set of Petri nets with the same underlying net, but different initial markings, satisfy a given property. We study the parameterized reachability, coverability, and liveness problems for immediate observation Petri nets. We show that all three problems are in PSPACE for infinite sets of initial markings defined by counting constraints, a class sufficiently rich for the intended application. This is remarkable, since the problems are already PSPACE-hard when the set of markings is a singleton, i.e., in the non-parameterized case. We use these results to prove that the correctness problem for immediate observation population protocols is PSPACE-complete, answering a question left open in a previous paper.
  %@ 978-3-030-21571-2
  

• 1.

  Jaax, S., Kiefer, S.: On Semigroups of Two-Dimensional Upper-Triangular Integer Matrices. CoRR. abs/1905.05114, (2019)
  groups matrix reachability semi
  Preprint: <a href="https://arxiv.org/abs/1905.05114">Link</a><br>#informal

  BibTeXEndNote

  @article{journals/corr/abs-1905-05114,
  author = {Jaax, Stefan and Kiefer, Stefan},
  journal = {CoRR},
  keywords = {groups matrix reachability semi},
  note = {Preprint: Link
  #informal},
  title = {On Semigroups of Two-Dimensional Upper-Triangular Integer Matrices.},
  volume = {abs/1905.05114},
  year = 2019
  }
  

  %0 Journal Article
  %1 journals/corr/abs-1905-05114
  %A Jaax, Stefan
  %A Kiefer, Stefan
  %D 2019
  %J CoRR
  %T On Semigroups of Two-Dimensional Upper-Triangular Integer Matrices.
  %V abs/1905.05114
  

• 1.

  Blondin, M., Esparza, J., Jaax, S.: Expressive Power of Oblivious Consensus Protocols, http://arxiv.org/abs/1902.01668, (2019)
  broadcast population protocols
  URL: Link
  #informal

  AbstractURLBibTeXEndNote

  Population protocols are a formal model of computation by identical, anonymous mobile agents interacting in pairs. It has been shown that their computational power is rather limited: They can only compute the predicates expressible in Presburger arithmetic. Population protocols are oblivious, in the sense that their behavior only depends on the number of agents in each state of the current configuration, and nothing else. Obliviousness has advantages for applications where agents want to reveal as little as possible about their trajectories in a computation. We investigate the computational power of oblivious protocols. We first show that, under a weak assumption, oblivious protocols can only compute number predicates \($\varphi : \mathbbN^m \rightarrow \0, 1\$\) in NSPACE(n) (with the input written, as usual, in binary), while all predicates computed by population protocols are in DSPACE(log n), thus proving an exponential gap. Then we introduce broadcast consensus protocols, in which agents can also broadcast signals to all other agents. We prove that they compute all predicates in NSPACE(n), reaching the theoretical limit for oblivious protocols. Finally, we conduct the first systematic comparison of different models introduced in the literature (population protocols, broadcast protocols, community protocols, and mediated protocols) with respect to their computational power and their privacy guarantees.

  @preprint{blondin2019expressive,
  abstract = {Population protocols are a formal model of computation by identical, anonymous mobile agents interacting in pairs. It has been shown that their computational power is rather limited: They can only compute the predicates expressible in Presburger arithmetic. Population protocols are oblivious, in the sense that their behavior only depends on the number of agents in each state of the current configuration, and nothing else. Obliviousness has advantages for applications where agents want to reveal as little as possible about their trajectories in a computation. We investigate the computational power of oblivious protocols. We first show that, under a weak assumption, oblivious protocols can only compute number predicates \($\varphi : \mathbbN^m \rightarrow \0, 1\$\) in NSPACE(n) (with the input written, as usual, in binary), while all predicates computed by population protocols are in DSPACE(log n), thus proving an exponential gap. Then we introduce broadcast consensus protocols, in which agents can also broadcast signals to all other agents. We prove that they compute all predicates in NSPACE(n), reaching the theoretical limit for oblivious protocols. Finally, we conduct the first systematic comparison of different models introduced in the literature (population protocols, broadcast protocols, community protocols, and mediated protocols) with respect to their computational power and their privacy guarantees.},
  author = {Blondin, Michael and Esparza, Javier and Jaax, Stefan},
  keywords = {broadcast population protocols},
  note = {#informal},
  title = {Expressive Power of Oblivious Consensus Protocols},
  year = 2019
  }
  

  %0 Generic
  %1 blondin2019expressive
  %A Blondin, Michael
  %A Esparza, Javier
  %A Jaax, Stefan
  %D 2019
  %T Expressive Power of Oblivious Consensus Protocols
  %U http://arxiv.org/abs/1902.01668
  %X Population protocols are a formal model of computation by identical, anonymous mobile agents interacting in pairs. It has been shown that their computational power is rather limited: They can only compute the predicates expressible in Presburger arithmetic. Population protocols are oblivious, in the sense that their behavior only depends on the number of agents in each state of the current configuration, and nothing else. Obliviousness has advantages for applications where agents want to reveal as little as possible about their trajectories in a computation. We investigate the computational power of oblivious protocols. We first show that, under a weak assumption, oblivious protocols can only compute number predicates \($\varphi : \mathbbN^m \rightarrow \0, 1\$\) in NSPACE(n) (with the input written, as usual, in binary), while all predicates computed by population protocols are in DSPACE(log n), thus proving an exponential gap. Then we introduce broadcast consensus protocols, in which agents can also broadcast signals to all other agents. We prove that they compute all predicates in NSPACE(n), reaching the theoretical limit for oblivious protocols. Finally, we conduct the first systematic comparison of different models introduced in the literature (population protocols, broadcast protocols, community protocols, and mediated protocols) with respect to their computational power and their privacy guarantees.
  

• 1.

  Meyer, P.J., Esparza, J., Offtermatt, P.: Computing the Expected Execution Time of Probabilistic Workflow Nets. In: Vojnar, T. and Zhang, L. (eds.) TACAS (2). pp. 154–171. Springer (2019)
  expectedterminationtime petrinets
  URL: Link
  #conference

  AbstractURLBibTeXEndNote

  Free-Choice Workflow Petri nets, also known as Workflow Graphs, are a popular model in Business Process Modeling. In this paper we introduce Timed Probabilistic Workflow Nets (TPWNs), and give them a Markov Decision Process (MDP) semantics. Since the time needed to execute two parallel tasks is the maximum of the times, and not their sum, the expected time cannot be directly computed using the theory of MDPs with rewards. In our first contribution, we overcome this obstacle with the help of “earliest-first” schedulers, and give a single exponential-time algorithm for computing the expected time. In our second contribution, we show that computing the expected time is #P -hard, and so polynomial algorithms are very unlikely to exist. Further, #P -hardness holds even for workflows with a very simple structure in which all transitions times are 1 or 0, and all probabilities are 1 or 0.5. Our third and final contribution is an experimental investigation of the runtime of our algorithm on a set of industrial benchmarks. Despite the negative theoretical results, the results are very encouraging. In particular, the expected time of every workflow in a popular benchmark suite with 642 workflow nets can be computed in milliseconds. Data or code related to this paper is available at: [24].

  @inproceedings{conf/tacas/MeyerEO19,
  abstract = {Free-Choice Workflow Petri nets, also known as Workflow Graphs, are a popular model in Business Process Modeling. In this paper we introduce Timed Probabilistic Workflow Nets (TPWNs), and give them a Markov Decision Process (MDP) semantics. Since the time needed to execute two parallel tasks is the maximum of the times, and not their sum, the expected time cannot be directly computed using the theory of MDPs with rewards. In our first contribution, we overcome this obstacle with the help of “earliest-first” schedulers, and give a single exponential-time algorithm for computing the expected time. In our second contribution, we show that computing the expected time is #P -hard, and so polynomial algorithms are very unlikely to exist. Further, #P -hardness holds even for workflows with a very simple structure in which all transitions times are 1 or 0, and all probabilities are 1 or 0.5. Our third and final contribution is an experimental investigation of the runtime of our algorithm on a set of industrial benchmarks. Despite the negative theoretical results, the results are very encouraging. In particular, the expected time of every workflow in a popular benchmark suite with 642 workflow nets can be computed in milliseconds. Data or code related to this paper is available at: [24].},
  author = {Meyer, Philipp J. and Esparza, Javier and Offtermatt, Philip},
  booktitle = {TACAS (2)},
  crossref = {conf/tacas/2019-2},
  editor = {Vojnar, Tomás and Zhang, Lijun},
  keywords = {expectedterminationtime petrinets},
  note = {#conference},
  pages = {154-171},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Computing the Expected Execution Time of Probabilistic Workflow Nets.},
  volume = 11428,
  year = 2019
  }
  

  %0 Conference Paper
  %1 conf/tacas/MeyerEO19
  %A Meyer, Philipp J.
  %A Esparza, Javier
  %A Offtermatt, Philip
  %B TACAS (2)
  %D 2019
  %E Vojnar, Tomás
  %E Zhang, Lijun
  %I Springer
  %P 154-171
  %R 10.1007/978-3-030-17465-1_9
  %T Computing the Expected Execution Time of Probabilistic Workflow Nets.
  %U https://doi.org/10.1007/978-3-030-17465-1_9
  %V 11428
  %X Free-Choice Workflow Petri nets, also known as Workflow Graphs, are a popular model in Business Process Modeling. In this paper we introduce Timed Probabilistic Workflow Nets (TPWNs), and give them a Markov Decision Process (MDP) semantics. Since the time needed to execute two parallel tasks is the maximum of the times, and not their sum, the expected time cannot be directly computed using the theory of MDPs with rewards. In our first contribution, we overcome this obstacle with the help of “earliest-first” schedulers, and give a single exponential-time algorithm for computing the expected time. In our second contribution, we show that computing the expected time is #P -hard, and so polynomial algorithms are very unlikely to exist. Further, #P -hardness holds even for workflows with a very simple structure in which all transitions times are 1 or 0, and all probabilities are 1 or 0.5. Our third and final contribution is an experimental investigation of the runtime of our algorithm on a set of industrial benchmarks. Despite the negative theoretical results, the results are very encouraging. In particular, the expected time of every workflow in a popular benchmark suite with 642 workflow nets can be computed in milliseconds. Data or code related to this paper is available at: [24].
  %@ 978-3-030-17465-1
  

• 1.

  Raskin, M., Welzel, C.: Working with first-order proofs and provers. European Lisp Symposium (2019)
  automatedtheoremprovers firstorderlogic interactiveproofsystems
  URL: Link
  Slides: <a href="https://european-lisp-symposium.org/static/2019/raskin.pdf">Link</a><br>#talk

  URLBibTeXEndNote

  @conference{conference/els/2019/RW-ELS-2019,
  author = {Raskin, Michael and Welzel, Christoph},
  booktitle = {European Lisp Symposium},
  keywords = {automatedtheoremprovers firstorderlogic interactiveproofsystems},
  note = {Slides: Link
  #talk},
  title = {Working with first-order proofs and provers.},
  volume = {ELS-2019},
  year = 2019
  }
  

  %0 Generic
  %1 conference/els/2019/RW-ELS-2019
  %A Raskin, Michael
  %A Welzel, Christoph
  %B European Lisp Symposium
  %D 2019
  %T Working with first-order proofs and provers.
  %U https://european-lisp-symposium.org/2019/index.html
  %V ELS-2019
  

• 1.

  Raskin, M.: Population protocols with unreliable communication. CoRR. abs/1902.10041, (2019)
  broadcastprotocols faulttolerance populationprotocols
  Preprint: <a href="http://arxiv.org/abs/1902.10041">Link</a><br>#informal

  BibTeXEndNote

  @article{journals/corr/abs-1902-10041,
  author = {Raskin, Mikhail},
  journal = {CoRR},
  keywords = {broadcastprotocols faulttolerance populationprotocols},
  note = {Preprint: Link
  #informal},
  title = {Population protocols with unreliable communication.},
  volume = {abs/1902.10041},
  year = 2019
  }
  

  %0 Journal Article
  %1 journals/corr/abs-1902-10041
  %A Raskin, Mikhail
  %D 2019
  %J CoRR
  %T Population protocols with unreliable communication.
  %V abs/1902.10041
  

• 1.

  Hansen, K.A., Raskin, M.: A Stay-in-a-Set Game without a Stationary Equilibrium. Electronic Proceedings in Theoretical Computer Science. 305, 83–90 (2019)
  gametheory myown safetyconditions verification
  URL: Link
  #conference

  URLBibTeXEndNote

  @article{Hansen_2019,
  author = {Hansen, Kristoffer Arnsfelt and Raskin, Mikhail},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  keywords = {gametheory myown safetyconditions verification},
  month = {sep},
  note = {#conference},
  pages = {83--90},
  publisher = {Open Publishing Association},
  title = {A Stay-in-a-Set Game without a Stationary Equilibrium},
  volume = 305,
  year = 2019
  }
  

  %0 Journal Article
  %1 Hansen_2019
  %A Hansen, Kristoffer Arnsfelt
  %A Raskin, Mikhail
  %D 2019
  %I Open Publishing Association
  %J Electronic Proceedings in Theoretical Computer Science
  %P 83--90
  %R 10.4204/eptcs.305.6
  %T A Stay-in-a-Set Game without a Stationary Equilibrium
  %U https://doi.org/10.4204%2Feptcs.305.6
  %V 305
  

• 1.

  Blondin, M., Esparza, J., Jaax, S.: Expressive Power of Broadcast Consensus Protocols. In: Fokkink, W. and van Glabbeek, R. (eds.) 30th International Conference on Concurrency Theory (CONCUR 2019). pp. 31:1–31:16. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019)
  broadcast complexity protocols
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/1902.01668">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  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.

  @inproceedings{blondin2019expressive,
  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.},
  address = {Dagstuhl, Germany},
  author = {Blondin, Michael and Esparza, Javier and Jaax, Stefan},
  booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)},
  editor = {Fokkink, Wan and van Glabbeek, Rob},
  keywords = {broadcast complexity protocols},
  note = {Preprint: Link
  #conference},
  pages = {31:1--31:16},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {Expressive Power of Broadcast Consensus Protocols},
  volume = 140,
  year = 2019
  }
  

  %0 Conference Paper
  %1 blondin2019expressive
  %A Blondin, Michael
  %A Esparza, Javier
  %A Jaax, Stefan
  %B 30th International Conference on Concurrency Theory (CONCUR 2019)
  %C Dagstuhl, Germany
  %D 2019
  %E Fokkink, Wan
  %E van Glabbeek, Rob
  %I Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
  %P 31:1--31:16
  %R 10.4230/LIPIcs.CONCUR.2019.31
  %T Expressive Power of Broadcast Consensus Protocols
  %U https://drops.dagstuhl.de/opus/volltexte/2019/10933/
  %V 140
  %X 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.
  %@ 978-3-95977-121-4
  

• 1.

  Berkovits, I., Lazic, M., Losa, G., Padon, O., Shoham, S.: Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. In: Dillig, I. and Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. pp. 245–266. Springer (2019)
  distributedalgorithms myown parameterizedverification
  URL: Link
  #conference

  AbstractURLBibTeXEndNote

  Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code and in its correctness proof, e.g., a process can perform an action only if it has received an acknowledgment from at least half of its peers. Verification of threshold-based protocols is extremely challenging as it involves two kinds of reasoning: first-order reasoning about the unbounded state of the protocol, together with reasoning about sets and cardinalities. In this work, we develop a new methodology for decomposing the verification task of such protocols into two decidable logics: EPR and BAPA. Our key insight is that such protocols use thresholds in a restricted way as a means to obtain certain properties of “intersection” between sets. We define a language for expressing such properties, and present two translations: to EPR and BAPA. The EPR translation allows verifying the protocol while assuming these properties, and the BAPA translation allows verifying the correctness of the properties. We further develop an algorithm for automatically generating the properties needed for verifying a given protocol, facilitating fully automated deductive verification. Using this technique we have verified several challenging protocols, including Byzantine one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos.

  @inproceedings{DBLP:conf/cav/BerkovitsLLPS19,
  abstract = {Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code and in its correctness proof, e.g., a process can perform an action only if it has received an acknowledgment from at least half of its peers. Verification of threshold-based protocols is extremely challenging as it involves two kinds of reasoning: first-order reasoning about the unbounded state of the protocol, together with reasoning about sets and cardinalities. In this work, we develop a new methodology for decomposing the verification task of such protocols into two decidable logics: EPR and BAPA. Our key insight is that such protocols use thresholds in a restricted way as a means to obtain certain properties of “intersection” between sets. We define a language for expressing such properties, and present two translations: to EPR and BAPA. The EPR translation allows verifying the protocol while assuming these properties, and the BAPA translation allows verifying the correctness of the properties. We further develop an algorithm for automatically generating the properties needed for verifying a given protocol, facilitating fully automated deductive verification. Using this technique we have verified several challenging protocols, including Byzantine one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos.},
  author = {Berkovits, Idan and Lazic, Marijana and Losa, Giuliano and Padon, Oded and Shoham, Sharon},
  booktitle = {Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II},
  editor = {Dillig, Isil and Tasiran, Serdar},
  keywords = {distributedalgorithms myown parameterizedverification},
  note = {#conference},
  pages = {245--266},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics},
  volume = 11562,
  year = 2019
  }
  

  %0 Conference Paper
  %1 DBLP:conf/cav/BerkovitsLLPS19
  %A Berkovits, Idan
  %A Lazic, Marijana
  %A Losa, Giuliano
  %A Padon, Oded
  %A Shoham, Sharon
  %B Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II
  %D 2019
  %E Dillig, Isil
  %E Tasiran, Serdar
  %I Springer
  %P 245--266
  %R 10.1007/978-3-030-25543-5_15
  %T Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
  %U https://doi.org/10.1007/978-3-030-25543-5_15
  %V 11562
  %X Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code and in its correctness proof, e.g., a process can perform an action only if it has received an acknowledgment from at least half of its peers. Verification of threshold-based protocols is extremely challenging as it involves two kinds of reasoning: first-order reasoning about the unbounded state of the protocol, together with reasoning about sets and cardinalities. In this work, we develop a new methodology for decomposing the verification task of such protocols into two decidable logics: EPR and BAPA. Our key insight is that such protocols use thresholds in a restricted way as a means to obtain certain properties of “intersection” between sets. We define a language for expressing such properties, and present two translations: to EPR and BAPA. The EPR translation allows verifying the protocol while assuming these properties, and the BAPA translation allows verifying the correctness of the properties. We further develop an algorithm for automatically generating the properties needed for verifying a given protocol, facilitating fully automated deductive verification. Using this technique we have verified several challenging protocols, including Byzantine one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos.
  

• 1.

  Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In: Fokkink, W. and van Glabbeek, R. (eds.) CONCUR. pp. 33:1–33:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
  distributedalgorithms myown parametrizedverification randomizedconsensus
  URL: Link
  Preprint: <a href="https://hal.inria.fr/hal-01925533/">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round r-1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or's and Bracha's seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.

  @inproceedings{conf/concur/BertrandKLW19,
  abstract = {Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round r-1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or's and Bracha's seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.},
  author = {Bertrand, Nathalie and Konnov, Igor and Lazic, Marijana and Widder, Josef},
  booktitle = {CONCUR},
  crossref = {conf/concur/2019},
  editor = {Fokkink, Wan and van Glabbeek, Rob},
  keywords = {distributedalgorithms myown parametrizedverification randomizedconsensus},
  note = {Preprint: Link
  #conference},
  pages = {33:1-33:15},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  series = {LIPIcs},
  title = {Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries.},
  volume = 140,
  year = 2019
  }
  

  %0 Conference Paper
  %1 conf/concur/BertrandKLW19
  %A Bertrand, Nathalie
  %A Konnov, Igor
  %A Lazic, Marijana
  %A Widder, Josef
  %B CONCUR
  %D 2019
  %E Fokkink, Wan
  %E van Glabbeek, Rob
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %P 33:1-33:15
  %T Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries.
  %U https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10935
  %V 140
  %X Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round r-1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or's and Bracha's seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.
  %@ 978-3-95977-121-4
  

• 1.

  Goubault, Éric, Lazic, M., Ledent, J., Rajsbaum, S.: Wait-Free Solvability of Equality Negation Tasks. In: Suomela, J. (ed.) DISC. pp. 21:1–21:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
  myown
  URL: Link
  #conference

  AbstractURLBibTeXEndNote

  We introduce a family of tasks for n processes, as a generalization of the two process equality negation task of Lo and Hadzilacos (SICOMP 2000). Each process starts the computation with a private input value taken from a finite set of possible inputs. After communicating with the other processes using immediate snapshots, the process must decide on a binary output value, 0 or 1. The specification of the task is the following: in an execution, if the set of input values is large enough, the processes should agree on the same output; if the set of inputs is small enough, the processes should disagree; and in-between these two cases, any output is allowed. Formally, this specification depends on two threshold parameters k and l, with k

  @inproceedings{conf/wdag/GoubaultLLR19,
  abstract = {We introduce a family of tasks for n processes, as a generalization of the two process equality negation task of Lo and Hadzilacos (SICOMP 2000). Each process starts the computation with a private input value taken from a finite set of possible inputs. After communicating with the other processes using immediate snapshots, the process must decide on a binary output value, 0 or 1. The specification of the task is the following: in an execution, if the set of input values is large enough, the processes should agree on the same output; if the set of inputs is small enough, the processes should disagree; and in-between these two cases, any output is allowed. Formally, this specification depends on two threshold parameters k and l, with k author = {Goubault, Éric and Lazic, Marijana and Ledent, Jérémy and Rajsbaum, Sergio},
  booktitle = {DISC},
  crossref = {conf/wdag/2019},
  editor = {Suomela, Jukka},
  keywords = {myown},
  note = {#conference},
  pages = {21:1-21:16},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  series = {LIPIcs},
  title = {Wait-Free Solvability of Equality Negation Tasks.},
  volume = 146,
  year = 2019
  }
  

  %0 Conference Paper
  %1 conf/wdag/GoubaultLLR19
  %A Goubault, Éric
  %A Lazic, Marijana
  %A Ledent, Jérémy
  %A Rajsbaum, Sergio
  %B DISC
  %D 2019
  %E Suomela, Jukka
  %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  %P 21:1-21:16
  %T Wait-Free Solvability of Equality Negation Tasks.
  %U https://drops.dagstuhl.de/opus/volltexte/2019/11328/
  %V 146
  %X We introduce a family of tasks for n processes, as a generalization of the two process equality negation task of Lo and Hadzilacos (SICOMP 2000). Each process starts the computation with a private input value taken from a finite set of possible inputs. After communicating with the other processes using immediate snapshots, the process must decide on a binary output value, 0 or 1. The specification of the task is the following: in an execution, if the set of input values is large enough, the processes should agree on the same output; if the set of inputs is small enough, the processes should disagree; and in-between these two cases, any output is allowed. Formally, this specification depends on two threshold parameters k and l, with k%@ 978-3-95977-126-9
  

• 1.

  Raskin, M., Simkin, M.: Perfectly Secure Oblivious RAM with Sublinear Bandwidth Overhead. In: Galbraith, S.D. and Moriai, S. (eds.) Lecture Notes in Computer Science. pp. 537–563. Springer International Publishing (2019)
  cryptography myown protocols security
  URL: Link
  Preprint: <a href="https://eprint.iacr.org/2018/268">Link</a><br>#journal

  URLBibTeXEndNote

  @incollection{Raskin_2019,
  author = {Raskin, Michael and Simkin, Mark},
  booktitle = {Lecture Notes in Computer Science},
  editor = {Galbraith, Steven D. and Moriai, Shiho},
  keywords = {cryptography myown protocols security},
  note = {Preprint: Link
  #journal},
  pages = {537--563},
  publisher = {Springer International Publishing},
  series = {Lecture Notes in Computer Science},
  title = {Perfectly Secure Oblivious RAM with Sublinear Bandwidth Overhead},
  type = {Publication},
  volume = 11922,
  year = 2019
  }
  

  %0 Book Section
  %1 Raskin_2019
  %A Raskin, Michael
  %A Simkin, Mark
  %B Lecture Notes in Computer Science
  %D 2019
  %E Galbraith, Steven D.
  %E Moriai, Shiho
  %I Springer International Publishing
  %P 537--563
  %R 10.1007/978-3-030-34621-8_19
  %T Perfectly Secure Oblivious RAM with Sublinear Bandwidth Overhead
  %U https://doi.org/10.1007/978-3-030-34621-8_19
  %V 11922
  

• 1.

  Goubault, Éric, Lazic, M., Ledent, J., Rajsbaum, S.: A Dynamic Epistemic Logic Analysis of the Equality Negation Task. In: Barbosa, L.S. and Baltag, A. (eds.) DaLí. pp. 53–70. Springer (2019)
  logic myown
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/1909.03263">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  In this paper we study the solvability of the equality negation task in a simple wait-free model where processes communicate by reading and writing shared variables or exchanging messages. In this task, two processes start with a private input value in the set 0,1,2, and after communicating, each one must decide a binary output value, so that the outputs of the processes are the same if and only if the input values of the processes are different. This task is already known to be unsolvable; our goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by Goubault, Ledent and Rajsbaum in GandALF 2018. We show that in fact, there is no epistemic logic formula that explains why the task is unsolvable. We fix this issue by extending the language of our DEL framework, which allows us to construct such a formula, and discuss its utility.

  @inproceedings{conf/tap/GoubaultLLR19,
  abstract = {In this paper we study the solvability of the equality negation task in a simple wait-free model where processes communicate by reading and writing shared variables or exchanging messages. In this task, two processes start with a private input value in the set 0,1,2, and after communicating, each one must decide a binary output value, so that the outputs of the processes are the same if and only if the input values of the processes are different. This task is already known to be unsolvable; our goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by Goubault, Ledent and Rajsbaum in GandALF 2018. We show that in fact, there is no epistemic logic formula that explains why the task is unsolvable. We fix this issue by extending the language of our DEL framework, which allows us to construct such a formula, and discuss its utility.},
  author = {Goubault, Éric and Lazic, Marijana and Ledent, Jérémy and Rajsbaum, Sergio},
  booktitle = {DaLí},
  crossref = {conf/dali/2019},
  editor = {Barbosa, Luís Soares and Baltag, Alexandru},
  keywords = {logic myown},
  note = {Preprint: Link
  #conference},
  pages = {53-70},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {A Dynamic Epistemic Logic Analysis of the Equality Negation Task.},
  volume = 12005,
  year = 2019
  }
  

  %0 Conference Paper
  %1 conf/tap/GoubaultLLR19
  %A Goubault, Éric
  %A Lazic, Marijana
  %A Ledent, Jérémy
  %A Rajsbaum, Sergio
  %B DaLí
  %D 2019
  %E Barbosa, Luís Soares
  %E Baltag, Alexandru
  %I Springer
  %P 53-70
  %R 10.1007/978-3-030-38808-9_4
  %T A Dynamic Epistemic Logic Analysis of the Equality Negation Task.
  %U https://doi.org/10.1007/978-3-030-38808-9_4
  %V 12005
  %X In this paper we study the solvability of the equality negation task in a simple wait-free model where processes communicate by reading and writing shared variables or exchanging messages. In this task, two processes start with a private input value in the set 0,1,2, and after communicating, each one must decide a binary output value, so that the outputs of the processes are the same if and only if the input values of the processes are different. This task is already known to be unsolvable; our goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by Goubault, Ledent and Rajsbaum in GandALF 2018. We show that in fact, there is no epistemic logic formula that explains why the task is unsolvable. We fix this issue by extending the language of our DEL framework, which allows us to construct such a formula, and discuss its utility.
  %@ 978-3-030-38808-9
  

• 1.

  Blondin, M., Haase, C., Mazowiecki, F., Raskin, M.: Affine Extensions of Integer Vector Addition Systems with States. (2019)
  complexity myown reachability
  Preprint: <a href="https://arxiv.org/abs/1909.12386">Link</a> (25 pages, 7 figures)<br>#informal

  AbstractBibTeXEndNote

  We study the reachability problem for affine \($\mathbbZ$\)-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine \($\mathbbZ$\)-VASS with the finite-monoid property (afmp-\($\mathbbZ$\)-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-\($\mathbbZ$\)-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-\($\mathbbZ$\)-VASS reduces to reachability in a \($\mathbbZ$\)-VASS whose control-states grow linearly in the size of the matrix monoid. Our construction shows that reachability relations of afmp-\($\mathbbZ$\)-VASS are semilinear, and in particular enables us to show that reachability in \($\mathbbZ$\)-VASS with transfers and \($\mathbbZ$\)-VASS with copies is PSPACE-complete. We then focus on the reachability problem for affine \($\mathbbZ$\)-VASS with monogenic monoids: (possibly infinite) matrix monoids generated by a single matrix. We show that, in a particular case, the reachability problem is decidable for this class, disproving a conjecture about affine \($\mathbbZ$\)-VASS with infinite matrix monoids we raised in a preliminary version of this paper. We complement this result by presenting an affine \($\mathbbZ$\)-VASS with monogenic matrix monoid and undecidable reachability relation.

  @article{blondin2019affine,
  abstract = {We study the reachability problem for affine \($\mathbbZ$\)-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine \($\mathbbZ$\)-VASS with the finite-monoid property (afmp-\($\mathbbZ$\)-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-\($\mathbbZ$\)-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-\($\mathbbZ$\)-VASS reduces to reachability in a \($\mathbbZ$\)-VASS whose control-states grow linearly in the size of the matrix monoid. Our construction shows that reachability relations of afmp-\($\mathbbZ$\)-VASS are semilinear, and in particular enables us to show that reachability in \($\mathbbZ$\)-VASS with transfers and \($\mathbbZ$\)-VASS with copies is PSPACE-complete. We then focus on the reachability problem for affine \($\mathbbZ$\)-VASS with monogenic monoids: (possibly infinite) matrix monoids generated by a single matrix. We show that, in a particular case, the reachability problem is decidable for this class, disproving a conjecture about affine \($\mathbbZ$\)-VASS with infinite matrix monoids we raised in a preliminary version of this paper. We complement this result by presenting an affine \($\mathbbZ$\)-VASS with monogenic matrix monoid and undecidable reachability relation.},
  author = {Blondin, Michael and Haase, Christoph and Mazowiecki, Filip and Raskin, Mikhail},
  keywords = {complexity myown reachability},
  note = {Preprint: Link (25 pages, 7 figures)
  #informal},
  title = {Affine Extensions of Integer Vector Addition Systems with States},
  year = 2019
  }
  

  %0 Journal Article
  %1 blondin2019affine
  %A Blondin, Michael
  %A Haase, Christoph
  %A Mazowiecki, Filip
  %A Raskin, Mikhail
  %D 2019
  %T Affine Extensions of Integer Vector Addition Systems with States
  %X We study the reachability problem for affine \($\mathbbZ$\)-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine \($\mathbbZ$\)-VASS with the finite-monoid property (afmp-\($\mathbbZ$\)-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-\($\mathbbZ$\)-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-\($\mathbbZ$\)-VASS reduces to reachability in a \($\mathbbZ$\)-VASS whose control-states grow linearly in the size of the matrix monoid. Our construction shows that reachability relations of afmp-\($\mathbbZ$\)-VASS are semilinear, and in particular enables us to show that reachability in \($\mathbbZ$\)-VASS with transfers and \($\mathbbZ$\)-VASS with copies is PSPACE-complete. We then focus on the reachability problem for affine \($\mathbbZ$\)-VASS with monogenic monoids: (possibly infinite) matrix monoids generated by a single matrix. We show that, in a particular case, the reachability problem is decidable for this class, disproving a conjecture about affine \($\mathbbZ$\)-VASS with infinite matrix monoids we raised in a preliminary version of this paper. We complement this result by presenting an affine \($\mathbbZ$\)-VASS with monogenic matrix monoid and undecidable reachability relation.
  

2018

• 1.

  Blondin, M., Esparza, J., Kucera, A.: Automatic Analysis of Expected Termination Time for Population Protocols. In: Schewe, S. and Zhang, L. (eds.) 29th International Conference on Concurrency Theory (CONCUR 2018). pp. 33:1–33:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)
  ExpectedTerminationTime PerformanceAnalysis PopulationProtocols
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/1807.00331">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  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.

  @inproceedings{conf/concur/BlondinEK18,
  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.},
  author = {Blondin, Michael and Esparza, Javier and Kucera, Antonín},
  booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
  crossref = {conf/concur/2018},
  editor = {Schewe, Sven and Zhang, Lijun},
  keywords = {ExpectedTerminationTime PerformanceAnalysis PopulationProtocols},
  note = {Preprint: Link
  #conference},
  pages = {33:1-33:16},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {Automatic Analysis of Expected Termination Time for Population Protocols.},
  volume = 118,
  year = 2018
  }
  

  %0 Conference Paper
  %1 conf/concur/BlondinEK18
  %A Blondin, Michael
  %A Esparza, Javier
  %A Kucera, Antonín
  %B 29th International Conference on Concurrency Theory (CONCUR 2018)
  %D 2018
  %E Schewe, Sven
  %E Zhang, Lijun
  %I Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
  %P 33:1-33:16
  %R 10.4230/LIPIcs.CONCUR.2018.33
  %T Automatic Analysis of Expected Termination Time for Population Protocols.
  %U https://drops.dagstuhl.de/opus/volltexte/2018/9571/
  %V 118
  %X 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.
  %@ 978-3-95977-087-3
  

• 1.

  Esparza, J., Ganty, P., Majumdar, R., Weil-Kennedy, C.: Verification of Immediate Observation Population Protocols. In: Schewe, S. and Zhang, L. (eds.) 29th International Conference on Concurrency Theory (CONCUR 2018). pp. 31:1–31:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)
  ImmediateObservation ParametrizedVerification PopulationProtocols
  URL: Link
  Preprint: <a href="https://arxiv.org/abs/1807.06071">Link</a><br>#conference

  AbstractURLBibTeXEndNote

  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.

  @inproceedings{conf/concur/EsparzaGMW18,
  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.},
  author = {Esparza, Javier and Ganty, Pierre and Majumdar, Rupak and Weil-Kennedy, Chana},
  booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
  crossref = {conf/concur/2018},
  editor = {Schewe, Sven and Zhang, Lijun},
  keywords = {ImmediateObservation ParametrizedVerification PopulationProtocols},
  note = {Preprint: Link
  #conference},
  pages = {31:1-31:16},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  title = {Verification of Immediate Observation Population Protocols.},
  volume = 118,
  year = 2018
  }
  

  %0 Conference Paper
  %1 conf/concur/EsparzaGMW18
  %A Esparza, Javier
  %A Ganty, Pierre
  %A Majumdar, Rupak
  %A Weil-Kennedy, Chana
  %B 29th International Conference on Concurrency Theory (CONCUR 2018)
  %D 2018
  %E Schewe, Sven
  %E Zhang, Lijun
  %I Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
  %P 31:1-31:16
  %R 10.4230/LIPIcs.CONCUR.2018.31
  %T Verification of Immediate Observation Population Protocols.
  %U https://drops.dagstuhl.de/opus/volltexte/2018/9569/
  %V 118
  %X 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.
  %@ 978-3-95977-087-3