Infinite automata 1000-2M22AN
Infinite state-spaces are ubiquitous in computer science, for instance they arise as a consequence of unbounded stack depth or unbounded concurrency. It is sometimes arguably better to consider an infinite set of states, instead of artificially restricting to an a priori finite but astronomically large finite set. This is the case, for instance, in pushdown automata, register automata, timed automata or Petri nets. Despite the infinity of state spaces, many important decision problems are algorithmically solvable for these models. We will investigate the most interesting of these problems, in particular hard decidability proof: reachability in Petri nets. We will also mention some interesting problems that still remain open.
We will present topics chosen among:
1. Semilinear sets, properties and applications
2. Wqo techniques
3. Decision problems for 1-dimensional VASS
4. Lossy counter automata
5. Coverability and reachability in VASS
6. Reversible systems
7. Equivalences in infinite-state systems
8. Language equivalence of deterministic PDA
9. Separability in infinite-state systems
10. Automata with registers or clocks
Main fields of studies for MISMaP
Type of course
Requirements
Prerequisites
Course coordinators
Assessment criteria
Star assignments and oral exam.
In the case of PhD student an additional requirement: solving of some star assignment or presenting some recent research article on the chosen topic.
Bibliography
J. Fearnley, M. Jurdziński, Reachability in two-clock timed automata is PSPACE-complete, ICALP 2013.
Petr Jancar, Bisimulation Equivalence of 1st Order Grammars, ICALP 2014.
Roadmap of infinite results, http://www.brics.dk/~srba/roadmap/roadmap.pdf
S. Lasota, I. Walukiewicz, Alternating Timed Automata. ACM Transactions on Computational Logic 9(2), 2008.
W. Czerwiński, Ł. Orlikowski, Reachability in Vector Addition Systems is Ackermann-complete, FOCS 2021.
S.Lasota, VASS reachability in three steps, 2020.
Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, ed., Handbook of Process Algebra, Elsevier, 2001.
W. Czerwinski, S. Lasota, R. Meyer, S. Muskalla, K. N. Kumar, P. Saivasan:
Regular Separability of Well-Structured Transition Systems. CONCUR 2018
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: