Martin Helfrich

I was a doctoral candidate advised by Prof. Javier Esparza in the Chair for Foundations of Software Reliability and Theoretical Computer Science at the Technical University of Munich. I specialized in the verification, synthesis, complexity, and efficient analysis of parameterized systems. My research focused on systems where complexity arises from the interaction of many simple agents, particularly in the context of population protocols and chemical reaction networks.

I was part of the research training group ConVeY as well as the ERC-supported project PaVeS.

After four years, I completed my doctoral studies in 2023. Starting 2024, I am working as specialist for system integration at BWM in Munich.

Publications

Journals (peer-reviewed)

Fast and succinct population protocols for Presburger arithmetic
Philipp Czerner, Roland Guttenberg, Martin Helfrich, Javier Esparza
Journal of Computer and System Sciences
@article{czernerFastAndSuccinctPPjournal, title = {Fast and succinct population protocols for Presburger arithmetic}, journal = {Journal of Computer and System Sciences}, volume = {140}, pages = {103481}, year = {2024}, issn = {0022-0000}, doi = {https://doi.org/10.1016/j.jcss.2023.103481}, url = {https://www.sciencedirect.com/science/article/pii/S0022000023000867}, author = {Philipp Czerner and Roland Guttenberg and Martin Helfrich and Javier Esparza}, keywords = {Population protocols, Fast, Succinct, Population computers}, abstract = {In their 2006 seminal paper in Distributed Computing, Angluin et al. present a construction that, given any Presburger predicate, outputs a leaderless population protocol that decides the predicate. The protocol for a predicate of size m runs in O(m n^2 log n) expected number of interactions, which is almost optimal in n, the number of interacting agents. However, the number of states is exponential in m. Blondin et al. presented at STACS 2020 another construction that produces protocols with a polynomial number of states, but exponential expected number of interactions. We present a construction that produces protocols with O(m) states that run in expected O(m^7 n^2) interactions, optimal in n, for all inputs of size Ω(m). For this, we introduce population computers, a generalization of population protocols, and show that our computers for Presburger predicates can be translated into fast and succinct population protocols.} }

Conferences (peer-reviewed)

Abstraction-Based Segmental Simulation of Chemical Reaction Networks
Martin Helfrich, Milan Ceska, Jan Kretinsky, Stefan Marticek
CMSB, 2022
@InProceedings{helfrichSegmental, author="Helfrich, Martin and {\v{C}}e{\v{s}}ka, Milan and K{\v{r}}et{\'i}nsk{\'y}, Jan and Marti{\v{c}}ek, {\v{S}}tefan", editor="Petre, Ion and P{\u{a}}un, Andrei", title="Abstraction-Based Segmental Simulation of Chemical Reaction Networks", booktitle="Computational Methods in Systems Biology", year="2022", publisher="Springer International Publishing", address="Cham", pages="41--60", 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.", isbn="978-3-031-15034-0", doi="10.1007/978-3-031-15034-0_3" }
Fast and Succinct Population Protocols for Presburger Arithmetic
Philipp Czerner, Roland Guttenberg, Martin Helfrich, Javier Esparza
SAND, 2022
Best Paper Award
@InProceedings{czernerFastAndSuccinctPP, author = {Czerner, Philipp and Guttenberg, Roland and Helfrich, Martin and Esparza, Javier}, title = {{Fast and Succinct Population Protocols for Presburger Arithmetic}}, booktitle = {1st Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2022)}, pages = {11:1--11:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-224-2}, ISSN = {1868-8969}, year = {2022}, volume = {221}, editor = {Aspnes, James and Michail, Othon}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, doi = {10.4230/LIPIcs.SAND.2022.11}, annote = {Keywords: population protocols, fast, succinct, population computers} }
Decision Power of Weak Asynchronous Models of Distributed Computing
Philipp Czerner, Roland Guttenberg, Martin Helfrich, Javier Esparza
PODC, 2021
@inproceedings{czernerDecisionPower, author = {Czerner, Philipp and Guttenberg, Roland and Helfrich, Martin and Esparza, Javier}, title = {Decision Power of Weak Asynchronous Models of Distributed Computing}, year = {2021}, isbn = {9781450385480}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3465084.3467918}, doi = {10.1145/3465084.3467918}, abstract = {Esparza and Reiter have recently conducted a systematic comparative study of models of distributed computing consisting of a network of identical finite-state automata that cooperate to decide if the underlying graph of the network satisfies a given property. The study classifies models according to four criteria, and shows that twenty-four initially possible combinations collapse into seven equivalence classes with respect to their decision power, i.e. the properties that the automata of each class can decide. However, Esparza and Reiter only show (proper) inclusions between the classes, and so do not characterise their decision power. In this paper we do so for labelling properties, i.e. properties that depend only on the labels of the nodes, but not on the structure of the graph. In particular, majority (whether more nodes carry label a than b) is a labelling property. Our results show that only one of the seven equivalence classes identified by Esparza and Reiter can decide majority for arbitrary networks. We then study the expressive power of the classes on bounded-degree networks, and show that three classes can. In particular, we present an algorithm for majority that works for all bounded-degree networks under adversarial schedulers, i.e. even if the scheduler must only satisfy that every node makes a move infinitely often, and prove that no such algorithm can work for arbitrary networks.}, booktitle = {Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing}, pages = {115–125}, numpages = {11}, keywords = {communication graphs, graph automata, decision power, labelling properties, distributed computing, weak asynchronous models}, location = {Virtual Event, Italy}, series = {PODC'21} }
Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs
Javier Esparza, Martin Helfrich, Stefan Jaax, Philipp J. Meyer
ATVA, 2020
@InProceedings{esparzaExplainingCorrectness, author="Esparza, Javier and Helfrich, Martin and Jaax, Stefan and Meyer, Philipp J.", editor="Hung, Dang Van and Sokolsky, Oleg", title="Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs", booktitle="Automated Technology for Verification and Analysis", year="2020", publisher="Springer International Publishing", address="Cham", pages="550--556", abstract="We present a new version of Peregrine, the tool for the analysis and parameterized verification of population protocols introduced in [Blondin et al., CAV'2018]. Population protocols are a model of computation, intensely studied by the distributed computing community, in which mobile anonymous agents interact stochastically to perform a task. Peregrine 2.0 features a novel verification engine based on the construction of stage graphs. Stage graphs are proof certificates, introduced in [Blondin et al., CAV'2020], that are typically succinct and can be independently checked. Moreover, unlike the techniques of Peregrine 1.0, the stage graph methodology can verify protocols whose executions never terminate, a class including recent fast majority protocols. Peregrine 2.0 also features a novel proof visualization component that allows the user to interactively explore the stage graph generated for a given protocol.", doi="10.1007/978-3-030-59152-6_32", isbn="978-3-030-59152-6" }
Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
Michael Blondin, Javier Esparza, Martin Helfrich, Antonín Kučera, Philipp Meyer
CAV, 2020
-teaser -talk
@InProceedings{blondinCheckingLiveness, author="Blondin, Michael and Esparza, Javier and Helfrich, Martin and Ku{\v{c}}era, Anton{\'i}n and Meyer, Philipp J.", editor="Lahiri, Shuvendu K. and Wang, Chao", title="Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling", booktitle="Computer Aided Verification", year="2020", publisher="Springer International Publishing", address="Cham", pages="372--397", 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.", doi="10.1007/978-3-030-53291-8_20", isbn="978-3-030-53291-8" }
Automata Tutor v3
Loris D'Antoni, Martin Helfrich, Jan Kretinsky, Emanuel Ramneantu, Maximilian Weininger
CAV, 2020
-teaser -talk
@InProceedings{ATv3, author="D'Antoni, Loris and Helfrich, Martin and Kretinsky, Jan and Ramneantu, Emanuel and Weininger, Maximilian", editor="Lahiri, Shuvendu K. and Wang, Chao", title="Automata Tutor v3", booktitle="Computer Aided Verification", year="2020", publisher="Springer International Publishing", address="Cham", pages="3--14", 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.", isbn="978-3-030-53291-8", doi="10.1007/978-3-030-53291-8_1" }
Succinct Population Protocols for Presburger Arithmetic
Michael Blondin, Javier Esparza, Blaise Genest, Martin Helfrich and Stefan Jaax
STACS, 2020
@InProceedings{blondinSuccinctPP, author = {Michael Blondin and Javier Esparza and Blaise Genest and Martin Helfrich and Stefan Jaax}, title = {{Succinct Population Protocols for Presburger Arithmetic}}, booktitle = {37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)}, pages = {40:1--40:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-140-5}, ISSN = {1868-8969}, year = {2020}, volume = {154}, editor = {Christophe Paul and Markus Bl{\"a}ser}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/opus/volltexte/2020/11901}, URN = {urn:nbn:de:0030-drops-119018}, doi = {10.4230/LIPIcs.STACS.2020.40}, annote = {Keywords: Population protocols, Presburger arithmetic, state complexity} }

Theses

Efficient Analysis of Population Protocols and Chemical Reaction Networks
PhD thesis, Technical University Munich, 2023
Automatic Verification of non-silent Population Protocols
Master Sc. thesis, Technical University Munich, 2019
Kontextfreie Grammatiken in AutomataTutor
Bachelor Sc. thesis, Technical University Munich, 2017

Tools

During my time at university I worked on the following tools:

SAQuaiA

SAQuaiA is a tool for Simluation & Abstraction-based Quantitative Analysis of Chemical Reaction Networks (CRNs). The GUI allows to perform simulations and simulation-based transient analysis and the visulazation of their results.

SAQuaiA implements multiple simulation approaches like the slow but accurate Stochastic Simulation Algorithm (SSA) as well as faster approximate simulation techniques. They include the novel abstraction-based segmental simulation approach that uses memoization to reuse short trajectories, called segments, of previous simulations in order to generate new simulations.

Peregrine

Peregrine is a tool for the analysis and parameterized verification of population protocols. With its graphical user interface, it allows the user to specify population protocols that then can be simulated both manually and automatically. Peregrine can also find executions of faulty protocols and it can automatically verify if a given protocol computes a specified formula for all of the infinitely many initial configurations.

Peregrine 2.0 features a novel verification engine based on the construction of stage graphs. Stage graphs are proof certificates that are typically succinct and can be independently checked. By studing the interactive stage graph visualization, users can more easily understand why a protocol is correct.

Automata Tutor v3

Automata Tutor is an online tool that uses techniques from program synthesis and decision procedures to improve the quality and effectiveness of teaching in courses on formal languages and theory of computation, two of the fundamental topics in computer science education.

Teaching

During my time at university I was involved in teaching the following courses and subjects:

SS 2022 - Technical University Munich - Teaching Assistant
Introduction to Formal Languages and Theory of Computation
WS 2021/22 - Technical University Munich - Tutor
Algorithms for Programming Contests
SS 2021 - Technical University Munich - Teaching Assistant
Introduction to Formal Languages and Theory of Computation
Teaching Award
WS 2020/21 - Technical University Munich - Tutor
Algorithms for Programming Contests
SS 2020 - Technical University Munich - Tutor
Introduction to Formal Languages and Theory of Computation
SS 2017 - Technical University Munich - Tutor
Introduction to Formal Languages and Theory of Computation