Mailing address
Georg Zetzsche
Max Planck Institute for Software Systems
Paul-Ehrlich Strasse G 26
67663 Kaiserslautern
Germany Email
g e o r g (at) m p i - s w s . o r g Mastodon @gz@chaos.social
Before
that, I obtained a PhD with Prof. Dr. Roland
Meyer in the Concurrency Theory
Group in Kaiserslautern. I defended my
dissertation on June 19th, 2015. Until December 2010, I studied
Computer Science (with a minor in Mathematics) at Universität Hamburg.
My research is concerned with theoretical foundations of verification
and synthesis of software systems. More specifically, I am interested
in decidability and complexity issues of infinite-state systems. One
current focus is synthesis of finite-state abstractions of
infinite-state systems (separability problems, downward closures,
Parikh images), which can be used as correctness certificates or as
building blocks for decision procedures.
In addition, I am working on decision problems for infinite groups,
where I seek to apply methods from verification and gain insights on
how to devise infinite-state models with pleasant analysis properties.
News
Together with Anthony W. Lin, I'm organizing the Theorietag 2023 on automata and formal languages.
My project FINABIS, Finite-state abstractions of infinite-state systems, will be funded by an ERC Starting Grant. Thanks a lot to everyone who gave me advice on the application!
@MISC{BaumannKeskinMeyerZetzsche2024a,
AUTHOR = {Baumann, Pascal and Keskin, Eren and Meyer, Roland and Zetzsche, Georg},
TITLE = {Separability in B{\"u}chi VASS and Singly Non-Linear Systems of Inequalities},
NOTE = {To appear in Proc. of the 51st EATCS International Colloquium on Automata, Languages, and Programming (ICALP 2024)}
}
@MISC{HaaseMadnaniKrishnaMishraZetzsche2024a,
AUTHOR = {Haase, Christoph and S., Krishna and Madnani, Khushraj and Mishra, Om Swostik and Zetzsche, Georg},
TITLE = {An efficient quantifier elimination procedure for Presburger arithmetic},
NOTE = {To appear in Proc. of the 51st EATCS International Colloquium on Automata, Languages, and Programming (ICALP 2024)}
}
@MISC{CiobanuZetzsche2024a,
AUTHOR = {Ciobanu, Laura and Zetzsche, Georg},
TITLE = {Slice closures of indexed languages and word equations with counting constraints},
NOTE = {To appear in Proc. of the Thirty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024)}
}
@MISC{AnandSchmitzSchuetzeZetzsche2024a,
AUTHOR = {Anand, Ashwani and Schmitz, Sylvain and Sch{\"u}tze, Lia and Zetzsche, Georg},
TITLE = {Verifying unboundedness via amalgamation},
NOTE = {To appear in Proc. of the Thirty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024)}
}
Abstract
We study the problem of deciding whether a given language is directed. A
language $L$ is \emph{directed} if every pair of words in $L$ have a common (scattered)
superword in $L$. Deciding directedness is a fundamental problem in connection
with ideal decompositions of downward closed sets.
% A language $L$ is directed if and only if the ideal
%decomposition of $L$'s downward closure consists of exactly one ideal.
Another motivation is that deciding whether two \emph{directed} context-free
languages have the same downward closures can be decided in polynomial time,
whereas for general context-free languages, this problem is known to be $\coNEXP$-complete.
We show that the directedness problem for regular languages, given as NFAs, belongs to
$\AC^1$, and thus polynomial time. Moreover, it is $\NL$-complete for fixed
alphabet sizes. Furthermore, we show that for context-free languages,
the directedness problem is $\PSPACE$-complete.
@INPROCEEDINGS{GanardiSaglamZetzsche2024a,
AUTHOR = {Ganardi, Moses and Salam, Irmak and Zetzsche, Georg},
TITLE = {Directed Regular and Context-Free Languages},
BOOKTITLE = {Proc. of the 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
YEAR = {2024},
SERIES = {LIPIcs},
VOLUME = {289},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
ADDRESS = {Dagstuhl, Germany},
PAGES = {36:1--36:20},
DOI = {10.4230/LIPICS.STACS.2024.36}
}
Abstract
Pushdown Vector Addition Systems with States (PVASS) consist of finitely many control states, a pushdown stack, and a set of counters that can be incremented and decremented, but not tested for zero.
Whether the reachability problem is decidable for PVASS is a long-standing open problem.
We consider continuous PVASS, which are PVASS with a continuous semantics.
This means, the counter values are rational numbers and whenever a vector is added to the current counter values, this vector is first scaled with an arbitrarily chosen rational factor between zero and one.
We show that reachability in continuous PVASS is NEXPTIME-complete.
Our result is unusually robust: Reachability can be decided in NEXPTIME even if all numbers are specified in binary.
On the other hand, NEXPTIME-hardness already holds for coverability, in fixed dimension, for bounded stack, and even if all numbers are specified in unary.
@INPROCEEDINGS{BalasubramanianMajumdarThinniyamZetzsche2024a,
AUTHOR = {Balasubramanian, A. R. and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {Reachability in Continuous Pushdown VASS},
BOOKTITLE = {Proc. of the 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024)},
YEAR = {2024},
PUBLISHER = {ACM},
ADDRESS = {USA},
SERIES = {Proceedings of the ACM on Programming Languages},
DOI = {10.1145/3633279}
}
Abstract
We study Satisfiability Modulo Theories (SMT) enriched with the so-called
Ramsey quantifiers, which assert the existence of cliques (complete graphs)
in the graph induced by some formulas. The extended framework is known to
have
applications in
proving program termination (in particular, whether a transitive binary
predicate is well-founded), and monadic decomposability of SMT formulas.
Our main result is a new algorithm for eliminating Ramsey
quantifiers from three common SMT theories: Linear Integer Arithmetic (LIA),
Linear Real Arithmetic (LRA), and Linear Integer Real Arithmetic (LIRA).
In particular, if we work only with existentially quantified formulas, then our
algorithm runs in polynomial time and produces a formula of linear size. One
immediate consequence is
that checking well-foundedness of a given formula in the aforementioned theory
defining a transitive predicate
can be straightforwardly handled by highly optimized SMT-solvers. We show also
how this provides a
uniform semi-algorithm for verifying termination and liveness with
completeness guarantee
(in fact, with an optimal computational complexity) for several well-known
classes of
infinite-state systems, which include succinct timed systems, one-counter
systems, and monotonic counter systems.
Another immediate consequence is a solution to an open problem on checking
monadic decomposability of a given relation in quantifier-free fragments of
LRA and LIRA, which is an
important problem in automated reasoning and constraint databases. Our
result immediately implies decidability of this problem with an optimal
complexity (coNP-complete) and enables exploitation of SMT-solvers. It also
provides a termination guarantee for the generic monadic decomposition
algorithm of Veanes et al. for LIA, LRA, and LIRA. We report encouraging
experimental results on a prototype implementation of our algorithms on
micro-benchmarks.
@INPROCEEDINGS{BergstraesserGanardiLinZetzsche2024a,
AUTHOR = {Bergstr{\"a}{\ss}er, Pascal and Ganardi, Moses and Lin, Anthony W. and Zetzsche, Georg},
TITLE = {Ramsey Quantifiers in Linear Arithmetics},
BOOKTITLE = {Proc. of the 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024)},
YEAR = {2024},
PUBLISHER = {ACM},
ADDRESS = {USA},
SERIES = {Proceedings of the ACM on Programming Languages},
DOI = {10.1145/3632843}
}
Abstract
We study regular separators of vector addition systems (VASS, for
short) with coverability semantics. A regular language $R$ is a
\emph{regular separator} of languages $K$ and $L$ if $K\subseteq R$ and
$L\cap R=\emptyset$. It was shown by Czerwi\'{n}ski, Lasota, Meyer,
Muskalla, Kumar, and Saivasan~(CONCUR 2018) that it is decidable
whether, for two given VASS, there exists a regular separator. In fact,
they show that a regular separator exists if and only if the two VASS
languages are disjoint. However, they provide a triply exponential
upper bound and a doubly exponential lower bound for the size of such
separators and leave open which bound is tight.
We show that if two VASS have disjoint languages, then there exists a
regular separator with at most doubly exponential size. Moreover, we
provide tight size bounds for separators in the case of fixed
dimensions and unary/binary encodings of updates and NFA/DFA
separators. In particular, we settle the aforementioned question.
The key ingredient in the upper bound is a structural analysis of
separating automata based on the concept of \emph{basic separators}, which was
recently introduced by Czerwi\'{n}ski and the second author. This allows us to
determinize (and thus complement) without the powerset construction and avoid one exponential
blowup.
@INPROCEEDINGS{KoecherZetzsche2023a,
AUTHOR = {K{\"o}cher, Chris and Zetzsche, Georg},
TITLE = {Regular Separators for VASS Coverability Languages
},
BOOKTITLE = {Proc. of the 43rd Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
YEAR = {2023},
SERIES = {LIPIcs},
VOLUME = {284},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
ADDRESS = {Dagstuhl, Germany},
PAGES = {15:1--15:19},
DOI = {10.4230/LIPIcs.FSTTCS.2023.15}
}
Abstract
Bounding the number of reversals in a counter machine is one of the most
prominent restrictions to achieve decidability of the reachability problem.
Given this success, we explore whether this notion can be relaxed while
retaining decidability.
To this end, we introduce the notion of an
$f$-reversal-bounded counter machine for a monotone function $f\colon \N\to
\N$. In such a machine, every run of length $n$ makes at most $f(n)$ reversals. Our first main result is a dichotomy theorem: We show that for every
monotone function $f$, one of the following holds: Either (i)~$f$ grows so
slowly that every $f$-reversal bounded counter machine is already $k$-reversal
bounded for some constant $k$ or (ii)~$f$ belongs to $\Omega(\log(n))$ and
reachability in $f$-reversal bounded counter machines is undecidable. This
shows that classical reversal bounding already captures the decidable cases of
$f$-reversal bounding for any monotone function $f$. The key technical
ingredient is an analysis of the growth of small solutions of iterated
compositions of Presburger-definable constraints. In our second contribution, we investigate whether imposing $f$-reversal
boundedness improves the complexity of the reachability problem in vector
addition systems with states (VASS). Here, we obtain an analogous dichotomy:
We show that either (i)~$f$ grows so slowly that every $f$-reversal-bounded VASS is already $k$-reversal-bounded for some constant $k$ or (ii)~$f$ belongs to $\Omega(n)$ and the reachability problem for $f$-reversal-bounded VASS remains Ackermann-complete. This result is proven using run amalgamation in VASS.
Overall, our results imply that classical restriction of reversal boundedness is a robust one.
@INPROCEEDINGS{FinkelKrishnaMadnaniMajumdarZetzsche2023a,
AUTHOR = {Finkel, Alain and S., Krishna and Madnani, Khushraj and Majumdar, Rupak and Zetzsche, Georg},
TITLE = {Counter Machines With Infrequent Reversals},
BOOKTITLE = {Proc. of the 43rd Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
YEAR = {2023},
SERIES = {LIPIcs},
VOLUME = {284},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
ADDRESS = {Dagstuhl, Germany},
PAGES = {38:1--38:17},
DOI = {10.4230/LIPIcs.FSTTCS.2023.42}
}
Abstract
When a system sends messages through a lossy channel, then the language encoding all sequences of messages can be abstracted by its downward closure, i.e. the set of all (not necessarily contiguous) subwords. This is useful because even if the system has infinitely many states, its downward closure is a regular language. However, if the channel has congestion control based on priorities assigned to the messages, then we need a finer abstraction: The downward closure with respect to the priority embedding. As for subword-based downward closures, one can also show that these priority downward closures are always regular.
While computing finite automata for the subword-based downward closure is well understood, nothing is known in the case of priorities. We initiate the study of this problem and provide algorithms to compute priority downward closures for regular languages, one-counter languages, and context-free languages.
@INPROCEEDINGS{AnandZetzsche2023a,
AUTHOR = {Anand, Ashwani and Zetzsche, Georg},
TITLE = {Priority Downward Closures},
BOOKTITLE = {Proc. of the 34th International Conference on Concurrency Theory (CONCUR 2023)},
YEAR = {2023},
SERIES = {LIPIcs},
VOLUME = {279},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
ADDRESS = {Dagstuhl, Germany},
PAGES = {39:1--39:18},
DOI = {10.4230/LIPIcs.CONCUR.2023.39}
}
Abstract
Vector addition systems with states (VASS) are a popular model for concurrent systems. However, many decision problems have prohibitively high complexity. Therefore, it is sometimes useful to consider overapproximating semantics in which these problems can be decided more efficiently.
We study an overapproximation, called monus semantics, that slightly relaxes the semantics of decrements: A key property of a vector addition systems is that in order to decrement a counter, this counter must have a positive value. In contrast, our semantics allows decrements of zero-valued counters: If such a transition is executed, the counter just remains zero.
It turns out that if only a subset of transitions is used with monus semantics (and the others with classical semantics), then reachability is undecidable. However, we show that if monus semantics is used throughout, reachability remains decidable. In particular, we show that reachability for VASS with monus semantics is as hard as that of classical VASS (i.e. Ackermann-hard), while the zero-reachability and coverability are easier (i.e. EXPSPACE-complete and NP-complete, respectively). We provide a comprehensive account of the complexity of the general reachability problem, reachability of zero configurations, and coverability under monus semantics. We study these problems in general VASS, two-dimensional VASS, and one-dimensional VASS, with unary and binary counter updates.
@INPROCEEDINGS{BaumannMadnaniMazowieckiZetzsche2023a,
AUTHOR = {Baumann, Pascal and Madnani, Khushraj and Mazowiecki, Filip and Zetzsche, Georg},
TITLE = {Monus Semantics in Vector Addition Systems with States},
BOOKTITLE = {Proc. of the 34th International Conference on Concurrency Theory (CONCUR 2023)},
YEAR = {2023},
SERIES = {LIPIcs},
VOLUME = {279},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
ADDRESS = {Dagstuhl, Germany},
PAGES = {10:1--10:18},
DOI = {10.4230/LIPIcs.CONCUR.2023.10}
}
Abstract
Context-bounded analysis of concurrent programs is a technique to compute a sequence of under-approximations of all behaviors of the program. For a fixed bound k, a context bounded analysis considers only those runs in which a single process is interrupted at most k times. As k grows, we capture more and more behaviors of the program. Practically, context-bounding has been very effective as a bug-finding tool: many bugs can be found even with small bounds. Theoretically, context-bounded analysis is decidable for a large number of programming models for which verification problems are undecidable. In this paper, we survey some recent work in context-bounded analysis of multithreaded programs.
In particular, we show a general decidability result. We study context-bounded reachability in a language-theoretic setup. We fix a class of languages (satisfying some mild conditions) from which each thread is chosen. We show context-bounded safety and termination verification problems are decidable iff emptiness is decidable for the underlying class of languages and context-bounded boundedness is decidable iff finiteness is decidable for the underlying class.
@INPROCEEDINGS{BaumannGanardiMajumdarThinniyamZetzsche2023c,
AUTHOR = {Baumann, Pascal and Ganardi, Moses and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {Context-Bounded Analysis of Concurrent Programs (Invited Talk)},
BOOKTITLE = {Proc. of the 50th EATCS International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
YEAR = {2023},
SERIES = {LIPIcs},
VOLUME = {261},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
ADDRESS = {Dagstuhl, Germany},
PAGES = {3:1--3:16},
DOI = {10.4230/LIPIcs.ICALP.2023.3}
}
Abstract
In the language-theoretic approach to refinement verification, we check that the
language of traces of an implementation all belong to the language of a specification.
We consider the refinement verification problem for asynchronous programs against specifications given by a Dyck
language.
We show that this problem is EXPSPACE-complete---the same complexity as that of language emptiness and for
refinement verification against a regular specification.
Our algorithm uses several technical ingredients.
First, we show that checking if the coverability language of a succinctly described
vector addition system with states (VASS) is contained in a Dyck language
is EXPSPACE-complete.
Second, in the more technical part of the proof, we define an ordering on words and show a downward closure construction that
allows replacing the (context-free) language of each task in an asynchronous program by a regular language.
Unlike downward closure operations usually considered in infinite-state verification, our ordering is not a well-quasi-ordering, and we have
to construct the regular language ab initio.
Once the tasks can be replaced, we show a reduction to an appropriate VASS and use our first ingredient.
In addition to the inherent theoretical interest, refinement verification with Dyck specifications captures common
practical resource usage patterns based on reference counting, for which few algorithmic techniques were known.
@INPROCEEDINGS{BaumannGanardiMajumdarThinniyamZetzsche2023b,
AUTHOR = {Baumann, Pascal and Ganardi, Moses and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {Checking Refinement of Asynchronous Programs against Context-Free Specifications},
BOOKTITLE = {Proc. of the 50th EATCS International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
YEAR = {2023},
SERIES = {LIPIcs},
VOLUME = {261},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
ADDRESS = {Dagstuhl, Germany},
PAGES = {110:1--110:20},
DOI = {10.4230/LIPIcs.ICALP.2023.110}
}
Abstract
We consider a general class of decision problems concerning formal languages, called ``(one-dimensional) unboundedness predicates'', for automata that feature reversal-bounded counters (RBCA). We show that each problem in this class reduces -- non-deterministically in polynomial time -- to the same problem for just finite automata. We also show an analogous reduction for automata that have access to both a pushdown stack and reversal-bounded counters (PRBCA).
This allows us to answer several open questions: For example, we show that it is coNP-complete to decide whether a given (P)RBCA language L is bounded, meaning whether there exist words $w_1,\ldots,w_n$ with $L\subseteq w_1^*w_2^*\cdots w_n^*$. For PRBCA, even decidability was open. Our methods also show that there is no language of a (P)RBCA of intermediate growth. This means, the number of words of each length grows either polynomially or exponentially. Part of our proof is likely of independent interest: We show that one can translate an RBCA into a machine with Z-counters in logarithmic space, while preserving the accepted language.
@INPROCEEDINGS{BaumannDAlessandroGanardiIbarraMcQuillenSchuetzeZetzsche2023a,
AUTHOR = {Baumann, Pascal and D'Alessandro, Flavio and Ibarra, Oscar and Ganardi, Moses and McQuillan, Ian and Sch{\"u}tze, Lia and Zetzsche, Georg},
TITLE = {Unboundedness problems for machines with reversal-bounded counters},
BOOKTITLE = {Proc. of the 26th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2023)},
YEAR = {2023},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer},
VOLUME = {13992},
PAGES = {240--264},
DOI = {10.1007/978-3-031-30829-1\_12}
}
Abstract
We study the regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages $L_1$ and $L_2$, check whether there is a regular language that fully contains $L_1$ while remaining disjoint from $L_2$.
We show that the problem is decidable in general and PSPACE-complete in the 1-dimensional case, assuming succinct counter updates.
The results rely on several arguments.
We characterize the set of all regular languages disjoint from $L_2$.
Based on this, we derive a (sound and complete) notion of inseparability witnesses, non-regular subsets of $L_1$.
Finally, we show how to symbolically represent inseparability witnesses and how to check their existence.
@INPROCEEDINGS{BaumannMeyerZetzsche2023a,
AUTHOR = {Baumann, Pascal and Meyer, Roland and Zetzsche, Georg},
TITLE = {Regular Separability in B{\"u}chi VASS},
BOOKTITLE = {Proc. of the 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
YEAR = {2023},
SERIES = {LIPIcs},
VOLUME = {254},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
ADDRESS = {Dagstuhl, Germany},
PAGES = {9:1--9:19},
DOI = {10.4230/LIPIcs.STACS.2023.9}
}
Abstract
A fundamental problem in refinement verification is to check that the language of behaviors of an implementation
is included in the language of the specification.
We consider the refinement verification problem where the implementation is a multithreaded shared memory system
modeled as a multistack pushdown automaton and the specification is an input-deterministic multistack pushdown language.
Our main result shows that the context-bounded refinement problem, where we ask that all behaviors
generated in runs of bounded number of context switches belong to a specification given by a Dyck language,
is decidable and coNP-complete.
The more general case of input-deterministic languages follows, with the same complexity.
Context-bounding is essential since emptiness for multipushdown automata is already undecidable, and so is the refinement verification problem for the subclass
of regular specifications.
Input-deterministic languages capture many non-regular specifications of practical interest and our result opens the way for algorithmic analysis of these properties.
The context-bounded refinement problem is coNP-hard already with deterministic regular specifications;
our result demonstrates that the problem is not harder despite the stronger class of specifications.
Our proof introduces several general techniques for formal languages and counter programs and shows that the search for counterexamples
can be reduced in non-deterministic polynomial time to the satisfiability problem for existential Presburger arithmetic.
These techniques are essential to ensure the coNP upper bound: existing techniques for regular specifications are not powerful enough
for decidability, while simple reductions lead to problems that are either undecidable or have high complexities.
As a special case, our decidability result gives an algorithmic verification technique to reason about
reference counting and re-entrant locking in multithreaded programs.
@INPROCEEDINGS{BaumannGanardiMajumdarThinniyamZetzsche2023a,
AUTHOR = {Baumann, Pascal and Ganardi, Moses and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {Context-Bounded Verification of Context-Free Specifications},
BOOKTITLE = {Proc. of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023)},
YEAR = {2023},
PUBLISHER = {ACM},
ADDRESS = {USA},
SERIES = {Proceedings of the ACM on Programming Languages},
DOI = {10.1145/3571266}
}
Abstract
We show that the subset sum problem, the knapsack problem and the rational subset membership problem for permutation groups are NP-complete.
Concerning the knapsack problem we obtain NP-completeness for every fixed n \geq 3, where n is the number of permutations in the knapsack equation. In other words: membership in products of three cyclic permutation groups is NP-complete. This sharpens a result of Luks, which states NP-completeness of the membership problem for products of three abelian permutation groups. We also consider the context-free membership problem in permutation groups and prove that it is PSPACE-complete but NP-complete for a restricted class of context-free grammars where acyclic derivation trees must have constant Horton-Strahler number. Our upper bounds hold for black box groups. The results for context-free membership problems
in permutation groups yield new complexity bounds for various intersection non-emptiness problems for DFAs and a single context-free grammar.
@INPROCEEDINGS{LohreyRosowskiZetzsche2022a,
AUTHOR = {Lohrey, Markus and Rosowski, Andreas and Zetzsche, Georg},
TITLE = {Membership problems in finite groups},
BOOKTITLE = {Proc. of the 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
YEAR = {2022},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
VOLUME = {241},
ADDRESS = {Dagstuhl, Germany},
SERIES = {LIPIcs},
DOI = {10.4230/LIPIcs.MFCS.2022.71}
}
Abstract
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store.
A PVASS is said to be bidirected if every transition (pushing/popping a symbol or modifying a counter)
has an accompanying opposite transition that reverses the effect.
Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachability.
We show that the reachability problem for bidirected PVASS is decidable in Ackermann
time and primitive recursive for any fixed dimension.
For the special case of one-dimensional bidirected PVASS, we show reachability is in PSPACE, and in fact in
polynomial time if the stack is polynomially bounded.
Our results are in contrast to the directed setting, where decidability of reachability is a long-standing open problem already
for one dimensional PVASS, and there is a PSPACE-lower bound already for one-dimenstional PVASS with bounded stack.
The reachability relation in the bidirected (stateless) case is a congruence over N^d.
Our upper bounds exploit saturation techniques over congruences.
In particular, we show novel elementary-time constructions of semilinear representations of congruences generated by finitely many vector pairs.
For the special case of one-dimensional PVASS, we show a saturation procedure over bounded-size counters.
We complement our upper bound with a TOWER-hardness result for arbitrary dimension and
k-EXPSPACE hardness in dimension 2k+6 using a technique by Lazić and Totzke
to implement iterative exponentiations.
@INPROCEEDINGS{GanardiMajumdarPavlogiannisSchuetzeZetzsche2022a,
AUTHOR = {Ganardi, Moses and Majumdar, Rupak and Pavlogiannis, Andreas and Sch{\"u}tze, Lia and Zetzsche, Georg},
TITLE = {Reachability in Bidirected Pushdown VASS},
BOOKTITLE = {Proc. of the 49th EATCS International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
YEAR = {2022},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
VOLUME = {229},
ADDRESS = {Dagstuhl, Germany},
SERIES = {LIPIcs},
DOI = {10.4230/LIPIcs.ICALP.2022.124}
}
Abstract
Reachability problems in infinite-state systems are often subject to extremely
high complexity.
This motivates the investigation of efficient overapproximations, where we add transitions to
obtain a system in which reachability can be decided more easily. We consider
bidirected infinite-state systems, where for every transition there is a
transition with opposite effect. We study bidirected reachability in the
framework of valence systems, an abstract model featuring finitely many control
states and an infinite-state storage that is specified by a finite graph.
By picking suitable graphs, valence systems can uniformly model counters as in vector addition systems,
pushdowns, integer counters, and combinations thereof.
We provide a comprehensive complexity landscape for bidirected reachability and show that
the complexity drops substantially (often to polynomial
time) from that of general reachability, for almost every storage mechanism
where reachability is known to be decidable.
@INPROCEEDINGS{GanardiMajumdarZetzsche2022a,
AUTHOR = {Ganardi, Moses and Majumdar, Rupak and Zetzsche, Georg},
TITLE = {The complexity of bidirected reachability in valence systems},
YEAR = {2022},
BOOKTITLE = {Proc. of the Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022)},
PUBLISHER = {ACM},
PAGES = {1--15},
DOI = {10.1145/3531130.3533345}
}
Abstract
Automatic structures are infinite structures that are finitely represented by
synchronized finite-state automata. This paper concerns specifically automatic
structures over finite words and trees (ranked/unranked).
We investigate the ``directed version'' of Ramsey quantifiers, which
express the existence of an infinite directed clique. This subsumes the standard
``undirected version'' of Ramsey quantifiers.
Interesting connections between Ramsey quantifiers and two problems in verification
are firstly observed:
(1) reachability with Büchi and generalized Büchi conditions in regular
model checking can be seen as Ramsey quantification over transitive automatic
graphs (i.e. whose edge relations are transitive), (2) checking monadic
decomposability (a.k.a. recognizability) of automatic relations can be
viewed as Ramsey quantification
over co-transitive automatic graphs (i.e. the complements of whose edge
relations are transitive). We provide a comprehensive complexity
landscape of Ramsey quantifiers in these three cases (general, transitive,
co-transitive), all between NL and EXP. In turn, this yields a
wealth of new results with precise complexity, e.g., verification of subtree/flat prefix rewriting, as well as monadic
decomposability over tree-automatic relations.
We also obtain substantially simpler proofs, e.g., for NL complexity for monadic
decomposability over word-automatic relations (given by DFAs).
@INPROCEEDINGS{BergstraesserGanardiLinZetzsche2022a,
AUTHOR = {Bergstr{\"a}{\ss}er, Pascal and Ganardi, Moses and Lin, Anthony W. and Zetzsche, Georg},
TITLE = {Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification},
YEAR = {2022},
BOOKTITLE = {Proc. of the Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022)},
PUBLISHER = {ACM},
PAGES = {1--14},
DOI = {10.1145/3531130.3533346}
}
Abstract
We study first-order logic (FO) over the structure consisting of finite words
over some alphabet~$A$, together with the (non-contiguous) subword ordering.
In terms of decidability of quantifier alternation fragments, this logic is
well-understood: If every word is available as a constant, then even the
$\Sigma_1$ (i.e.\ existential) fragment is undecidable, already for binary
alphabets $A$.
However, up to now, little is known about the expressiveness of the
quantifier alternation fragments: For example, the undecidability proof for
the existential fragment relies on Diophantine equations and only
shows that recursively enumerable languages over a singleton alphabet (and
some auxiliary predicates) are definable.
We show that if $|A|\ge 3$, then a relation is definable in the existential
fragment over $A$ with constants if and only if it is recursively enumerable.
This implies characterizations for all fragments~$\Sigma_i$: If $|A|\ge 3$,
then a relation is definable in $\Sigma_i$ if and only if it belongs to the
$i$-th level of the arithmetical hierarchy. In addition, our result yields
an analogous complete description of the $\Sigma_i$-fragments for $i\ge 2$ of
the pure logic, where the words of $A^*$ are not available as
constants.
@INPROCEEDINGS{BaumannGanardiThinniyamZetzsche2022a,
AUTHOR = {Baumann, Pascal and Ganardi, Moses and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {Existential definability over the subword ordering},
BOOKTITLE = {Proc. of the 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)},
YEAR = {2022},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
VOLUME = {219},
ADDRESS = {Dagstuhl, Germany},
SERIES = {LIPIcs},
DOI = {10.4230/LIPIcs.STACS.2022.7}
}
Abstract
Thread pooling is a common programming idiom in which a fixed set of worker threads
are maintained to execute tasks concurrently.
The workers repeatedly pick tasks and execute them to completion.
Each task is sequential, with possibly recursive code, and tasks
communicate over shared memory.
Executing a task can lead to more new tasks being spawned.
We consider the safety verification problem for thread-pooled programs.
We parameterize the problem with two parameters:
the size of the thread pool as well as the number of context switches for each task.
The size of the thread pool determines the number of workers running concurrently.
The number of context switches determines how many times a worker can be swapped out while executing
a single task---like many verification problems for multithreaded recursive programs, the context bounding is important
for decidability.
We show that the safety verification problem for thread-pooled, context-bounded, Boolean programs
is EXPSPACE-complete, even if the size of the thread pool and the context bound are given in binary.
Our main result, the EXPSPACE upper bound, is derived using a sequence of new
succinct encoding techniques of independent language-theoretic interest.
In particular, we show a polynomial-time construction of downward closures
of languages accepted by succinct pushdown automata as doubly succinct nondeterministic finite automata.
While there are explicit doubly exponential lower bounds on the size of nondeterministic
finite automata accepting the downward closure, our result shows these automata can be compressed.
We show that thread pooling significantly reduces computational power:
in contrast, if only the context bound is provided in binary, but there
is no thread pooling, the safety verification problem becomes 3EXPSPACE-complete.
Given the high complexity lower bounds of related problems involving binary parameters,
the relatively low complexity of safety verification with thread-pooling comes as a surprise.
@INPROCEEDINGS{BaumannMajumdarThinniyamZetzsche2022a,
AUTHOR = {Baumann, Pascal and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {Context-Bounded Verification of Thread Pools},
BOOKTITLE = {Proc. of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022)},
YEAR = {2022},
PUBLISHER = {ACM},
ADDRESS = {USA},
SERIES = {Proceedings of the ACM on Programming Languages},
DOI = {10.1145/3498678}
}
Abstract
Valence systems are an abstract model of computation that consists of a finite-state control and some storage mechanism. In contrast to traditional models, the storage mechanism is not fixed, but given as a parameter. This allows us to precisely state questions like: For which storage mechanisms is the reachability problem decidable?
This survey reports on recent results that aim to understand the impact of the storage mechanism on decidability and complexity of several variants of the reachability problem. The considered problems are configuration reachability, model-checking first-order logic with reachability, and reachability under bounded context switching and scope-boundedness.
@INPROCEEDINGS{Zetzsche2021a,
AUTHOR = {Zetzsche, Georg},
TITLE = {Recent Advances on Reachability Problems for Valence Systems (Invited Talk)},
BOOKTITLE = {Proc. of the 15th International Conference on Reachability Problems (RP 2021)},
YEAR = {2021},
PUBLISHER = {Springer},
ADDRESS = {Cham},
PAGES = {52--65},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {13035},
DOI = {10.1007/978-3-030-89716-1_4}
}
Abstract
The model of asynchronous programming arises in many contexts,
from low-level systems software to high-level web programming.
We take a language-theoretic perspective and show general
decidability and undecidabilit y results for asynchronous
programs that capture all known results as well as show
decidability of new and important classes. As a main
consequence, we show decidability of safety, termination and
boundedness verification for \emph{higher-order} asynchronous
programs---such as OCaml programs using Lwt---and
undecidability of liveness verification already for order-2
asynchronous programs. We show that, surprisingly, safety and
termination verification of asynchronous programs with handlers
from a language class are decidable \emph{if{}f} emptiness is
decidable for the underlying language class.
Moreover, we show that configuration reachability and liveness
(fair termination) verification are equivalent, and
decidability of these problems implies decidability of the
well-known ``equal-letters'' problem on languages. Our results
close the decidability frontier for asynchronous programs.
@INPROCEEDINGS{MajumdarThinniyamZetzsche2021a,
AUTHOR = {Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {
General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
},
BOOKTITLE = {Proc. of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021)},
YEAR = {2021},
PUBLISHER = {Springer},
ADDRESS = {Cham},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12651},
DOI = {10.1007/978-3-030-72016-2_24}
}
Abstract
Multi-pushdown systems are a standard model for concurrent recursive programs, but they have an undecidable reachability problem. Therefore, there have been several proposals to underapproximate their sets of runs so that reachability in this underapproximation becomes decidable. One such underapproximation that covers a relatively high portion of runs is scope boundedness. In such a run, after each push to stack i, the corresponding pop operation must come within a bounded number of visits to stack i.
In this work, we generalize this approach to a large class of infinite-state systems. For this, we consider the model of valence systems, which consist of a finite-state control and an infinite-state storage mechanism that is specified by a finite undirected graph. This framework captures pushdowns, vector addition systems, integer vector addition systems, and combinations thereof. For this framework, we propose a notion of scope boundedness that coincides with the classical notion when the storage mechanism happens to be a multi-pushdown.
We show that with this notion, reachability can be decided in PSPACE for every storage mechanism in the framework. Moreover, we describe the full complexity landscape of this problem across all storage mechanisms, both in the case of (i) the scope bound being given as input and (ii) for fixed scope bounds. Finally, we provide an almost complete description of the complexity landscape if even a description of the storage mechanism is part of the input.
@INPROCEEDINGS{ShettyKrishnaZetzsche2021a,
AUTHOR = {Shetty, Aneesh and S., Krishna and Zetzsche, Georg},
TITLE = {Scope-Bounded Reachability in Valence Systems},
YEAR = {2021},
BOOKTITLE = {Proc. of the 32nd International Conference on Concurrency Theory (CONCUR 2021)},
YEAR = {2021},
SERIES = {LIPIcs},
VOLUME = {118},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
DOI = {10.4230/LIPIcs.CONCUR.2021.29}
}
Abstract
The knapsack problem for groups was introduced by Miasnikov,
Nikolaev, and Ushakov. It is defined for each finitely generated
group $G$ and takes as input group elements
$g_1,\ldots,g_n,g\in G$ and asks whether there are
$x_1,\ldots,x_n\ge 0$ with $g_1^{x_1}\cdots
g_n^{x_n}=g$. We study the knapsack problem for wreath products
$G\wr H$ of groups $G$ and $H$.
Our main result is a characterization of those wreath products
$G\wr H$ for which the knapsack problem is decidable. The
characterization is in terms of decidability properties of the
indiviual factors $G$ and $H$. To this end, we introduce two
decision problems, the \emph{intersection knapsack problem} and its
restriction, the \emph{positive intersection knapsack problem}.
Moreover, we apply our main result to $H_3(\Z)$, the discrete
Heisenberg group, and to Baumslag-Solitar groups $\BS(1,q)$ for
$q\ge 1$. First, we show that the knapsack problem is undecidable
for $G\wr H_3(\Z)$ for any $G\ne 1$. This implies that for $G\ne 1$
and for infinite and virtually nilpotent groups $H$, the knapsack
problem for $G\wr H$ is decidable if and only if $H$ is virtually
abelian and solvability of systems of exponent equations is
decidable for $G$. Second, we show that the knapsack problem is
decidable for $G\wr\BS(1,q)$ if and only if solvability of systems
of exponent equations is decidable for $G$.
@INPROCEEDINGS{BergstraesserGanardiZetzsche2021a,
AUTHOR = {Bergstr{\"a}{\ss}er, Pascal and Ganardi, Moses and Zetzsche, Georg},
TITLE = {A characterization of wreath products where knapsack is decidable},
BOOKTITLE = {Proc. of the 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)},
YEAR = {2021},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
VOLUME = {187},
ADDRESS = {Dagstuhl, Germany},
SERIES = {LIPIcs},
DOI = {10.4230/LIPIcs.STACS.2021.11}
}
Abstract
We study context-bounded verification of liveness properties of
multi-threaded, shared-memory programs, where each thread can
spawn additional threads. Our main result shows that
context-bounded fair termination is decidable for the model;
context-bounded implies that each spawned thread can be context
switched a fixed constant number of times. Our proof is
technical, since fair termination requires reasoning about the
composition of unboundedly many threads each with unboundedly
large stacks. In fact, techniques for related problems, which
depend crucially on replacing the pushdown threads with
finite-state threads, are not applicable. Instead, we introduce
an extension of vector addition systems with states (VASS), called
VASS with balloons (VASSB), as an intermediate model; it is an
infinite-state model of independent interest. A VASSB allows
tokens that are themselves markings (balloons). We show that
context bounded fair termination reduces to fair termination for
VASSB. We show the latter problem is decidable by showing a
series of reductions: from fair termination to configuration
reachability for VASSB and thence to the reachability problem for
VASS. For a lower bound, fair termination is known to be
non-elementary already in the special case where threads run to
completion (no context switches).
We also show that the simpler problem of context-bounded
termination is 2EXPSPACE-complete, matching the complexity
bound---and indeed the techniques---for safety verification.
Additionally, we show the related problem of \emph{fair
starvation}, which checks if some thread can be starved along a
fair run, is also decidable in the context-bounded case. The
decidability employs an intricate reduction from fair starvation
to fair termination. Like fair termination, this problem is also
non-elementary.
@INPROCEEDINGS{BaumannMajumdarThinniyamZetzsche2021a,
AUTHOR = {Baumann, Pascal and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs},
BOOKTITLE = {Proc. of the 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021)},
YEAR = {2021},
PUBLISHER = {ACM},
ADDRESS = {USA},
SERIES = {Proceedings of the ACM on Programming Languages},
DOI = {10.1145/3434325}
}
@INPROCEEDINGS{LohreyZetzsche2020a,
AUTHOR = {Lohrey, Markus and Zetzsche, Georg},
TITLE = {Knapsack and the power word problem in solvable Baumslag-Solitar groups},
YEAR = {2020},
BOOKTITLE = {Proc. of the 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
VOLUME = {170},
ADDRESS = {Dagstuhl, Germany},
SERIES = {LIPIcs},
DOI = {10.4230/LIPIcs.MFCS.2020.67}
}
@INPROCEEDINGS{BaumannMajumdarThinniyamZetzsche2020a,
AUTHOR = {Baumann, Pascal and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {The complexity of bounded context switching with dynamic thread creation},
YEAR = {2020},
BOOKTITLE = {Proc. of the 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
VOLUME = {168},
ADDRESS = {Dagstuhl, Germany},
SERIES = {LIPIcs},
DOI = {10.4230/LIPIcs.ICALP.2020.111}
}
@INPROCEEDINGS{CadilhacChistikovZetzsche2020a,
TITLE = {Rational subsets of Baumslag-Solitar groups},
AUTHOR = {Cadilhac, Micha{\"e}l and Chistikov, Dmitry and Zetzsche, Georg},
YEAR = {2020},
BOOKTITLE = {Proc. of the 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
VOLUME = {168},
ADDRESS = {Dagstuhl, Germany},
SERIES = {LIPIcs},
DOI = {10.4230/LIPIcs.ICALP.2020.116}
}
@INPROCEEDINGS{FigeliusGanardiLohreyZetzsche2020a,
TITLE = {The complexity of knapsack problems in wreath products},
AUTHOR = {Figelius, Michael and Ganardi, Moses and Lohrey, Markus and Zetzsche, Georg},
YEAR = {2020},
BOOKTITLE = {Proc. of the 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
VOLUME = {168},
ADDRESS = {Dagstuhl, Germany},
SERIES = {LIPIcs},
DOI = {10.4230/LIPIcs.ICALP.2020.126}
}
Abstract
We consider extensions of monadic second order logic over
$\omega$-words, which are obtained by adding one language that
is not $\omega$-regular. We show that if the added language $L$
has a neutral letter, then the resulting logic is necessarily
undecidable. A corollary is that the $\omega$-regular languages
are the only decidable Boolean-closed full trio over
$\omega$-words.
@INPROCEEDINGS{BojanczykKelmendiStefanskiZetzsche2020a,
AUTHOR = {Boja{\'{n}}czyk, Miko{\l}aj and Kelmendi, Edon and Stefa{\'{n}}ski, Rafa{\l} and Zetzsche, Georg},
TITLE = {Extensions of Omega-Regular Languages},
YEAR = {2020},
BOOKTITLE = {Proc. of the Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020)},
PUBLISHER = {ACM},
PAGES = {266--272},
EDITOR = {Holger Hermanns and Lijun Zhang and Naoki Kobayashi and Dale Miller},
DOI = {10.1145/3373718.3394779}
}
Abstract
We study the problem of regular separability of languages of
vector addition systems with states (VASS). It asks whether for
two given VASS languages $K$ and $L$, there exists a regular
language $R$ that includes $K$ and is disjoint from $L$. While
decidability of the problem in full generality remains an open
question, there are several subclasses for which decidability has
been shown: It is decidable for (i)~one-dimensional VASS,
(ii)~VASS coverability languages, (iii)~languages of integer
VASS, and (iv)~commutative VASS languages.
We propose a general approach to deciding regular
separability. We use it to decide regular separability of an
arbitrary VASS language from any language in the classes~(i),
(ii), and~(iii). This generalizes all previous results,
including~(iv).
@INPROCEEDINGS{CzerwinskiZetzsche2020a,
AUTHOR = {Czerwi{\'{n}}ski, Wojciech and Zetzsche, Georg},
TITLE = {An Approach to Regular Separability in Vector Addition Systems},
BOOKTITLE = {Proc. of the Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020)},
PUBLISHER = {ACM},
PAGES = {341--354},
EDITOR = {Holger Hermanns and Lijun Zhang and Naoki Kobayashi and Dale Miller},
YEAR = {2020},
DOI = {10.1145/3373718.3394776}
}
@INPROCEEDINGS{ThinniyamZetzsche2019a,
AUTHOR = {Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {Regular Separability and Intersection Emptiness are Independent Problems},
BOOKTITLE = {Proc. of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
VOLUME = {150},
ADDRESS = {Dagstuhl, Germany},
YEAR = {2019},
SERIES = {LIPIcs}
}
Abstract
We consider the model of pushdown vector addition systems with
resets. These consist of vector addition systems that have access
to a pushdown stack and have instructions to reset counters. For
this model, we study the coverability problem. In the absence of
resets, this problem is known to be decidable for one-dimensional
pushdown vector addition systems, but decidability is open for
general pushdown vector addition systems. Moreover, coverability
is known to be decidable for reset vector addition systems without
a pushdown stack. We show in this note that the problem is
undecidable for one-dimensional pushdown vector addition systems
with resets.
@INPROCEEDINGS{SchmitzZetzsche2019a,
AUTHOR = {Schmitz, Sylvain and Zetzsche, Georg},
TITLE = {Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets},
BOOKTITLE = {Proc. of the 13th International Conference on Reachability Problems (RP 2019)},
YEAR = {2019},
PUBLISHER = {Springer},
ADDRESS = {Cham},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {11674},
DOI = {10.1007/978-3-030-30806-3_15}
}
Abstract
We study the computational complexity of existential Presburger
arithmetic with (possibly nested occurrences of) a Kleene-star
operator. In addition to being a natural extension of Presburger
arithmetic, our investigation is motivated by two other decision
problems.
The first problem is the rational subset membership problem in graph
groups. A graph group is an infinite group specified by a finite
undirected graph. While a characterisation of graph groups with a
decidable rational subset membership problem was given by Lohrey and
Steinberg [J. Algebra, 320(2) (2008)], it has been an open
problem (i) whether the decidable fragment has elementary complexity
and (ii) what is the complexity for each fixed graph group. The
second problem is the reachability problem for integer vector
addition systems with states and nested zero tests.
We prove that the satisfiability problem for existential Presburger
arithmetic with stars is NEXP-complete and that all three
problems are polynomially inter-reducible. Moreover, we consider for
each problem a variant with a fixed parameter: We fix the
star-height in the logic, the group for the membership problem, and
the number of distinct zero-tests in the integer vector addition
systems. We establish NP-completeness of all problems with fixed
parameters.
In particular, this enables us to obtain a complete description of
the complexity landscape of the rational subset membership problem
for fixed graph groups: If the graph is a clique, the problem is
NL-complete. If the graph is a disjoint union of cliques, it is
PTIME-complete. If it is a transitive forest (and not a union of
cliques), the problem is NP-complete. Otherwise, the problem is
undecidable.
@INPROCEEDINGS{HaaseZetzsche2019a,
AUTHOR = {Haase, Christoph and Zetzsche, Georg},
TITLE = {Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests},
PUBLISHER = {IEEE},
PAGES = {1--14},
BOOKTITLE = {Proc. of the Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019)},
YEAR = {2019},
DOI = {10.1109/LICS.2019.8785850}
}
Abstract
We consider a language together with the subword relation, the cover
relation, and regular predicates. For such structures, we consider
the extension of first-order logic by threshold- and modulo-counting
quantifiers. Depending on the language, the used predicates, and the
fragment of the logic, we determine four new combinations that yield
decidable theories. These results extend earlier ones where only the
language of all words without the cover relation and fragments of
first-order logic were considered.
@INPROCEEDINGS{KuskeZetzsche2019a,
AUTHOR = {Kuske, Dietrich and Zetzsche, Georg},
TITLE = {Languages ordered by the subword order},
BOOKTITLE = {Proc. of the 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2019)},
PAGES = {348--364},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {11425},
PUBLISHER = {Springer},
ADDRESS = {Cham},
YEAR = {2019},
DOI = {10.1007/978-3-030-17127-8_20}
}
Abstract
We study valence systems, finite-control programs over
infinite-state memories modeled in terms of graph monoids. Our
contribution is a notion of bounded context switching (BCS).
Valence systems generalize pushdowns, concurrent pushdowns, and
Petri nets. In these settings, our definition conservatively
generalizes existing notions. The main finding is that
reachability within a bounded number of context switches is in
$\NPTIME$, independent of the memory (the graph monoid). Our
proof is genuinely algebraic, and therefore contributes a new way
to think about BCS.
@INPROCEEDINGS{MeyerMuskallaZetzsche2018a,
AUTHOR = {Meyer, Roland and Muskalla, Sebastian and Zetzsche, Georg},
TITLE = {Bounded Context Switching for Valence Systems},
YEAR = {2018},
BOOKTITLE = {Proc. of the 29th International Conference on Concurrency Theory (CONCUR 2018)},
PAGES = {12:1--12:18},
YEAR = {2018},
SERIES = {LIPIcs},
VOLUME = {118},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
DOI = {10.4230/LIPIcs.CONCUR.2018.12}
}
Abstract
A vector addition system (VAS) with an initial and a final marking
and transition labels induces a language. In part because the
reachability problem in VAS remains far from being well-understood,
it is difficult to devise decision procedures for such languages.
This is especially true for checking properties that state
the existence of infinitely many words of a particular
shape. Informally, we call these \emph{unboundedness properties}.
We present a simple set of axioms for predicates that can express
unboundedness properties. Our main result is that such a
predicate is decidable for VAS languages as soon as it is decidable
for regular languages. Among other results, this allows us to show
decidability of (i)~separability by bounded regular languages,
(ii)~unboundedness of occurring factors from a language $K$ with
mild conditions on $K$, and (iii)~universality of the set of factors.
@INPROCEEDINGS{CzerwinskiHofmanZetzsche2018a,
AUTHOR = {Czerwi{\'{n}}ski, Wojciech and Hofman, Piotr and Zetzsche, Georg},
TITLE = {Unboundedness problems for languages of vector addition systems},
YEAR = {2018},
BOOKTITLE = {Proc. of the 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
PAGES = {119:1--119:15},
SERIES = {Leibniz International Proceedings in Informatics (LIPIcs)},
YEAR = {2018},
VOLUME = {107},
EDITOR = {Ioannis Chatzigiannakis and Christos Kaklamanis and D{\'a}niel Marx and Donald Sannella},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
ADDRESS = {Dagstuhl, Germany},
DOI = {10.4230/LIPIcs.ICALP.2018.119}
}
Abstract
We introduce a flexible class of well-quasi-orderings (WQOs) on
words that generalizes the ordering of (not necessarily contiguous)
subwords.
Each such WQO induces a class of piecewise testable languages (PTLs)
as Boolean combinations of upward closed sets. In this way, a range
of regular language classes arises as PTLs. Moreover, each of the
WQOs guarantees regularity of all downward closed sets.
We consider two problems. First, we study which (perhaps
non-regular) language classes allow to decide whether two given
languages are separable by a PTL with respect to a given
WQO. Second, we want to effectively compute downward closures with
respect to these WQOs.
Our first main result is that for each of the WQOs, under mild
assumptions, both problems reduce to the simultaneous unboundedness
problem (SUP) and are thus solvable for many powerful system
models. In the second main result, we apply the framework to show
decidability of separability of regular languages by
$\mathcal{B}\Sigma_1[<, \mathsf{mod}]$, a fragment of
first-order logic with modular predicates.
@INPROCEEDINGS{Zetzsche2018a,
AUTHOR = {Zetzsche, Georg},
TITLE = {Separability by piecewise testable languages and downward closures beyond subwords},
YEAR = {2018},
BOOKTITLE = {Proc. of the Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)},
PAGES = {929--938},
YEAR = {2018},
EDITOR = {Anuj Dawar and Erich Gr{\"a}del},
PUBLISHER = {ACM},
YEAR = {2018},
DOI = {10.1145/3209108.3209201}
}
Abstract
In recent years, knapsack problems for (in general
non-commutative) groups have attracted attention. In this paper,
the knapsack problem for wreath products is studied. It turns out
that decidability of knapsack is not preserved under wreath
product. On the other hand, the class of knapsack-semilinear
groups, where solutions sets of knapsack equations are effectively
semilinear, is closed under wreath product. As a consequence, we
obtain the decidability of knapsack for free solvable
groups. Finally, it is shown that for every non-trivial abelian
group $G$, knapsack (as well as the related subset sum problem)
for the wreath product $G \wr \Z$ is $\NP$-complete.
@INPROCEEDINGS{GanardiKoenigLohreyZetzsche2017a,
AUTHOR = {Ganardi, Moses and K{\"o}nig, Daniel and Lohrey, Markus and Zetzsche, Georg},
TITLE = {Knapsack problems for wreath products},
YEAR = {2018},
PAGES = {32:1--32:13},
SERIES = {Leibniz International Proceedings in Informatics (LIPIcs)},
EDITOR = {Rolf Niedermeier and Brigitte Val{\'{e}}e},
ADDRESS = {Dagstuhl, Germany},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
VOLUME = {96},
BOOKTITLE = {Proc. of the 35th International Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
DOI = {10.4230/LIPIcs.STACS.2018.32}
}
Abstract
We consider first-order logic over the subword ordering on finite
words, where each word is available as a constant. Our first result is that the
$\Sigma_1$ theory is undecidable (already over two letters).
We investigate
the decidability border by considering fragments where all but a certain number
of variables are alternation bounded, meaning that the variable must always be
quantified over languages with a bounded number of letter alternations. We
prove that when at most two variables are not alternation bounded, the $\Sigma_1$
fragment is decidable, and that it becomes undecidable when three variables are
not alternation bounded. Regarding higher quantifier alternation depths, we
prove that the $\Sigma_2$ fragment is undecidable already for one variable without
alternation bound and that when all variables are alternation bounded, the
entire first-order theory is decidable.
@INPROCEEDINGS{HalfonSchnoebelenZetzsche2017a,
AUTHOR = {Halfon, Simon and Schnoebelen, Philippe and Zetzsche, Georg},
TITLE = {Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering},
BOOKTITLE = {Proc. of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)},
PAGES = {1--12},
PUBLISHER = {IEEE Computer Society},
YEAR = {2017}
}
Abstract
Myasnikov et al. have introduced the knapsack problem for arbitrary finitely
generated groups. In previous work, the authors proved that for each graph
group, the knapsack problem can be solved in NP. Here, we determine the
exact complexity of the problem for every graph group. While the problem is
TC0-complete for complete graphs, it is LogCFL-complete for each
(non-complete) transitive forest. For every remaining graph, the problem is
NP-complete.
@INPROCEEDINGS{LohreyZetzsche2017a,
AUTHOR = {Lohrey, Markus and Zetzsche, Georg},
TITLE = {The Complexity of Knapsack in Graph Groups},
YEAR = {2017},
PAGES = {52:1--52:14},
SERIES = {Leibniz International Proceedings in Informatics (LIPIcs)},
EDITOR = {Heribert Vollmer and Brigitte Val{\'{e}}e},
ADDRESS = {Dagstuhl, Germany},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
VOLUME = {66},
BOOKTITLE = {Proc. of the 34th International Symposium on Theoretical Aspects of Computer Science (STACS 2017)}
}
@INPROCEEDINGS{KoenigLohreyZetzsche2015a,
AUTHOR = {K{\"o}nig, Daniel and Lohrey, Markus and Zetzsche, Georg},
TITLE = {Knapsack and subset sum problems in nilpotent, polycyclic, and co-context-free groups},
BOOKTITLE = {Proc. of the AMS Special Session on Groups, Algorithms, and Cryptography (San Antonio, Texas, 2015)},
PUBLISHER = {American Mathematical Society},
ADDRESS = {Providence, RI, USA},
SERIES = {Contemporary Mathematics},
VOLUME = {677},
YEAR = {2016},
PAGES = {129},
DOI = {10.1090/conm/677}
}
Abstract
The downward closure of a language is the set of all (not necessarily
contiguous) subwords of its members. It is well-known that the downward
closure of every language is regular. Moreover, recent results show
that downward closures are computable for quite powerful system models.
One advantage of abstracting a language by its downward closure is that then,
equivalence and inclusion become decidable. In this work, we study the
complexity of these two problems. More precisely, we consider the following
decision problems: Given languages $K$ and $L$ from classes $\C$ and $\D$,
respectively, does the downward closure of $K$ include (equal) that of $L$?
These problems are investigated for finite automata, one-counter automata,
context-free grammars, and reversal-bounded counter automata. For each
combination, we prove a completeness result either for fixed or for arbitrary
alphabets. Moreover, for Petri net languages, we show that both problems are
Ackermann-hard and for higher-order pushdown automata of order $k$, we prove
hardness for complements of nondeterministic $k$-fold exponential time.
@INPROCEEDINGS{Zetzsche2016a,
AUTHOR = {Zetzsche, Georg},
TITLE = {The Complexity of Downward Closure Comparisons},
YEAR = {2016},
BOOKTITLE = {Proc. of the 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016)},
PAGES = {123:1--123:14},
SERIES = {Leibniz International Proceedings in Informatics (LIPIcs)},
EDITOR = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
ADDRESS = {Dagstuhl, Germany},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
VOLUME = {55},
YEAR = {2016}
}
Abstract
We study the computational and descriptional complexity
of the following transformation: Given a one-counter automaton (OCA) A,
construct a nondeterministic finite automaton (NFA) B
that recognizes an abstraction of the language of A:
its (1) downward closure, (2) upward closure, or (3) Parikh image.
For the Parikh image over a fixed alphabet and for the upward and
downward closures, we find polynomial-time algorithms that compute
such an NFA. For the Parikh image with the alphabet as part of
the input, we find a quasi-polynomial time algorithm and prove
a completeness result: we construct a sequence of OCA that admits
a polynomial-time algorithm iff there is one for all OCA.
For all three abstractions, it was previously unknown
if appropriate NFA of sub-exponential size exist.
@INPROCEEDINGS{AtigChistikovHofmanKumarSaivasanZetzsche2015a,
AUTHOR = {Atig, Mohamed Faouzi and Chistikov, Dmitry and Hofman, Piotr and Kumar, K Narayan and Saivasan, Prakash and Zetzsche, Georg},
TITLE = {The complexity of regular abstractions of one-counter languages},
YEAR = {2016},
PAGES = {207--216},
PUBLISHER = {ACM},
ADDRESS = {New York, NY, USA},
BOOKTITLE = {Proc. of the Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016)}
}
Abstract
First-order logic with the reachability predicate (FOR)
is an important means of specification in system analysis.
Its decidability status is known for some individual
types of infinite-state systems such as pushdown (decidable)
and vector addition systems (undecidable).
This work aims at a general understanding of which types of
systems admit decidability. As a unifying model, we employ
valence systems over graph monoids, which feature a
finite-state control and are parameterized by a monoid to
represent their storage mechanism. As special cases, this
includes pushdown systems, various types of counter systems
(such as vector addition systems) and combinations thereof.
Our main result is a complete characterization of those
graph monoids where FOR is decidable for the resulting
transition systems.
@INPROCEEDINGS{DOsualdoMeyerZetzsche2016a,
AUTHOR = {D'Osualdo, Emanuele and Meyer, Roland and Zetzsche, Georg},
TITLE = {First-order logic with reachability for infinite-state systems},
YEAR = {2016},
PAGES = {457--466},
PUBLISHER = {ACM},
ADDRESS = {New York, NY, USA},
BOOKTITLE = {Proc. of the Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016)}
}
Abstract
It is shown that the knapsack problem, which was introduced by Myasnikov et al.
for arbitrary finitely generated groups, can be solved in NP for graph
groups. This result even holds if the group elements are represented in a
compressed form by SLPs, which generalizes the classical NP-completeness
result of the integer knapsack problem. We also prove general transfer results:
NP-membership of the knapsack problem is passed on to finite
extensions, HNN-extensions over finite associated subgroups, and amalgamated
products with finite identified subgroups.
@INPROCEEDINGS{LohreyZetzsche2016a,
AUTHOR = {Lohrey, Markus and Zetzsche, Georg},
TITLE = {Knapsack in Graph Groups, HNN-Extensions and Amalgamated Products},
PAGES = {50:1--50:14},
SERIES = {Leibniz International Proceedings in Informatics (LIPIcs)},
EDITOR = {Nicolas Ollinger and Heribert Vollmer},
ADDRESS = {Dagstuhl, Germany},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
VOLUME = {47},
BOOKTITLE = {Proc. of the 33rd International Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
YEAR = {2016},
DOI = {10.4230/LIPIcs.STACS.2016.50}
}
Abstract
This work studies which storage mechanisms in automata permit
decidability of the reachability problem. The question is formalized
using valence automata, an abstract model that generalizes automata with
storage. For each of a variety of storage mechanisms, one can choose a
(typically infinite) monoid $M$ such that valence automata over $M$ are
equivalent to (one-way) automata with this type of storage.
In fact, many interesting storage mechanisms can be realized by monoids defined
by finite graphs, called graph monoids. Hence, we study for which graph
monoids the emptiness problem for valence automata is decidable. A particular
model realized by graph monoids is that of Petri nets with a pushdown stack.
For these, decidability is a long-standing open question and we do not answer
it here.
However, if one excludes subgraphs corresponding to this model, a
characterization can be achieved. This characterization yields a new extension
of Petri nets with a decidable reachability problem. Moreover, we provide a
description of those storage mechanisms for which decidability remains open.
This leads to a natural model that generalizes both pushdown Petri nets and
priority multicounter machines.
@INPROCEEDINGS{Zetzsche2015c,
AUTHOR = {Zetzsche, Georg},
TITLE = {The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets},
EDITOR = {Miko{\l}aj Boja{\'{n}}czyk and S{\l}awomir Lasota and Igor Potapov},
SERIES = {LNCS},
VOLUME = {9328},
PAGES = {166--178},
PUBLISHER = {Springer},
ADDRESS = {Berlin Heidelberg},
BOOKTITLE = {Proc. of the 9th International Workshop on Reachability Problems (RP 2015)},
YEAR = {2015},
DOI = {10.1007/978-3-319-24537-9_15}
}
Abstract
The downward closure of a word language is the set
of all (not necessarily contiguous) subwords of its
members. It is well-known that the downward closure of
any language is regular. While the downward closure
appears to be a powerful abstraction, algorithms for
computing a finite automaton for the downward closure
of a given language have been established only for few
language classes.
This work presents a simple general method for computing
downward closures. For language classes that are closed
under rational transductions, it is shown that the
computation of downward closures can be reduced to
checking a certain unboundedness property.
This result is used to prove that downward closures
are computable for (i) every language class with
effectively semilinear Parikh images that are closed
under rational transductions, (ii) matrix languages,
and (iii) indexed languages (equivalently, languages
accepted by higher-order pushdown automata of order~2).
@INPROCEEDINGS{Zetzsche2015b,
AUTHOR = {Zetzsche, Georg},
TITLE = {An Approach to Computing Downward Closures},
EDITOR = {Magn{\'{u}}s M. Halld{\'{o}}rsson and Kazuo Iwama and Naoki Kobayashi and Bettina Speckmann},
SERIES = {LNCS},
VOLUME = {9135},
PAGES = {440--451},
PUBLISHER = {Springer},
ADDRESS = {Berlin Heidelberg},
YEAR = {2015},
BOOKTITLE = {Proc. of the 42nd International Colloquium on Automata, Languages and Programming (ICALP 2015)},
DOI = {10.1007/978-3-662-47666-6_35}
}
Abstract
The downward closure of a language $L$ of words is the set of all (not
necessarily contiguous) subwords of members of $L$. It is well known that the
downward closure of any language is regular. Although the downward
closure seems to be a promising abstraction, there are only few language
classes for which an automaton for the downward closure is known to be
computable.
It is shown here that for stacked counter automata, the downward closure is
computable. Stacked counter automata are finite automata with a storage
mechanism obtained by \emph{adding blind counters} and \emph{building stacks}.
Hence, they generalize pushdown and blind counter automata.
The class of languages accepted by these automata are precisely those in the
hierarchy obtained from the context-free languages by alternating two closure
operators: imposing semilinear constraints and taking the algebraic extension.
The main tool for computing downward closures is the new concept of Parikh
annotations. As a second application of Parikh annotations, it is shown that
the hierarchy above is strict at every level.
@INPROCEEDINGS{Zetzsche2015a,
AUTHOR = {Zetzsche, Georg},
TITLE = {Computing downward closures for stacked counter automata},
PAGES = {743--756},
SERIES = {Leibniz International Proceedings in Informatics (LIPIcs)},
EDITOR = {Ernst W. Mayr and Nicolas Ollinger},
ADDRESS = {Dagstuhl, Germany},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
VOLUME = {30},
BOOKTITLE = {Proc. of the 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
YEAR = {2015},
DOI = {10.4230/LIPIcs.STACS.2015.743}
}
Abstract
We investigate the monoid of transformations that are induced by
sequences of writing to and reading from a queue storage. We describe
this monoid by means of a confluent and terminating semi-Thue system
and study some of its basic algebraic properties, e.g., conjugacy.
Moreover, we show that while several properties concerning its
rational subsets are undecidable, their uniform membership problem is
NL-complete. Furthermore, we present an algebraic characterization of
this monoid's recognizable subsets. Finally, we prove that it is not
Thurston-automatic.
@INPROCEEDINGS{HuschenbettKuskeZetzsche2014a,
AUTHOR = {Huschenbett, Martin and Kuske, Dietrich and Zetzsche, Georg},
TITLE = {The Monoid of Queue Actions},
BOOKTITLE = {Proc. of the 39th International Symposium on Mathematical Foundations of Computer Science (MFCS 2014)},
VOLUME = {8634},
EDITOR = {Csuhaj-Varj{\'{u}}, Erzs{\'{e}}bet and Dietzfelbinger, Martin and {\'{E}}sik, Zolt{\'{a}}n},
SERIES = {LNCS},
PUBLISHER = {Springer},
ADDRESS = {Berlin Heidelberg},
PAGES = {340--351},
YEAR = {2014},
DOI = {10.1007/978-3-662-44522-8_29}
}
Abstract
A Boolean closed full trio is a class of languages that is closed under the
Boolean operations (union, intersection, and complementation) and rational
transductions. It is well-known that the regular languages constitute such a
Boolean closed full trio. It is shown here that every such language class that
contains any non-regular language already includes the whole arithmetical
hierarchy (and even the one relative to this language).
A consequence of this result is that aside from the regular languages, no full
trio generated by one language is closed under complementation.
Our construction also shows that there is a fixed rational Kripke frame such
that assigning an arbitrary non-regular language to some variable allows the
definition of any language from the arithmetical hierarchy in the
corresponding Kripke structure using multimodal logic.
@INPROCEEDINGS{LohreyZetzsche2014a,
AUTHOR = {Lohrey, Markus and Zetzsche, Georg},
TITLE = {On {Boolean} closed full trios and rational {Kripke} frames},
BOOKTITLE = {Proc. of the 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)},
PAGES = {530--541},
SERIES = {Leibniz International Proceedings in Informatics (LIPIcs)},
VOLUME = {25},
EDITOR = {Mayr, Ernst W. and Portier, Natacha},
PUBLISHER = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
ADDRESS = {Dagstuhl, Germany},
YEAR = {2014},
DOI = {10.4230/LIPIcs.STACS.2014.530}
}
Abstract
Valence automata are a generalization of various models of automata with
storage. Here, each edge carries, in addition to an input word, an element of
a monoid. A computation is considered valid if multiplying the monoid elements
on the visited edges yields the identity element. By choosing suitable
monoids, a variety of automata models can be obtained as special valence
automata.
This work is concerned with the accepting power of valence automata.
Specifically, we ask for which monoids valence automata can accept only
context-free languages or only languages with semilinear Parikh image,
respectively.
First, we present a characterization of those graph products (of monoids) for
which valence automata accept only context-free languages. Second, we provide a
necessary and sufficient condition for a graph product of copies of the
bicyclic monoid and the integers to yield only languages with semilinear Parikh
image when used as a storage mechanism in valence automata. Third, we show that
all languages accepted by valence automata over torsion groups have a
semilinear Parikh image.
@INPROCEEDINGS{BuckheisterZetzsche2013a,
AUTHOR = {Buckheister, P. and Zetzsche, Georg},
TITLE = {Semilinearity and Context-Freeness of Languages Accepted by Valence Automata},
YEAR = {2013},
BOOKTITLE = {Proc. of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS 2013)},
EDITOR = {Chatterjee, Krishnendu and Sgall, Jir{\'{i}}},
PUBLISHER = {Springer},
ADDRESS = {Berlin Heidelberg},
PAGES = {231--242},
VOLUME = {8087},
SERIES = {LNCS},
DOI = {10.1007/978-3-642-40313-2_22}
}
Abstract
It is shown that membership in rational subsets of wreath
products $H \wr V$ with $H$ a finite group and $V$ a virtually
free group is decidable. On the other hand, it is shown that
there exists a fixed finitely generated submonoid in the wreath
product $\mathbb{Z}\wr\mathbb{Z}$ with an undecidable
membership problem.
@INPROCEEDINGS{LohreySteinbergZetzsche2013a,
AUTHOR = {Lohrey, Markus and Steinberg, Benjamin and Zetzsche, Georg},
TITLE = {Rational Subsets and Submonoids of Wreath Products},
BOOKTITLE = {Proc. of the 40th International Colloquium on Automata, Languages and Programming (ICALP 2013)},
EDITOR = {Fedor V. Fomin and R{\={u}}si{\c{n}}{\v{s}} Freivalds and Marta Kwiatkowska and David Peleg},
PUBLISHER = {Springer},
ADDRESS = {Berlin Heidelberg},
VOLUME = {7966},
SERIES = {LNCS},
YEAR = {2013},
PAGES = {361--372},
DOI = {10.1007/978-3-642-39212-2_33}
}
Abstract
We consider the computational power of silent transitions in one-way automata
with storage. Specifically, we ask which storage mechanisms admit a
transformation of a given automaton into one that accepts the same language
and reads at least one input symbol in each step.
We study this question using the model of valence automata. Here, a finite
automaton is equipped with a storage mechanism that is given by a monoid.
This work presents generalizations of known results on silent transitions.
For two classes of monoids, it provides characterizations of those monoids that
allow the removal of silent transitions. Both classes are defined by
graph products of copies of the bicyclic monoid and the group of integers. The
first class contains pushdown storages as well as the blind counters while the
second class contains the blind and the partially blind counters.
@INPROCEEDINGS{Zetzsche2013a,
AUTHOR = {Zetzsche, Georg},
TITLE = {Silent Transitions in Automata with Storage},
BOOKTITLE = {Proc. of the 40th International Colloquium on Automata, Languages and Programming (ICALP 2013)},
EDITOR = {Fedor V. Fomin and R{\={u}}si{\c{n}}{\v{s}} Freivalds and Marta Kwiatkowska and David Peleg},
PUBLISHER = {Springer},
ADDRESS = {Berlin Heidelberg},
VOLUME = {7966},
SERIES = {LNCS},
YEAR = {2013},
PAGES = {434--445},
DOI = {10.1007/978-3-642-39212-2_39}
}
Abstract
In each grammar model, it is an important question whether erasing productions
are necessary to generate all languages. Using the concept of grammars with
control languages by Salomaa, which offers a uniform treatment of a variety of
grammar models, we present a condition on the class of control languages that
guarantees that erasing productions are avoidable in the resulting grammar
model. On the one hand, this generalizes the previous result that in Petri net
controlled grammars, erasing productions can be eliminated. On the other hand,
it allows us to infer that the same is true for vector grammars.
@INPROCEEDINGS{Zetzsche2011c,
AUTHOR = {Zetzsche, Georg},
TITLE = {A Sufficient Condition for Erasing Productions to Be Avoidable},
BOOKTITLE = {Proc. of the 15th International Conference on Developments in Language Theory (DLT 2011)},
EDITOR = {Giancarlo Mauri and Alberto Leporati},
PUBLISHER = {Springer},
ADDRESS = {Berlin Heidelberg},
VOLUME = {6795},
SERIES = {LNCS},
PAGES = {452--463},
YEAR = {2011},
DOI = {10.1007/978-3-642-22321-1_39}
}
Abstract
During recent decades, classical models in language theory have been extended
by control mechanisms defined by monoids. We study which monoids cause the
extensions of context-free grammars, finite automata, or finite state
transducers to exceed the capacity of the original model. Furthermore, we
investigate when, in the extended automata model, the nondeterministic variant
differs from the deterministic one in capacity. We show that all these
conditions are in fact equivalent and present an algebraic characterization. In
particular, the open question of whether every language generated by a valence
grammar over a finite monoid is context-free is provided with a positive
answer.
@INPROCEEDINGS{Zetzsche2011b,
AUTHOR = {Zetzsche, Georg},
TITLE = {On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids},
BOOKTITLE = {Proc. of the 38th International Colloquium on Automata, Languages and Programming (ICALP 2011)},
EDITOR = {Luca Aceto et al.},
PUBLISHER = {Springer},
ADDRESS = {Berlin Heidelberg},
VOLUME = {6756},
SERIES = {LNCS},
PAGES = {222--233},
YEAR = {2011},
DOI = {10.1007/978-3-642-22012-8_17}
}
Abstract
Three open questions in the theory of regulated
rewriting are addressed. The first is whether every
permitting random context grammar has a non-erasing
equivalent. The second asks whether the same is true
for matrix grammars without appearance checking. The
third concerns whether permitting random context
grammars have the same generative capacity as matrix
grammars without appearance checking.
The main result is a positive answer to the first
question. For the other two, conjectures are
presented. It is then deduced from the main result
that at least one of the two holds.
@INPROCEEDINGS{Zetzsche2010,
AUTHOR = {Zetzsche, Georg},
TITLE = {On Erasing Productions in Random Context Grammars},
BOOKTITLE = {Proc. of the 37th International Colloquium on Automata, Languages and Programming (ICALP 2010)},
EDITOR = {
Abramsky, Samson and
Gavoille, Cyril and
Kirchner, Claude and
Meyer auf der Heide, Friedhelm and
Spirakis, Paul
},
VOLUME = {6199},
SERIES = {LNCS},
PUBLISHER = {Springer},
ADDRESS = {Berlin Heidelberg},
PAGES = {175--186},
YEAR = {2010},
DOI = {10.1007/978-3-642-14162-1_15}
}
Abstract
It is shown that applying linear erasing to a Petri net
language yields a language generated by a non-erasing
matrix grammar. The proof uses Petri net controlled
grammars. These are context-free grammars, where the
application of productions has to comply with a firing
sequence in a Petri net. Petri net controlled grammars are
equivalent to arbitrary matrix grammars (without
appearance checking), but a certain restriction on them
(linear Petri net controlled grammars) leads to the class
of languages generated by non-erasing matrix grammars.
It is also shown that in Petri net controlled grammars
(with final markings and arbitrary labeling), erasing
rules can be eliminated, which yields a reformulation of
the problem of whether erasing rules in matrix grammars
can be eliminated.
@INPROCEEDINGS{Zetzsche09,
AUTHOR = {Zetzsche, Georg},
TITLE = {Erasing in {Petri} Net Languages and Matrix Grammars},
BOOKTITLE = {Proc. of the 13th International Conference on Developments in Language Theory (DLT 2009)},
EDITOR = {Diekert, Volker and Nowotka, Dirk},
PAGES = {490--501},
VOLUME = {5583},
YEAR = {2009},
SERIES = {LNCS},
PUBLISHER = {Springer},
ADDRESS = {Berlin Heidelberg},
DOI = {10.1007/978-3-642-02737-6_40}
}
Abstract
We compare various modes of firing transitions in Petri nets
and define classes of languages defined this way. We define
languages through steps, i. e. sets of transitions, maximal
steps, multi-steps, and maximal multi-steps of transitions
in Petri nets, but in a different manner than those defined
in [Burk 81a,Burk 83], by considering labeled transitions.
We will show that we obtain a hierarchy of families of
languages defined by multiple use of transition in firing
transitions in a single multistep. Except for the maximal
multi-steps all classes can be simulated by sequential
firing of transitions.
@INPROCEEDINGS{JantzenZetzsche2008a,
AUTHOR = {Jantzen, Matthias and Zetzsche, Georg},
TITLE = {Labeled Step Sequences in Petri Nets},
BOOKTITLE = {Proc. of the International Conference on Applications and Theory of Petri nets (PETRI NETS 2008)},
ADDRESS = {Berlin Heidelberg},
YEAR = {2008},
PAGES = {270--287},
EDITOR = {van Hee, Kees M. and Valk, R{\"u}diger},
PUBLISHER = {Springer},
VOLUME = {5062},
SERIES = {LNCS},
DOI = {10.1007/978-3-540-68746-7_19}
}
Abstract
We study first-order logic (FO) over the structure consisting of finite words
over some alphabet~$A$, together with the (non-contiguous) subword ordering.
In terms of decidability of quantifier alternation fragments, this logic is
well-understood: If every word is available as a constant, then even the
$\Sigma_1$ (i.e., existential) fragment is undecidable, already for binary
alphabets $A$.
However, up to now, little is known about the expressiveness of the
quantifier alternation fragments: For example, the undecidability proof for
the existential fragment relies on Diophantine equations and only
shows that recursively enumerable languages over a singleton alphabet (and
some auxiliary predicates) are definable.
We show that if $|A|\ge 3$, then a relation is definable in the existential
fragment over $A$ with constants if and only if it is recursively enumerable.
This implies characterizations for all fragments~$\Sigma_i$: If $|A|\ge 3$,
then a relation is definable in $\Sigma_i$ if and only if it belongs to the
$i$-th level of the arithmetical hierarchy. In addition, our result yields
an analogous complete description of the $\Sigma_i$-fragments for $i\ge 2$ of
the \emph{pure logic}, where the words of $A^*$ are not available as
constants.
@ARTICLE{BaumannGanardiThinniyamZetzsche2023a,
AUTHOR = {Baumann, Pascal and Ganardi, Moses and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {Existential definability over the subword ordering},
YEAR = {2023},
JOURNAL = {Logical Methods in Computer Science},
VOLUME = {19},
DOI = {10.46298/lmcs-19(4:35)2023}
}
Abstract
We prove that the power word problem for certain metabelian subgroups of $GL(2,\mathbb{C})$ (including the
solvable Baumslag-Solitar groups $BS(1,q) = \langle a,t \mid t a t^{-1} = a^q \rangle$) belongs to the circuit complexity class
$TC^0$. In the power word problem, the input consists of group elements $g_1, \ldots, g_d$ and binary encoded integers
$n_1, \ldots, n_d$ and it is asked whether $g_1^{n_1} \cdots g_d^{n_d} = 1$ holds. Moreover, we prove that the knapsack problem
for $\BS(1,q)$ is $\NP$-complete. In the knapsack problem, the input consists of group elements $g_1, \ldots, g_d,h$
and it is asked whether the equation $g_1^{x_1} \cdots g_d^{x_d} = h$ has a solution in $\N^d$. For the more general case of a system
of so-called exponent equations, where the exponent variables $x_i$ can occur multiple times, we show that solvability is undecidable for
$BS(1,q)$.
@ARTICLE{GanardiLohreyZetzsche2023a,
AUTHOR = {Ganardi, Moses and Lohrey, Markus and Zetzsche, Georg},
TITLE = {Knapsack and the power word problem in Baumslag-Solitar Groups},
YEAR = {2023},
JOURNAL = {International Journal of Algebra and Computation},
VOLUME = {33},
PAGES = {617--639},
DOI = {10.1142/S0218196723500285}
}
Abstract
A knapsack equation in a group $G$ is an equation of the form $g_1^{x_1}\cdots g_k^{x_k}=g$, where $g_1,\ldots,g_k,g$ are elements of G and $x_1,\ldots,x_k$ are variables that take values in the natural numbers. We study the class of groups G for which all knapsack equations have effectively semilinear solution sets. We show that the following group constructions preserve effective semilinearity: graph products, amalgamated free products with finite amalgamated subgroups, HNN-extensions with finite associated subgroups, and finite extensions. Moreover, we study a complexity measure, called magnitude, of the resulting semilinear solution sets. More precisely, we are interested in the growth of the magnitude in terms of the length of the knapsack equation (measured in number of generators). We investigate how this growth changes under the above group operations.
@ARTICLE{FigeliusLohreyZetzsche2021a,
AUTHOR = {Figelius, Michael and Lohrey, Markus and Zetzsche, Georg},
TITLE = {Closure properties of knapsack semilinear groups},
JOURNAL = {Journal of Algebra},
VOLUME = {589},
YEAR = {2022},
PAGES = {437--482},
DOI = {10.1016/j.jalgebra.2021.08.016}
}
Abstract
This work studies which storage mechanisms in automata
permit decidability of the emptiness problem. The question
is formalized using valence automata, an abstract model of
automata in which the storage mechanism is given by a
monoid. For each of a variety of storage mechanisms, one
can choose a (typically infinite) monoid $M$ such that
valence automata over $M$ are equivalent to (one-way)
automata with this type of storage. In fact, many
important storage mechanisms can be realized by monoids
defined by finite graphs, called graph monoids. Examples
include pushdown stacks, partially blind counters (which
behave like Petri net places), blind counters (which may
attain negative values), and combinations thereof.
Hence, we study for which graph monoids the emptiness
problem for valence automata is decidable. A particular
model realized by graph monoids is that of Petri nets with
a pushdown stack. For these, decidability is a
long-standing open question and we do not answer it here.
However, if one excludes subgraphs corresponding to this
model, a characterization can be achieved. Moreover, we
provide a description of those storage mechanisms for
which decidability remains open. This leads to a model
that naturally generalizes both pushdown Petri nets and
the priority multicounter machines introduced by
Reinhardt.
The cases that are proven decidable constitute a natural
and apparently new extension of Petri nets with decidable
reachability. It is finally shown that this model can be
combined with another such extension by Atig and Ganty: We
present a further decidability result that subsumes both
of these Petri net extensions.
@ARTICLE{Zetzsche2021b,
AUTHOR = {Zetzsche, Georg},
TITLE = {The Emptiness Problem for Valence Automata over Graph Monoids},
YEAR = {2021},
JOURNAL = {Information and Computation},
VOLUME = {277},
DOI = {10.1016/j.ic.2020.104583}
}
Abstract
The model of asynchronous programming arises in many contexts, from low-level systems software to high-level web programming. We take a language-theoretic perspective and show general decidability and undecidability results for asynchronous programs that capture all known results as well as show decidability of new and important classes. As a main consequence, we show decidability of safety, termination and boundedness verification for higher-order asynchronous programs -- such as OCaml programs using Lwt -- and undecidability of liveness verification already for order-2 asynchronous programs. We show that under mild assumptions, surprisingly, safety and termination verification of asynchronous programs with handlers from a language class are decidable iff emptiness is decidable for the underlying language class. Moreover, we show that configuration reachability and liveness (fair termination) verification are equivalent, and decidability of these problems implies decidability of the well-known "equal-letters" problem on languages. Our results close the decidability frontier for asynchronous programs.
@ARTICLE{MajumdarThinniyamZetzsche2022a,
AUTHOR = {Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
TITLE = {General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond},
YEAR = {2022},
JOURNAL = {Logical Methods in Computer Science},
VOLUME = {18},
DOI = {10.46298/lmcs-18(4:2)2022}
}
Abstract
It is shown that the knapsack problem, which was introduced by Myasnikov et al.
for arbitrary finitely generated groups, can be solved in {\sf NP} for every graph
group. This result even holds if the group elements are represented in a
compressed form by so called straight-line programs, which generalizes the classical {\sf NP}-completeness
result of the integer knapsack problem. If group elements are represented explicitly
by words over the generators, then knapsack for a graph group belongs the class
{\sf LogCFL} (a subclass of {\sf P}) if the graph group can be built up from the trivial
group using the operations of free product and direct product with $\Z$. In all other cases,
the knapsack problem is {\sf NP}-complete.
@ARTICLE{LohreyZetzsche2017b,
AUTHOR = {Lohrey, Markus and Zetzsche, Georg},
TITLE = {Knapsack in Graph Groups},
YEAR = {2018},
JOURNAL = {Theory of Computing Systems},
VOLUME = {62},
PAGES = {192--246},
DOI = {10.1007/s00224-017-9808-3},
NOTE = {Combines papers at STACS 2016 {\&} 2017}
}
Abstract
We investigate the monoid of transformations that are induced by
sequences of writing to and reading from a queue storage. We describe
this monoid by means of a confluent and terminating semi-Thue system
and study some of its basic algebraic properties, e.g., conjugacy.
Moreover, we show that while several properties concerning its
rational subsets are undecidable, their uniform membership problem is
NL-complete. Furthermore, we present an algebraic characterization of
this monoid's recognizable subsets. Finally, we prove that it is not
Thurston-automatic.
@ARTICLE{HuschenbettKuskeZetzsche2017a,
AUTHOR = {Huschenbett, Martin and Kuske, Dietrich and Zetzsche, Georg},
TITLE = {The Monoid of Queue Actions},
YEAR = {2017},
JOURNAL = {Semigroup Forum},
VOLUME = {95},
PAGES = {475--508},
DOI = {10.1007/s00233-016-9835-4}
}
Abstract
The separability problem for word languages of a class $\C$ by languages of
a class $\S$ asks, for two given languages $I$ and $E$ from $\C$, whether
there exists a language $S$ from $\S$ that includes $I$ and excludes $E$,
that is, $I \subseteq S$ and $S\cap E = \emptyset$. In this work, we assume
some mild closure properties for $\C$ and study for which such classes $\C$,
separability by piecewise testable languages (PTL) is decidable. We
characterize these classes in terms of decidability of (two variants of) an
unboundedness problem. From this we deduce that separability by PTL is
decidable for a number of language classes, such as the context-free
languages and languages of labeled vector addition systems. Furthermore, it
follows that separability by PTL is decidable if and only if one can compute
for any language of the class its downward closure wrt.\ the \subword
ordering (i.e., if the set of \subwords of any language of the class
is effectively regular).
The obtained decidability results contrast some undecidability
results. In fact, for all the (non-regular) language classes we
present as examples with decidable separability, it is undecidable
whether a given language is a PTL itself.
Our characterization involves a result of independent interest,
which states that for \emph{any} kind of languages $I$ and $E$,
non-separability is equivalent to the existence of common patterns
in $I$ and $E$.
@ARTICLE{CzerwinskiMartensRooijenZeitounZetzsche2017a,
AUTHOR = {Czerwi{\'{n}}ski, Wojciech and Martens, Wim and van Rooijen, Lorijn and Zeitoun, Marc and Zetzsche, Georg},
TITLE = {A Characterization for Decidable Separability by Piecewise Testable Languages},
YEAR = {2017},
JOURNAL = {Discrete Mathematics and Theoretical Computer Science},
VOLUME = {19},
NUMBER = {4},
YEAR = {2017},
DOI = {10.23638/DMTCS-19-4-1}
}
Abstract
We study what languages can be constructed from a non-regular
language $L$ using Boolean operations and (synchronized) rational
transductions. If all rational transductions are allowed, one can
construct the whole arithemtical hierarchy relative to $L$. If only
synchronized rational transductions are allowed, we present
non-regular languages that allow to construct at least languages
arbitrarily high in the arithmetical hierarchy and we present
non-regular languages that allow to construct only decidable
languages.
A consequence of the results is that aside from the regular
languages, no full trio generated by a single language is closed under
complementation.
Our construction also shows that there is a fixed rational Kripke
frame such that assigning an arbitrary non-regular language to some
variable allows the definition of any language from the arithmetical
hierarchy in the corresponding Kripke structure using multimodal
logic.
@ARTICLE{ZetzscheKuskeLohrey2017a,
AUTHOR = {Zetzsche, Georg and Kuske, Dietrich and Lohrey, Markus},
TITLE = {On {Boolean} closed full trios and rational {Kripke} frames},
VOLUME = {60},
PAGES = {438--472},
YEAR = {2017},
JOURNAL = {Theory of Computing Systems},
DOI = {10.1007/s00224-016-9694-0}
}
Monoids as Storage Mechanisms
Bulletin of the EATCS 120, 2016 [ Show BibTeXHide BibTeX
]
@ARTICLE{Zetzsche2016d,
AUTHOR = {Zetzsche, Georg},
TITLE = {Monoids as Storage Mechanisms},
YEAR = {2016},
JOURNAL = {Bulletin of the EATCS},
VOLUME = {120},
PAGES = {237--249},
NOTE = {Invited abstract due to EATCS Distinguished Dissertation Award}
}
Abstract
For a language $L$, we consider its cyclic closure, and more generally the
language $C^k(L)$, which consists of all words obtained by partitioning words
from $L$ into $k$ factors and permuting them. We prove that the classes of
ET0L and EDT0L languages are closed under the operators $C^k$. This both
sharpens and generalises Brandstädt's result that if $L$ is context-free then
$C^k(L)$ is context-sensitive and not context-free in general for $k\geq 3$.
We also show that the cyclic closure of an indexed language is indexed.
@ARTICLE{BroughCiobanuElderZetzsche2016a,
AUTHOR = {Brough, Tara and Ciobanu, Laura and Elder, Murray and Zetzsche, Georg},
TITLE = {Permutations of context-free, ET0L and indexed languages},
YEAR = {2016},
JOURNAL = {Discrete Mathematics and Theoretical Computer Science},
VOLUME = {17},
NUMBER = {3},
YEAR = {2016},
PAGES = {167--178}
}
Abstract
It is shown that membership in rational subsets of wreath
products $H \wr V$ with $H$ a finite group and $V$ a virtually
free group is decidable. On the other hand, it is shown that
there exists a fixed finitely generated submonoid in the wreath
product $\mathbb{Z}\wr\mathbb{Z}$ with an undecidable
membership problem.
@ARTICLE{LohreySteinbergZetzsche2015a,
AUTHOR = {Lohrey, Markus and Steinberg, Benjamin and Zetzsche, Georg},
TITLE = {Rational subsets and submonoids of wreath products},
JOURNAL = {Information and Computation},
VOLUME = {243},
PAGES = {191--204},
YEAR = {2015},
DOI = {10.1016/j.ic.2014.12.014}
}
Toward Understanding the Generative Capacity of Erasing Rules in Matrix Grammars
International Journal of Foundations of Computer Science 22(2), 2011
Special Issue on DLT 2009 [ Show BibTeXHide BibTeX
| Show abstractHide abstract
| DOI ]
Abstract
This article presents approaches to the open problem of whether erasing
rules can be eliminated in matrix grammars. The class of languages
generated by non-erasing matrix grammars is characterized by the newly
introduced linear Petri net grammars. Petri net grammars are known to be
equivalent to arbitrary matrix grammars (without appearance checking). In
linear Petri net grammars, the marking has to be linear in size with
respect to the length of the sentential form. The characterization by
linear Petri net grammars is then used to show that applying linear erasing
to a Petri net language yields a language generated by a non-erasing matrix
grammar. It is also shown that in Petri net grammars (with final markings
and arbitrary labeling), erasing rules can be eliminated, which yields two
reformulations of the problem of whether erasing rules in matrix grammars
can be eliminated.
@ARTICLE{Zetzsche2011a,
AUTHOR = {Zetzsche, Georg},
TITLE = {Toward Understanding the Generative Capacity of Erasing Rules in Matrix Grammars},
JOURNAL = {International Journal of Foundations of Computer Science},
VOLUME = {22},
NUMBER = {2},
PAGES = {411--426},
YEAR = {2011},
DOI = {10.1142/S0129054111008118}
}
Abstract
The previously introduced multiset language classes
defined by multiset pushdown automata are being
explored with respect to their closure properties and
alternative characterizations.
@ARTICLE{KudlekTotzkeZetzsche2009a,
AUTHOR = {Kudlek, Manfred and Totzke, Patrick and Zetzsche, Georg},
TITLE = {Properties of Multiset Language Classes Defined by Multiset Pushdown Automata},
JOURNAL = {Fundamenta Informaticae},
VOLUME = {93},
PAGES = {235--244},
NUMBER = {1-3},
YEAR = {2009},
DOI = {10.3233/FI-2009-0099}
}
Abstract
Multiset finite Automata, a model equivalent to
regular commutative grammars, are extended with a
multiset store and the accepting power of this
extended model of computation is investigated. This
type of multiset automata come in two flavours,
varying only in the ability of testing the storage
for emptiness. This paper establishes normal forms
and relates the derived language classes to each
other as well as to known multiset language classes.
@ARTICLE{KudlekTotzkeZetzsche2009,
AUTHOR = {Kudlek, Manfred and Totzke, Patrick and Zetzsche, Georg},
TITLE = {Multiset Pushdown Automata},
JOURNAL = {Fundamenta Informaticae},
VOLUME = {93},
PAGES = {221--233},
NUMBER = {1-3},
YEAR = {2009},
DOI = {10.3233/FI-2009-0098}
}
Abstract
We present a generalization of finite automata using
Petri nets as control, called Concurrent Finite Automata
for short. Several modes of acceptance, defined by final
markings of the Petri net, are introduced, and their
equivalence is shown. The class of languages obtained by
l-free concurrent finite automata contains both the class
of regular sets and the class of Petri net languages
defined by final marking, and is contained in the class
of context-sensitive languages.
@ARTICLE{FaJaKuRoZe2008,
AUTHOR = {Farwer, Berndt and Jantzen, Matthias and Kudlek, Manfred and R{\"o}lke, Heiko and Zetzsche, Georg},
TITLE = {Petri Net Controlled Finite Automata},
JOURNAL = {Fundamenta Informaticae},
VOLUME = {85},
PAGES = {111--121},
NUMBER = {1-4},
YEAR = {2008}
}
Abstract
This paper presents results regarding the various
relations among the language classes defined by
Concurrent Finite Automata, relations to other language
classes, as well as decidability and closure properties.
@ARTICLE{JantzenKudlekZetzsche2008,
AUTHOR = {Jantzen, Matthias and Kudlek, Manfred and Zetzsche, Georg},
TITLE = {Language Classes Defined by Concurrent Finite Automata},
JOURNAL = {Fundamenta Informaticae},
VOLUME = {85},
PAGES = {267--280},
NUMBER = {1-4},
YEAR = {2008}
}
Abstract
Two kinds of multiset automata with a storage attached, varying
only in their ability of testing the storage for emptiness, are
introduced, as well as normal forms. Their accepting power and
relation to other multiset languages classes is investigated.
@INPROCEEDINGS{KudlekTotzkeZetzsche2008,
AUTHOR = {Kudlek, Manfred and Totzke, Patrick and Zetzsche, Georg},
TITLE = {Multiset Storage Automata},
BOOKTITLE = {Proc. of the Workshop on Concurrency, Specification and Programming (CS{\&}P 2008)},
EDITOR = {Burkhard, H.-D. and Czaja, Ludwik and Lindemann, G. and Skowron, A.},
VOLUME = {2},
PAGES = {265--277},
YEAR = {2008}
}
Abstract
The previously introduced multiset language classes defined by
multiset storage automata are being explored with respect to their
closure properties and alternative characterizations.
@INPROCEEDINGS{KudlekTotzkeZetzsche2008a,
AUTHOR = {Kudlek, Manfred and Totzke, Patrick and Zetzsche, Georg},
TITLE = {Properties of Multiset Language Classes Defined by Multiset Storage Automata},
BOOKTITLE = {Proc. of the Workshop on Concurrency, Specification and Programming (CS{\&}P 2008)},
EDITOR = {Burkhard, H.-D. and Czaja, Ludwik and Lindemann, G. and Skowron, A.},
VOLUME = {2},
PAGES = {278--288},
YEAR = {2008}
}
@INPROCEEDINGS{KudlekZetzsche2010,
AUTHOR = {Kudlek, Manfred and Zetzsche, Georg},
TITLE = {Concurrent finite automata and related language classes (an overview)},
BOOKTITLE = {Proc. of the Workshop Automata, Formal Languages and Algebraic Systems (AFLAS 2008)},
YEAR = {2010},
EDITOR = {Ito, Masami and Kobayashi, Yuji and Kunitaka, Shoji},
PUBLISHER = {World Scientific},
ADDRESS = {New Jersey},
PAGES = {103--113},
DOI = {10.1142/9789814317610_0008}
}
@INPROCEEDINGS{FaJaKuRoZe2007,
AUTHOR = {Farwer, Berndt and Jantzen, Matthias and Kudlek, Manfred and R{\"o}lke, Heiko and Zetzsche, Georg},
TITLE = {On Concurrent Finite Automata},
BOOKTITLE = {Proc. of the Workshop on Concurrency, Specification and Programming (CS{\&}P 2007)},
EDITOR = {Czaja, Ludwik},
VOLUME = {1},
PAGES = {180--190},
YEAR = {2007}
}
@INPROCEEDINGS{JantzenKudlekZetzsche2007a,
AUTHOR = {Jantzen, Matthias and Kudlek, Manfred and Zetzsche, Georg},
TITLE = {On Languages Accepted by Concurrent Finite Automata},
BOOKTITLE = {Proc. of the Workshop on Concurrency, Specification and Programming (CS{\&}P 2007)},
EDITOR = {Czaja, Ludwik},
VOLUME = {2},
PAGES = {321--332},
YEAR = {2007}
}
Abstract
Automata theory has given rise to a variety of automata models that consist of
a finite-state control and an infinite-state storage mechanism. The aim of
this work is to provide insights into how the structure of the storage
mechanism influences the expressiveness and the analyzability of the resulting
model. To this end, it presents generalizations of results about individual
storage mechanisms to larger classes. These
generalizations characterize those storage mechanisms for which the given
result remains true and for which it fails.
In order to speak of classes of storage mechanisms, we need an overarching
framework that accommodates each of the concrete storage mechanisms we wish to
address. Such a framework is provided by the model of valence automata,
in which the storage mechanism is represented by a monoid.
Since the monoid serves as a parameter to specifying the storage mechanism, our
aim translates into the question: For which monoids does the given
(automata-theoretic) result hold?
As a first result, we present an algebraic characterization of those monoids
over which valence automata accept only regular languages. In addition,
it turns out that for each monoid, this is the case if and only if
valence grammars, an analogous grammar model, can generate only
context-free languages.
Furthermore, we are concerned with closure properties: We study which monoids
result in a Boolean closed language class.
For every language class that is closed under rational transductions (in
particular, those induced by valence automata), we show: If the class is Boolean
closed and contains any non-regular language, then it already includes the
whole arithmetical hierarchy.
This work also introduces the class of graph monoids, which are defined
by finite graphs. By choosing appropriate graphs, one can realize a number of
prominent storage mechanisms, but also combinations and variants thereof.
Examples are pushdowns, counters, and Turing tapes. We can therefore relate
the structure of the graphs to computational properties of the resulting
storage mechanisms.
In the case of graph monoids, we study (i) the
decidability of the emptiness problem, (ii) which storage mechanisms
guarantee semilinear Parikh images, (iii) when silent transitions
(i.e. those that read no input) can be avoided, and (iv) which storage
mechanisms permit the computation of downward closures.
@PHDTHESIS{Zetzsche2016c,
AUTHOR = {Zetzsche, Georg},
TITLE = {Monoids as Storage Mechanisms},
TYPE = {PhD thesis},
INSTITUTION = {Technische Universit{\"a}t Kaiserslautern},
YEAR = {2016}
}
Abstract
A successful idea in the area of verification is to
consider finite-state abstractions of infinite-state
systems. A prominent example is the fact that many
language classes satisfy a Parikh's theorem, i.e. for
each language, there exists a finite automaton that
accepts the same language up to the order of letters.
Hence, provided that the abstraction preserves
pertinent properties, this allows us to work with
finite-state systems, which are much easier to handle.
While Parikh-style abstractions have been studied very
intensely over the last decades, recent years have
seen an increasing interest in abstractions based on
the subword ordering. Examples include the set of (non
necessarily contiguous) subwords of members of a
language (the downward closure), or their superwords
(the upward closure). Whereas it is well-known that
these closures are regular for any language, it is
often not obvious how to compute them. Another type
of subword based abstractions are piecewise testable
separators. Here, a separators acts as an abstraction
of a pair of languages.
This talk will present approaches to computing
closures, deciding separability by piecewise testable
languages, and a (perhaps surprising) connection
between these problems. If time permits, complexity
issues will be discussed as well.
Abstract
It is shown that the knapsack problem, which was introduced by Myasnikov et al.
for arbitrary finitely generated groups, can be solved in NP for graph
groups. This result even holds if the group elements are represented in a
compressed form by SLPs, which generalizes the classical NP-completeness
result of the integer knapsack problem. We also prove general transfer results:
NP-membership of the knapsack problem is passed on to finite
extensions, HNN-extensions over finite associated subgroups, and amalgamated
products with finite identified subgroups.
Abstract
For each grammar model with regulated rewriting, it is an important question
whether erasing productions add to its expressivity. In some cases, however,
this has been a longstanding open problem.
In recent years,
several results have been obtained that clarified the generative capacity of erasing
productions in some grammar models with classical types of regulated rewriting.
The aim of this talk is to give an overview of these results.
Abstract
Reachability problems in infinite-state systems are often subject to extremely
high complexity.
This motivates the investigation of efficient overapproximations, where we add transitions to
obtain a system in which reachability can be decided more easily. We consider
bidirected infinite-state systems, where for every transition there is a
transition with opposite effect. We study bidirected reachability in the
framework of valence systems, an abstract model featuring finitely many control
states and an infinite-state storage that is specified by a finite graph.
By picking suitable graphs, valence systems can uniformly model counters as in vector addition systems,
pushdowns, integer counters, and combinations thereof.
We provide a comprehensive complexity landscape for bidirected reachability and show that
the complexity drops substantially (often to polynomial
time) from that of general reachability, for almost every storage mechanism
where reachability is known to be decidable.
Context-bounded verification of liveness properties for multithreaded shared-memory programs
Given at Seminar "Méthodes Formelles" at LaBRI in Bordeaux, France
Rational Subsets of Baumslag-Solitar Groups
Given at Seminar on Semigroups, Automata and Languages at Centro de Matemática, Universidade do Porto in Porto, Portugal
Rational Subsets of Baumslag-Solitar Groups
Given at Göttingen-Kassel Theory (Online) Seminar
Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets
(joint work with Sylvain Schmitz)
Given at RP 2019 in Brussels, Belgium [ Show abstractHide abstract
]
Abstract
We consider the model of pushdown vector addition systems with
resets. These consist of vector addition systems that have access
to a pushdown stack and have instructions to reset counters. For
this model, we study the coverability problem. In the absence of
resets, this problem is known to be decidable for one-dimensional
pushdown vector addition systems, but decidability is open for
general pushdown vector addition systems. Moreover, coverability
is known to be decidable for reset vector addition systems without
a pushdown stack. We show in this note that the problem is
undecidable for one-dimensional pushdown vector addition systems
with resets.
Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
Given at Highlights 2019 in Warsaw, Poland
Separability by piecewise testable languages and downward closures beyond subwords
Given at LICS 2018 in Oxford, United Kingdom [ Show abstractHide abstract
]
Abstract
We introduce a flexible class of well-quasi-orderings (WQOs) on
words that generalizes the ordering of (not necessarily contiguous)
subwords.
Each such WQO induces a class of piecewise testable languages (PTLs)
as Boolean combinations of upward closed sets. In this way, a range
of regular language classes arises as PTLs. Moreover, each of the
WQOs guarantees regularity of all downward closed sets.
We consider two problems. First, we study which (perhaps
non-regular) language classes allow to decide whether two given
languages are separable by a PTL with respect to a given
WQO. Second, we want to effectively compute downward closures with
respect to these WQOs.
Our first main result is that for each of the WQOs, under mild
assumptions, both problems reduce to the simultaneous unboundedness
problem (SUP) and are thus solvable for many powerful system
models. In the second main result, we apply the framework to show
decidability of separability of regular languages by
$\mathcal{B}\Sigma_1[<, \mathsf{mod}]$, a fragment of
first-order logic with modular predicates.
Storage mechanisms and finite-state abstractions for software verification
Given at MPI-SWS Colloquium in Kaiserslautern, Germany
Storage mechanisms and finite-state abstractions for software verification
Given at Kolloquium Technische Universität Kaiserslautern in Germany
Parameterized WQOs, downward closures, and separability problems
Given at Workshop on Separability Problems in Warsaw, Poland [ Show abstractHide abstract
]
Abstract
We discuss a flexible class of well-quasi-orderings on words
that generalizes the ordering of (not necessarily contiguous)
subwords. Each of these orderings is specified by a finite
automaton or a counter automaton and, like the subword ordering,
guarantees regularity of all downward (or upward) closures.
We then consider two problems. First, we study for which language
classes one can effectively compute downward closures with
respect to these orderings. Second, we are interested in which
language classes permit a decision procedure to decide whether
two given languages are separable by a PTL with respect to such
an ordering. Here, a PTL is a finite Boolean combination of
upward closed sets.
The main result is that, under mild assumptions on closure
properties, these two problems are solvable for the same language
classes. Moreover, solvability is equivalent to that of a
particular unboundedness problem that has recently been shown to
be decidable for many powerful language classes.
Abstract
This talk reports on results concerning first-order logic over
the subword ordering on finite words. It has been known since
2006 that the whole first-order logic over this structure is
undecidable, whereas the Sigma_1 fragment is NP-complete.
One might therefore expect that introducing each word as a
constant would leave the Sigma_1 fragment decidable. However,
it was shown recently that in the presence of these constants,
the \Sigma_1 theory becomes undecidable (already over two
letters).
Regarding the decidability border, we will consider fragments
where all but a certain number of variables are alternation
bounded, meaning that the variable must always be quantified over
languages with a bounded number of letter alternations. Here,
the second result is that when at most two variables are not
alternation bounded, the \Sigma_1 fragment is decidable, and that
it becomes undecidable when three variables are not alternation
bounded. Concerning higher quantifier alternation depths, the
\Sigma_2 fragment is undecidable already for one variable without
alternation bound and that when all variables are alternation
bounded, the entire first-order theory is decidable.
If time permits, complexity aspects will be treated as well.
This is joint work with Simon Halfon and Philippe Schnoebelen (to be
presented at LICS 2017).
Monoids as Storage Mechanisms
Given at Kasseler Informatik-Kolloquium, Universität Kassel in Germany [ Show abstractHide abstract
]
Abstract
The investigation of models extending finite automata by some
storage mechanism is a central theme in theoretical computer
science. Choosing an appropriate storage mechanism can yield a
model that is expressive enough to capture a given behavioral
aspect while admitting desired means of analysis.
It is therefore a central concern to understand which storage
mechanisms have which properties regarding expressiveness and
(algorithmic) analysis. This talk presents a line of research
that aims for general insights in this direction. In other words:
How does the structure of the storage mechanism influence
expressiveness and analysis of the resulting model?
In order to study this question, one needs a model in which the
storage mechanism appears as a parameter. Such a model is
available in valence automata, where the storage mechanism is
given by a (typically infinite) monoid. Choosing a suitable
monoid then yields models such as Turing machines, pushdown
automata, vector addition systems, or combinations thereof.
This talk surveys a selection of results that characterize
storage mechanisms with certain desirable properties, such as
decidability of reachability, semilinearity of Parikh images, and
decidability of logics.
Abstract
Myasnikov et al. have introduced the knapsack problem for arbitrary finitely
generated groups. In previous work, the authors proved that for each graph
group, the knapsack problem can be solved in NP. Here, we determine the
exact complexity of the problem for every graph group. While the problem is
TC0-complete for complete graphs, it is LogCFL-complete for each
(non-complete) transitive forest. For every remaining graph, the problem is
NP-complete.
Abstract
First-order logic with the reachability predicate (FOR)
is an important means of specification in system analysis.
Its decidability status is known for some individual
types of infinite-state systems such as pushdown (decidable)
and vector addition systems (undecidable).
This work aims at a general understanding of which types of
systems admit decidability. As a unifying model, we employ
valence systems over graph monoids, which feature a
finite-state control and are parameterized by a monoid to
represent their storage mechanism. As special cases, this
includes pushdown systems, various types of counter systems
(such as vector addition systems) and combinations thereof.
Our main result is a characterization of those
graph monoids where FOR is decidable for the resulting
transition systems.
Subword Based Abstractions of Formal Languages
Given at Seminar "Méthodes Formelles" at LaBRI in Bordeaux, France [ Show abstractHide abstract
]
Abstract
A successful idea in the area of verification is to
consider finite-state abstractions of infinite-state
systems. A prominent example is the fact that many
language classes satisfy a Parikh's theorem, i.e. for
each language, there exists a finite automaton that
accepts the same language up to the order of letters.
Hence, provided that the abstraction preserves
pertinent properties, this allows us to work with
finite-state systems, which are much easier to handle.
While Parikh-style abstractions have been studied very
intensely over the last decades, recent years have
seen an increasing interest in abstractions based on
the subword ordering. Examples include the set of (non
necessarily contiguous) subwords of members of a
language (the downward closure), or their superwords
(the upward closure). Whereas it is well-known that
these closures are regular for any language, it is
often not obvious how to compute them. Another type
of subword based abstractions are piecewise testable
separators. Here, a separators acts as an abstraction
of a pair of languages.
This talk will present approaches to computing
closures, deciding separability by piecewise testable
languages, and a (perhaps surprising) connection
between these problems. If time permits, complexity
issues will be discussed as well.
Subword Based Abstractions of Formal Languages
Given at Seminar "Automates et applications" at IRIF in Paris, France [ Show abstractHide abstract
]
Abstract
A successful idea in the area of verification is to
consider finite-state abstractions of infinite-state
systems. A prominent example is the fact that many
language classes satisfy a Parikh's theorem, i.e. for
each language, there exists a finite automaton that
accepts the same language up to the order of letters.
Hence, provided that the abstraction preserves
pertinent properties, this allows us to work with
finite-state systems, which are much easier to handle.
While Parikh-style abstractions have been studied very
intensely over the last decades, recent years have
seen an increasing interest in abstractions based on
the subword ordering. Examples include the set of (non
necessarily contiguous) subwords of members of a
language (the downward closure), or their superwords
(the upward closure). Whereas it is well-known that
these closures are regular for any language, it is
often not obvious how to compute them. Another type
of subword based abstractions are piecewise testable
separators. Here, a separators acts as an abstraction
of a pair of languages.
This talk will present approaches to computing
closures, deciding separability by piecewise testable
languages, and a (perhaps surprising) connection
between these problems. If time permits, complexity
issues will be discussed as well.
Abstract
First-order logic with the reachability predicate (FOR)
is an important means of specification in system analysis.
Its decidability status is known for some individual
types of infinite-state systems such as pushdown (decidable)
and vector addition systems (undecidable).
This work aims at a general understanding of which types of
systems admit decidability. As a unifying model, we employ
valence systems over graph monoids, which feature a
finite-state control and are parameterized by a monoid to
represent their storage mechanism. As special cases, this
includes pushdown systems, various types of counter systems
(such as vector addition systems) and combinations thereof.
Our main result is a characterization of those
graph monoids where FOR is decidable for the resulting
transition systems.
Monoids as Storage Mechanisms
Given at Theory Seminar at the National University of Singapore [ Show abstractHide abstract
]
Abstract
The investigation of models extending finite automata by some
storage mechanism is a central theme in theoretical computer
science. Choosing an appropriate storage mechanism can yield a
model that is expressive enough to capture a given behavioral
aspect while admitting desired means of analysis.
It is therefore a central concern to understand which storage
mechanisms have which properties regarding expressiveness and
(algorithmic) analysis. This talk presents a line of research
that aims for general insights in this direction. In other words:
How does the structure of the storage mechanism influence
expressiveness and analysis of the resulting model?
In order to study this question, one needs a model in which the
storage mechanism appears as a parameter. Such a model is
available in valence automata, where the storage mechanism is
given by a (typically infinite) monoid. Choosing a suitable
monoid then yields models such as Turing machines, pushdown
automata, vector addition systems, or combinations thereof.
This talk surveys a selection of results that characterize
storage mechanisms with certain desirable properties, such as
decidability of reachability, semilinearity of Parikh images, and
decidability of logics.
Monoids as Storage Mechanisms
Given at Communicating, Distributed and Parameterized Systems in Singapore [ Show abstractHide abstract
]
Abstract
The investigation of models extending finite automata by some
storage mechanism is a central theme in theoretical computer
science. Choosing an appropriate storage mechanism can yield a
model that is expressive enough to capture a given behavioral
aspect while admitting desired means of analysis.
It is therefore a central concern to understand which storage
mechanisms have which properties regarding expressiveness and
(algorithmic) analysis. This talk presents a line of research
that aims for general insights in this direction. In other
words: How does the structure of the storage mechanism
influence expressiveness and analysis of the resulting model?
In order to study this question, one needs a model in which the
storage mechanism appears as a parameter. Such a model is
available in valence automata, where the storage mechanism is
given by a (typically infinite) monoid. Choosing a suitable
monoid then yields models such as Turing machines, pushdown
automata, vector addition systems, or combinations thereof.
This talk surveys a selection of results that characterize
storage mechanisms with certain desirable properties, such as
decidability of reachability, semilinearity of Parikh images,
and decidability of logics.
Abstract
The downward closure of a language is the set of all (not necessarily
contiguous) subwords of its members. It is well-known that the downward
closure of every language is regular. Moreover, recent results show
that downward closures are computable for quite powerful system models.
One advantage of abstracting a language by its downward closure is that then,
equivalence and inclusion become decidable. In this work, we study the
complexity of these two problems. More precisely, we consider the following
decision problems: Given languages $K$ and $L$ from classes $\C$ and $\D$,
respectively, does the downward closure of $K$ include (equal) that of $L$?
These problems are investigated for finite automata, one-counter automata,
context-free grammars, and reversal-bounded counter automata. For each
combination, we prove a completeness result either for fixed or for arbitrary
alphabets. Moreover, for Petri net languages, we show that both problems are
Ackermann-hard and for higher-order pushdown automata of order $k$, we prove
hardness for complements of nondeterministic $k$-fold exponential time.
Abstract
It is a well-known phenomenon that languages classes induced
by infinite-state systems usually lack decidability and
closure properties that make regular languages pleasant to
analyze. Most notably, nondeterministic infinite-state
systems typically fail to be closed under Boolean
operations. In visibly pushdown automata, one has closure
under Boolean operations, but at the expense of restricting
the employed input alphabets, meaning they are not closed
under rational transductions.
This raises the question of whether there is some type of
infinite-state system that enjoys closure under Boolean
operations and rational transductions (and permits
decidability of, say, the emptiness problem). This talk
demonstrates that this is not the case. It is shown that
every language class that contains any non-regular language
and is closed under Boolean operations and rational
transductions already contains the whole arithmetic
hierarchy (which significantly extends the recursively
enumerable languages).
Abstract
The downward closure of a language is the set of all (not
necessarily contiguous) subwords of its members. It is
well-known that the downward closure of every language is
regular. One advantage of abstracting a language by its
downward closure is that then, equivalence and inclusion
become decidable.
It has recently been shown by Hague, Kochems, and Ong that
downward closures are computable for higher-order pushdown
automata. However, the current method yields no upper bound
on the complexity of such a computation. This talk will
present recent results on complexity issues surrounding
downward closures. Aside from general algorithms and
possible approaches to obtain upper bounds in the case of
HOPA, we will discuss a lower bound result for the
abovementioned equivalence and inclusion problem for HOPA.
Abstract
It is shown that the knapsack problem, which was introduced by Myasnikov et al.
for arbitrary finitely generated groups, can be solved in NP for graph
groups. This result even holds if the group elements are represented in a
compressed form by SLPs, which generalizes the classical NP-completeness
result of the integer knapsack problem. We also prove general transfer results:
NP-membership of the knapsack problem is passed on to finite
extensions, HNN-extensions over finite associated subgroups, and amalgamated
products with finite identified subgroups.
Monoids as Storage Mechanisms
Given at Seminar of the INFINI group at LSV in December 2015 in Cachan, France [ Show abstractHide abstract
| Slides ]
Abstract
The investigation of models extending finite automata by some storage mechanism
is a central theme in theoretical computer science. Choosing an appropriate
storage mechanism can yield a model that is expressive enough to capture a
given behavioral aspect while admitting desired means of analysis.
It is therefore a central concern to understand which storage mechanisms have
which properties regarding expressiveness and (algorithmic) analysis. This
talk presents a line of research that aims for general insights in this
direction. In other words: How does the structure of the storage mechanism
influences expressiveness and analysis of the resulting model?
In order to study this question, one needs a model in which the storage
mechanism appears as a parameter. Such a model is available in valence
automata, where the storage mechanism is given by a (typically infinite)
monoid. Choosing a suitable monoid then yields models such as Turing machines,
pushdown automata, vector addition systems, or combinations thereof.
This talk surveys a selection of results that characterize storage mechanisms
with certain desirable properties, such as deciability of reachability,
semilinearity of Parikh images, and avoidability of epsilon-transitions.
Abstract
The downward closure of a word language is the set of all (not necessarily
contiguous) subwords of its members. It is known that the downward closure of
every language is regular. However, algorithms for computing a finite automaton
for the downward closure of a given language are known only for few language
classes. This work presents a simple general approach to this problem. It is
used to prove that downward closures are computable for (i)~every language
class with effectively semilinear Parikh images that is closed under rational
transductions, (ii)~matrix languages, and (iii)~indexed languages
(equivalently, languages accepted by higher-order pushdown automata of
order~2).
The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets
Given at RP 2015 in Warsaw, Poland [ Show abstractHide abstract
| Slides ]
Abstract
This work studies which storage mechanisms in automata permit
decidability of the reachability problem. The question is formalized
using valence automata, an abstract model that generalizes automata with
storage. For each of a variety of storage mechanisms, one can choose a
(typically infinite) monoid $M$ such that valence automata over $M$ are
equivalent to (one-way) automata with this type of storage.
In fact, many interesting storage mechanisms can be realized by monoids defined
by finite graphs, called graph monoids. Hence, we study for which graph
monoids the emptiness problem for valence automata is decidable. A particular
model realized by graph monoids is that of Petri nets with a pushdown stack.
For these, decidability is a long-standing open question and we do not answer
it here.
However, if one excludes subgraphs corresponding to this model, a
characterization can be achieved. This characterization yields a new extension
of Petri nets with a decidable reachability problem. Moreover, we provide a
description of those storage mechanisms for which decidability remains open.
This leads to a natural model that generalizes both pushdown Petri nets and
priority multicounter machines.
Abstract
The downward closure of a word language is the set
of all (not necessarily contiguous) subwords of its
members. It is well-known that the downward closure of
any language is regular. While the downward closure
appears to be a powerful abstraction, algorithms for
computing a finite automaton for the downward closure
of a given language have been established only for few
language classes.
This work presents a simple general method for computing
downward closures. For language classes that are closed
under rational transductions, it is shown that the
computation of downward closures can be reduced to
checking a certain unboundedness property.
This result is used to prove that downward closures
are computable for (i) every language class with
effectively semilinear Parikh images that are closed
under rational transductions, (ii) matrix languages,
and (iii) indexed languages (equivalently, languages
accepted by higher-order pushdown automata of order~2).
Downward Closures of Indexed Languages
Given at HOPA 2015 in Kyoto, Japan [ Slides ]
Abstract
The downward closure of a language $L$ of words is the set of all (not
necessarily contiguous) subwords of members of $L$. It is well known that the
downward closure of any language is regular. Although the downward
closure seems to be a promising abstraction, there are only few language
classes for which an automaton for the downward closure is known to be
computable.
It is shown here that for stacked counter automata, the downward closure is
computable. Stacked counter automata are finite automata with a storage
mechanism obtained by \emph{adding blind counters} and \emph{building stacks}.
Hence, they generalize pushdown and blind counter automata.
The class of languages accepted by these automata are precisely those in the
hierarchy obtained from the context-free languages by alternating two closure
operators: imposing semilinear constraints and taking the algebraic extension.
The main tool for computing downward closures is the new concept of Parikh
annotations. As a second application of Parikh annotations, it is shown that
the hierarchy above is strict at every level.
Effectively regular downward closures
Given at LSV Seminar at ENS Cachan in Cachan, France [ Show abstractHide abstract
| Slides ]
Abstract
The downward closure of a language is the set of all (not
necessarily contiguous) subwords of its members. It is a
well-known consequence of Higman's Lemma that the downward
closure of every language is regular.
Aside from encoding interesting counting properties, the
downward closure constitutes a promising abstraction: If L is
the set of action sequences of a system, then the downward
closure of L is precisely what is observed through a lossy
channel, i.e. when actions can go unnoticed arbitrarily. Hence,
if the downward closure is available as a regular language,
the equivalence and even inclusion of system behaviors can be
decided with respect to such observations.
However, there are only few classes of languages for which it is
known how to compute the downward closure of a given language as
a finite automaton. This talk presents new approaches to this
problem.
Expressiveness and analysis of valence automata over graph monoids
Given at FORMAT Workshop 07/2014 in Kaiserslautern, Germany [ Slides ]
Abstract
Recent work on automata with abstract storage revealed a class of
storage mechanisms that proves quite expressive and amenable to various
kinds of algorithmic analysis. The storage mechanisms in this class are
obtained by \emph{building stacks} and \emph{adding blind counters}.
The former is to construct a new mechanism that stores a stack whose
entries are configurations of an old mechanism. One can then manipulate
the topmost entry, pop it if empty, or start a new one on top. Adding a
blind counter to an old mechanism yields a new mechanism in which the
old one and a blind counter can be used simultaneously. We call the
resulting model \emph{stacked counter automaton}.
This talk presents results on expressivity, Parikh images, membership
problems, and the computability of downward closures.
Abstract
A Boolean closed full trio is a class of languages that is closed under the
Boolean operations (union, intersection, and complementation) and rational
transductions. It is well-known that the regular languages constitute such a
Boolean closed full trio. It is shown here that every such language class that
contains any non-regular language already includes the whole arithmetical
hierarchy (and even the one relative to this language).
A consequence of this result is that aside from the regular languages, no full
trio generated by one language is closed under complementation.
Our construction also shows that there is a fixed rational Kripke frame such
that assigning an arbitrary non-regular language to some variable allows the
definition of any language from the arithmetical hierarchy in the
corresponding Kripke structure using multimodal logic.
On Boolean closed full trios and rational Kripke frames
(joint work with Markus Lohrey)
Given at Seminar "Automata and Logic" at Technische Universität Ilmenau in Ilmenau, Germany [ Show abstractHide abstract
]
Abstract
A Boolean closed full trio is a class of languages that is closed under Boolean
operations (union, intersection, and complement) and rational transductions. It
is well-known that the regular languages constitute such a Boolean closed full
trio. It is shown here that every such language class that contains any
non-regular language already includes the whole arithmetical hierarchy
(and even the one relative to this language).
Our construction also shows that there is a fixed rational Kripke frame such
that assigning an arbitrary non-regular language to some variable allows the
interpretation of any language from the arithmetical hierarchy in the
corresponding Kripke structure.
Another consequence of our result is that no full trio generated by one
language is closed under complementation, unless it coincides with the regular
languages.
Abstract
A Boolean closed full trio is a class of languages that is closed under Boolean
operations (union, intersection, and complement) and rational transductions. It
is well-known that the regular languages constitute such a Boolean closed full
trio. We present a result stating that every such language class that
contains any non-regular language already contains the whole arithmetical
hierarchy.
Our construction also shows that there is a fixed rational Kripke frame such
that assigning an arbitrary non-regular language to some variable allows the
interpretation of any language from the arithmetical hierarchy in the
corresponding Kripke structure.
Abstract
A valence automaton over a monoid $M$ is a finite automaton
in which each edge carries an input word and an element of
$M$. A word is then accepted if there is a run that spells
the word such that the product of the monoid elements is the
identity.
By choosing suitable monoids $M$, one can obtain various
kinds of automata with storage as special valence automata.
Examples include pushdown automata, blind multicounter
automata, and partially blind multicounter automata.
Therefore, valence automata offer a framework to generalize
results on such automata with storage.
This talk will present recent advances in this direction. The addressed
questions include: For which monoids do we have a Parikh's Theorem (as for
pushdown automata)? For which monoids can we avoid silent transitions?
Semilinearity and Context-Freeness of Languages Accepted by Valence Automata
(joint work with Phoebe Buckheister)
Given at MFCS 2013 in Klosterneuburg, Austria [ Show abstractHide abstract
| Slides ]
Abstract
Valence automata are a generalization of various models of automata with
storage. Here, each edge carries, in addition to an input word, an element of
a monoid. A computation is considered valid if multiplying the monoid elements
on the visited edges yields the identity element. By choosing suitable
monoids, a variety of automata models can be obtained as special valence
automata.
This work is concerned with the accepting power of valence automata.
Specifically, we ask for which monoids valence automata can accept only
context-free languages or only languages with semilinear Parikh image,
respectively.
First, we present a characterization of those graph products (of monoids) for
which valence automata accept only context-free languages. Second, we provide a
necessary and sufficient condition for a graph product of copies of the
bicyclic monoid and the integers to yield only languages with semilinear Parikh
image when used as a storage mechanism in valence automata. Third, we show that
all languages accepted by valence automata over torsion groups have a
semilinear Parikh image.
Abstract
It is shown that membership in rational subsets of wreath
products $H \wr V$ with $H$ a finite group and $V$ a virtually
free group is decidable. On the other hand, it is shown that
there exists a fixed finitely generated submonoid in the wreath
product $\mathbb{Z}\wr\mathbb{Z}$ with an undecidable
membership problem.
Abstract
We consider the computational power of silent transitions in one-way automata
with storage. Specifically, we ask which storage mechanisms admit a
transformation of a given automaton into one that accepts the same language
and reads at least one input symbol in each step.
We study this question using the model of valence automata. Here, a finite
automaton is equipped with a storage mechanism that is given by a monoid.
This work presents generalizations of known results on silent transitions.
For two classes of monoids, it provides characterizations of those monoids that
allow the removal of silent transitions. Both classes are defined by
graph products of copies of the bicyclic monoid and the group of integers. The
first class contains pushdown storages as well as the blind counters while the
second class contains the blind and the partially blind counters.
Abstract
A valence automaton over a monoid M is a finite automaton in
which each edge carries an input word and an element of M. A
word is then accepted if there is a run that spells the word
such that the product of the monoid elements is the identity.
By choosing appropriate monoids M, one can obtain various
kinds of automata with storage as special valence automata.
Examples include pushdown automata, blind multicounter
automata, and partially blind multicounter automata.
Therefore, valence automata offer a framework to generalize
results on such automata with storage. This talk will present
recent advances in this direction. The addressed questions
include: For which monoids can we accept non-regular
languages? For which monoids can we determinize automata? For
which monoids do we have a Parikh's Theorem (as for pushdown
automata)?
Abstract
A valence automaton over a monoid $M$ is a finite automaton in
which each edge carries an input word and an element of $M$. A
word is then accepted if there is a run that spells the word
such that the product of the monoid elements is the identity.
By choosing appropriate monoids $M$, one can obtain various
kinds of automata with storage as special valence automata.
Examples include pushdown automata, blind multicounter
automata, and partially blind multicounter automata. Therefore,
valence automata offer a framework to generalize results on
such automata with storage. This talk will present recent
results on valence automata. The addressed questions include:
For which monoids can we accept non-regular languages? For
which monoids can we determinize automata? For which monoids
can we avoid silent edges (i.e., those which read no input
symbol)?
Valence automata as a generalization of automata with storage
Given at Algebra and Cryptography Seminar at CUNY Graduate Center in New York City, USA [ Show abstractHide abstract
]
Abstract
A valence automaton over a monoid M is a finite automaton in which
each edge carries an input word and an element of M. A word is then
accepted if there is a run that spells the word such that the product of
the monoid elements is the identity.
By choosing appropriate monoids M, one can obtain various kinds of
automata with storage as special valence automata. Examples include
pushdown automata, blind multicounter automata, and partially blind
multicounter automata. Therefore, valence automata offer a framework to
generalize results on such automata with storage.
This talk will present recent results on valence automata. The addressed
questions include: For which monoids can we accept non-regular
languages? For which monoids can we determinize automata? For which
monoids can we avoid silent edges (i.e., those which read no input
symbol)?
Silent Transitions in Valence Automata
Given at Seminar "Algebraic and Logical Foundations of Computer Science" at Universität Leipzig in Germany [ Show abstractHide abstract
]
Abstract
We consider the problem of eliminating silent transitions
from one-way automata with storage. It is known that in
pushdown automata and in blind multicounter automata (where
the counter values can become negative and are only
zero-tested in the end), silent transitions can be avoided.
On the other hand, in the case of partially blind
multicounter automata (where the counter values are always
non-negative and are only zero-tested in the end), silent
transitions are necessary to accept all languages. In order
to study the expressive power of silent transitions in
greater generality, we use the model of valence automata.
Here, a finite automaton is equipped with a storage
mechanism that is given by a monoid. Since many models of
automata with storage (including all of the above) arise as
special valence automata, our question is: for which monoids
can silent transitions be avoided? This work presents
generalizations of the results above. For two classes of
monoids, it provides characerizations of those monoids that
allow the removal of silent transitions. Both classes are
defined by graph products of copies of the bicyclic monoid
and the group of integers.
Abstract
During recent decades, classical models in language theory have been extended
by control mechanisms defined by monoids. We study which monoids cause the
extensions of context-free grammars, finite automata, or finite state
transducers to exceed the capacity of the original model. Furthermore, we
investigate when, in the extended automata model, the nondeterministic variant
differs from the deterministic one in capacity. We show that all these
conditions are in fact equivalent and present an algebraic characterization. In
particular, the open question of whether every language generated by a valence
grammar over a finite monoid is context-free is provided with a positive
answer.
Abstract
In each grammar model, it is an important question whether erasing productions
are necessary to generate all languages. Using the concept of grammars with
control languages by Salomaa, which offers a uniform treatment of a variety of
grammar models, we present a condition on the class of control languages that
guarantees that erasing productions are avoidable in the resulting grammar
model. On the one hand, this generalizes the previous result that in Petri net
controlled grammars, erasing productions can be eliminated. On the other hand,
it allows us to infer that the same is true for vector grammars.
On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids
Given at ICALP 2011 in Zürich, Switzerland [ Show abstractHide abstract
]
Abstract
During recent decades, classical models in language theory have been extended
by control mechanisms defined by monoids. We study which monoids cause the
extensions of context-free grammars, finite automata, or finite state
transducers to exceed the capacity of the original model. Furthermore, we
investigate when, in the extended automata model, the nondeterministic variant
differs from the deterministic one in capacity. We show that all these
conditions are in fact equivalent and present an algebraic characterization. In
particular, the open question of whether every language generated by a valence
grammar over a finite monoid is context-free is provided with a positive
answer.
Abstract
Three open questions in the theory of regulated
rewriting are addressed. The first is whether every
permitting random context grammar has a non-erasing
equivalent. The second asks whether the same is true
for matrix grammars without appearance checking. The
third concerns whether permitting random context
grammars have the same generative capacity as matrix
grammars without appearance checking.
The main result is a positive answer to the first
question. For the other two, conjectures are
presented. It is then deduced from the main result
that at least one of the two holds.
Abstract
It is shown that applying linear erasing to a Petri net
language yields a language generated by a non-erasing
matrix grammar. The proof uses Petri net controlled
grammars. These are context-free grammars, where the
application of productions has to comply with a firing
sequence in a Petri net. Petri net controlled grammars are
equivalent to arbitrary matrix grammars (without
appearance checking), but a certain restriction on them
(linear Petri net controlled grammars) leads to the class
of languages generated by non-erasing matrix grammars.
It is also shown that in Petri net controlled grammars
(with final markings and arbitrary labeling), erasing
rules can be eliminated, which yields a reformulation of
the problem of whether erasing rules in matrix grammars
can be eliminated.
Abstract
We compare various modes of firing transitions in Petri nets
and define classes of languages defined this way. We define
languages through steps, i. e. sets of transitions, maximal
steps, multi-steps, and maximal multi-steps of transitions
in Petri nets, but in a different manner than those defined
in [Burk 81a,Burk 83], by considering labeled transitions.
We will show that we obtain a hierarchy of families of
languages defined by multiple use of transition in firing
transitions in a single multistep. Except for the maximal
multi-steps all classes can be simulated by sequential
firing of transitions.
Abstract
We present a generalization of finite automata using Petri nets
as control. Acceptance is defined by final markings of the
Petri net. The class of languages obtained by $\lambda$-free
concurrent finite automata contains both the class of regular
sets and the class of Petri net languages defined by final
marking.