I was in academia from 2015 to 2022, doing research in automata theory, a subarea of theoretical computer science.
I have coauthored 8 research papers, 6 of which were peer-reviewed, published, and presented at reputable conferences.
In 2023, I have obtained a PhD (Dr. rer. nat.) from TU Braunschweig.
You can find information on my publications below.
You may also want to check my list of publications at the dblp computer science bibliography: Sebastian Muskalla @ DBLP.
PhD thesis: Certificates for automata in a hostile environment
S. Muskalla
Certificates for automata in a hostile environment
PhD thesis, TU Braunschweig, 2023
I have obtained a PhD (Dr. rer. nat.) at the Carl-Friedrich-Gauß-Fakultät of the Technische Universität Braunschweig in 2023.
In August 2022, I have submitted my dissertation Certificates for automata in a hostile environment in theoretical computer science that I wrote under the supervision of Roland Meyer.
You can find the approved and published version of the thesis below.
The thesis contains and extends 5 of my peer-reviewed publications that you can find more details on below:
In May 2023, I defended the dissertation, graduating with highest honors (summa cum laude).
You can find the slides for the talk that was part of the defense below.
L. Holík, R. Meyer, and S. Muskalla
Summaries for context-free games
In: FSTTCS 2016, volume 65 of LIPIcs, pages 41:1–41:16
The paper Summaries for context-free games authored by Lukáš Holík, Roland Meyer, and me, was published in the proceedings of FSTTCS 2016, the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science.
The paper is concerned with two-player board games with perfect information on a game arena induced by a context-free grammar.
Plays of the game are derivation processes of the grammar, and the winning condition is membership of the derived word in a regular target language.
We provide an algorithm that works by finding the least solution to a system of equations using fixed-point iteration.
Both the winner of the game and the associated winning strategy can be read off from this least-solution.
Our algorithm provably has the optimal asymptotic time complexity.
I have presented our paper at FSSTCS 2016 in Chennai, India.
You can find the slides for that presentation below.
A full version of the paper that includes all proofs and additional material has been made available on arXiv.
You can find both the peer-reviewed, officially published conference version and the full version below.
In conjunction with our submission, I have programmed a prototype implementation of the algorithm.
The tool is called RIGG (regular inclusion grammar games).
The code is available on GitHub: RIGG @ GitHub.
M. Hague, R. Meyer, and S. Muskalla
Domains for higher-order games
In: MFCS 2017, volume 83 of LIPIcs, pages 59:1–59:15
The paper Domains for higher-order games authored by Matthew Hague, Roland Meyer, and me, was published in the proceedings of MFCS 2017, the 42nd International Symposium on Mathematical Foundations of Computer Science.
The paper extends our earlier work Summaries for context-free games.
We consider board games played on arenas generated by higher-order recursion schemes, a generalization of context-free grammars.
We provide an algorithm solving such games with the optimal asymptotic time complexity that is based on solving a system of equations.
In order to establish the soundness of the algorithm, we also present a framework for such systems of equations associated to higher-order recursion schemes.
The framework makes it possible to transfer the properties of the solution of the system with respect to one domain to a solution with respect to another domain.
My coauthor Matthew Hague has presented our paper at MFCS 2017 in Aalborg, Denmark.
You can find a link to his slides for that presentation below.
A full version of the paper that includes all proofs has been made available on arXiv.
You can find both the peer-reviewed, officially published conference version and the full version below.
Paper: On the upward/downward closure of Petri nets
M. F. Atig, R. Meyer, S. Muskalla and P. Saivasan
On the upward/downward closure of Petri nets
In: MFCS 2017, volume 83 of LIPIcs, pages 49:1–49:14
The paper On the upward/downward closure of Petri nets authored by Mohamed Faouzi Atig, Roland Meyer, Prakash Saivasan, and me, was published in the proceedings of FSTTCS 2016, the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science.
The paper is concerned with computing the closures of Petri net coverability languages with respect to the subword order.
We provide procedures that compute finite automata representing the closures with the optimal number of states.
We do this in the case of the upward and downward closures of both general Petri nets and restricted BPP nets.
We also consider the problem of checking whether the language of a Petri net is downward/upward closed.
To show decidability, we prove that regular containment is decidable.
Many of our results can be seen as extensions of famous results on Petri nets, e.g. by Rackoff, Lipton, and Esparza.
I have presented our paper at MFCS 2017 in Aalborg, Denmark.
You can find the slides for that presentation below.
A full version of the paper that includes all proofs has been made available on arXiv.
You can find both the peer-reviewed, officially published conference version and the full version below.
Paper: Regular separability of well-structured transition systems
W. Czerwiński, S. Lasota, R. Meyer, S. Muskalla, K. N. Kumar, and P. Saivasan
Regular separability of well-structured transition systems
In: CONCUR 2018, volume 118 of LIPIcs, pages 35:1–35:18
The paper Regular separability of well-structured transition systems authored by Wojciech Czerwiński, Sławomir Lasota, Roland Meyer, K Narayan Kumar, Prakash Saivasan, and me, was published in the proceedings of CONCUR 2018, the 29th International Conference on Concurrency Theory.
The paper establishes that under mild preconditions, any two disjoint languages of well-structured transition systems (WSTSes) are regularly separable.
Being regularly separable means that there is a regular separator, a regular language that contains one of the languages while being disjoint from the other.
As a consequence of our result, no non-regular WSTS language can have a complement that also is a WSTS language, and the WSTS languages have no subclass beyond the regular languages that is closed under complementation.
We make our construction of the automaton representing the regular separator explicit in the case of Petri net coverability languages, one instance of WSTS languages.
Additionally, we provide a collection of results on the relation among various subclasses of the class of WSTS languages, widening the applicability of our result on regular separability.
I have presented our paper at CONCUR 2018 in Beijing, China.
You can find the slides for that presentation below.
I have presented our paper at HIGHLIGHTS 2018 in Berlin.
You can find the slides and the poster for that presentation below.
A full version of the paper that includes all proofs has been made available on arXiv.
You can find both the peer-reviewed, officially published conference version and the full version below.
Paper: Bounded context switching for valence systems
R. Meyer, S. Muskalla, and G. Zetzsche
Bounded context switching for valence systems
In: CONCUR 2018, volume 118 of LIPIcs, pages 12:1–12:18
The paper Bounded context switching for valence systems authored by Roland Meyer, Georg Zetzsche, and me, was published in the proceedings of CONCUR 2018, the 29th International Conference on Concurrency Theory.
The paper establishes that reachability in valence systems over graph monoids under a bounded-context-switching restriction is an NP-complete problem.
Valence systems over graph monoids are an algebraic automata model that generalizes well-known models like pushdown automata and vector addition systems, or, equivalently, Petri nets.
Bounded context switching (BCS) means that the component of a concurrent system that is currently active may only change as often as specified by a given constant.
We provide a definition of BCS on the level of the graph monoid that generalizes the existing notion of BCS for multi-pushdown systems in a natural way.
We then prove NP-completeness by providing a non-deterministic algorithm solving reachability in polynomial time and a matching lower-bound.
I have presented our paper at CONCUR 2018 in Beijing, China.
You can find the slides for that presentation below.
A full version of the paper that includes all proofs has been made available on arXiv.
You can find both the peer-reviewed, officially published conference version and the full version below.
Paper: Parity to safety in polynomial time for pushdown and collapsible pushdown systems
M. Hague, R. Meyer, S. Muskalla, and M. Zimmermann
Parity to safety in polynomial time for pushdown and collapsible pushdown systems
In: MFCS 2018, volume 117 of LIPIcs, pages 57:1–57:15
The paper Parity to safety in polynomial time for pushdown and collapsible pushdown systems authored by Matthew Hague, Roland Meyer, Martin Zimmermann, and me, was published in the proceedings of MFCS 2018, the 43rd International Symposium on Mathematical Foundations of Computer Science.
The paper provides a polynomial-time reduction from parity games played on game arenas defined by (collapsible) higher-order pushdown systems to safety games on these arenas.
For finite game arenas, the existence of such a reduction is an open question.
While for game arenas defined by pushdown systems and their higher-order extensions, the existence of such a reduction has been proven in a non-constructive manner, a direct reduction was missing.
We provide this direct reduction.
The reduction (and its soundness) rely on extending and combining techniques for games on infinite game arenas like counter reductions and order reductions.
My coauthor Matthew Hague has presented our paper at MFCS 2018 in Liverpool, United Kingdom.
You can find a link to his slides for that presentation below.
A full version of the paper that includes all proofs has been made available on arXiv.
You can find both the peer-reviewed, officially published conference version and the full version below.
Paper: Liveness verification and synthesis - New algorithms for recursive programs
R. Meyer, S. Muskalla, and E. Neumann
Liveness verification and synthesis - New algorithms for recursive programs
Unpublished; Preprint available as arXiv 1701.02947
The paper Liveness verification and synthesis - New algorithms for recursive programs authored by Roland Meyer, Elisabeth Neumann, and me has not been published in a peer-reviewed form.
Instead, it can be found on arXiv.
In the paper, we consider decision problems associated to the omega-languages of context-free grammars.
We give a novel definition of these omega-languages, languages of infinite words, that is easier and more elegant while leading to the same class of languages as defined by Linna and others.
We consider two decision problems.
The first is the problem of checking whether the omega-language of a given grammar is contained in a given omega-regular language.
The second is solving board games on arenas defined by context-free grammars with membership in an omega-regular language as the winning condition.
In both cases, we provide an algorithm whose main step is solving a system of equations that characterizes the behavior of the grammar.
Our work on the first problem generalizes earlier work by Holík and Meyer from the case of safety verification to liveness verification.
The second problem is an extension of the theory we have presented in our paper Summaries for context-free games.
R. Meyer and S. Muskalla
Munchausen iteration
Unpublished; Preprint available as arXiv 1605.00422
The paper Munchausen iteration authored by Roland Meyer and me has not been published in a peer-reviewed form.
Instead, it can be found on arXiv.
In the paper, we consider systems of equations over so-called io-semirings.
Such systems occur in the context of program verification.
We present a method for finding the least solution to such a system of equations that works by computing over the semiring of functions.
The method improves its precision by substitution rather than by computation, so we named it after after the fictional Baron Munchausen who pulled himself out of a swamp by his own hair.
We show that the method is related to Newton iteration, another procedure to solve equations over io-semirings that was introduced by Esparza, Kiefer, and Luttenberger and that is loosely related to Newton's method for finding the roots of differentiable functions.
Master's thesis: Computing boundaries of tropical varieties
I completed my studies in mathematics and computer science at TU Kaiserslautern with a Master of Science (M.Sc.) degree in 2015.
My master's thesis Computing boundaries of tropical varieties in mathematics was supervised by Thomas Markwig.
The thesis contributes to an area of research called tropical geometry.
The tropicalization of an algebraic variety (a geometric object defined by polynomial equations) transforms it into a simpler object while preserving some characteristic properties.
My thesis is concerned with computing the so-called boundary of a tropical variety.
It provides theoretical results as well as libraries for the computer algebra system Singular.
Bachelor's thesis: Solving integer programs using the algorithm of Hosten and Sturmfels
I completed my undergraduate studies in mathematics and computer science at TU Kaiserslautern with a Bachelor of Science (B.Sc.) degree in 2013.
My bachelor's thesis Solving integer programs using the algorithm of Hosten and Sturmfels in mathematics was supervised by Thomas Markwig.
The thesis is concerned with an algorithm that translates integer programming, an optimization problem, into a problem in the realm of commutative algebra.
The latter can then be solved using methods from computer algebra.
This algorithm was introduced in a 1995 paper by Serkan Hosten and Bernd Sturmfels.
My thesis provides the necessary preliminaries, gives a detailed explanation of the algorithm and a formal proof of soundness.