Infinite automata 1000-2M22AN
Infinite-state systems are ubiquitous in computer science; they arise, for example, as
a consequence of unbounded concurrency or of unbounded stack depth. It can be
more appropriate and informative to consider an infinite set of states, instead of
forcibly restricting to a finite (but potentially astronomically large) set of states. This
is true, for instance, for pushdown automata (PDA) and vector addition systems with
states (VASS), which are equivalent to Petri nets. Despite the infiniteness of their
state space, many infinite-state models admit algorithmically solvable decision
problems; such as language emptiness, language inclusion, reachability, and
coverability. We will investigate a variety of infinite-state systems and several
important decision problems. One of the final goals of this course is to show that
reachability in Petri nets/VASS is decidable. This course covers the following topics:
1) PDAs (checking languages emptiness and searching for short runs);
2) Basic infinite-state systems that have an undecidable halting problem (such
as two-stack PDAs and counter machines);
3) Semilinear sets and Presburger arithmetic;
4) Parikh’s theorem and some applications (such as unary PDAs recognise
regular languages);
5) Well-quasi-orderings and some applications (such as decidability of
universality of counter nets);
6) Integer linear programming and some applications (such as reachability in
binary-encoded 1-VASS is in NP);
7) Coverability and boundedness in VASS (including Rackoff’s technique);
8) Interesting examples of VASS (including VASS with non-semilinear
reachability sets);
9) Fast growing functions and reachability in VASS is Ackermann-hard; and
10) Reachability in VASS is decidable.
Main fields of studies for MISMaP
Type of course
Requirements
Prerequisites
Course coordinators
Term 2025Z: | Term 2024Z: |
Assessment criteria
Oral exam and star assignments.
In the case of PhD student an additional requirement: solving of at least one star
assignment or presenting a recent research article closely related to a chosen topic.
Bibliography
R. Lipton: The Reachability Problem Requires Exponential Space. University of Yale Research Report (63), 1976.
C. Rackoff: The Covering and Boundedness Problems for Vector Addition Systems, Theoretical Computer Science 1978.
J. Hopcroft, J. Pansiot: On the Reachability Problem for 5-Dimensional Vector Addition Systems, Theoretical Computer Science 1979.
F. Eisenbrand, G. Shmonin: Carathéodory bounds for integer cones, Operations Research Letters 2006.
C. Haase, S. Kreutzer, J. Ouaknine, J. Worrell: Reachability in Succinct and
Parametric One-Counter Automata, CONCUR 2009.
S. Schmitz: The complexity of reachability in vector addition systems, ACM SIGLOG News 2016.
C. Haase: A Survival Guide to Presburger Arithmetic, ACM SIGLOG News 2018.
J. Leroux, S. Schmitz: Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension, LICS 2019.
S. Lasota: VASS reachability in three steps, 2020.
W. Czerwiński, Ł. Orlikowski: Reachability in Vector Addition Systems is Ackermann-complete, FOCS 2021.
Additional information
Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes:
- Bachelor's degree, first cycle programme, Computer Science
- Master's degree, second cycle programme, Computer Science
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: