Announcements:
- [2018-10-01] We start only on Nov 5, and we end on Dec 17.
- [2018-11-05] We start only at 12:30.
- [2018-11-07] No lecture on Nov 12 (by a last-minute decision of Polish parliament); we shift all the lectures by one week, and hence end on Jan 7.
Exam:
- PSPACE-hardness of 2-clock timed automata: J. Fearnley, M. Jurdziński, Reachability in two-clock timed automata is PSPACE-complete
- Timed automata with addition: B. Berard, C. Duford, Timed Automata and Additive Clock Constraints
- PSPACE-membership of the reachability problem for 2-VASS: M. Blondin, A. Finkel, S. Goller, C. Haase, P. McKenzie, Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete
- Deciding VASS reachability by Presburger-definable inductive invariants: J. Leroux, Vector Addition Systems Reachability Problem (A Simpler Solution)
- Non-primitive recursive complexity of the equality of reachability sets of bounded VASS: E.W. Mayr, A.R. Meyer, The Complexity of the Finite Containment Problem for Petri Nets
- Undecidability of equivalence problems for Petri nets: P. Jancar, Decidability Questions for Bismilarity of Petri Nets and Some Related Problems
- NP-completeness of the reachability problem for communication-free Petr nets: J. Esparza, Petri Nets, Commutative Context-Free Grammars, and Basic Parallel Processes
- Decidability of coverability of 1-VASS with stack: J. Leroux, G. Sutre, P. Totzke, On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension
- Semilinearity of the reachability set of 5-VAS: J.E. Hopcroft, J.-J. Pansiot, On the reachability problem for 5-dimensional vector addition systems
- Reachability for a tree variant of 1-VASS: S. Goller, C. Haase, R. Lazic, P. Totzke, A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One
Tentative plan:
- lecture 1: introductory example - computing reachability sets of pushdown graphs, definition of Petri nets,
decision problems for Petri nets
- tutorials: PN weakly computing the tower of exponentials (and even faster-growing functions),
translations between VAS, VASS and PN, nonnegative-integer vs integer semantics,
decidability of example properties (boundedness, structural boundedness)
- reading:
- T. Murata, Petri Nets: Properties, Analysis and Applications, sect. I-V (fragments)
- J. Esparza, M. Nielsen, Decidability issues for Petri nets - a survey, sect. 2, 3 (fragments)
- W. Reisig, Sieci Petriego, sect. 2, 5
- W. Reisig, G. Rozenberg (ed), Lectures on Petri Nets I: Basic Models, sect. 1 (fragments)
- homework:
- is liveness monotonic, in the following sense: if a net is live for some initial configuration,
is it also live for every larger initial configuration?
- how to transform an n-dimensional VASS (VAS with states) into an (n+3)-dimensional VAS (without states)?
- lecture 2: EXPSPACE lower bound for Petri nets, EXPSPACE algorithm for coverability
- tutorials: reductions between termination, boundedness, coverability and place-nonemptiness,
and EXPSPACE-completeness of these problems,
reductions between reachability and place-emptiness,
solving place boundedness by computing coverability trees
- reading:
- homework:
- show, by counter-example, that liveness is not monotonic even for 1-bounded Petri nets
(1-bounded = in every reachable configuration, at most 1 token on every place)
- for every m>0 construct a Petri net weakly computing the function Fm, where
- F1(n) = 2n
- Fm+1(n) = Fmn(1), that is, Fm composed n times applied to 1
- lecture 3: Decidability of the reachability problem I
- tutorials: effective decision procedure for the conditions Θ1 and Θ2;
inter-reducibility of reachability and deadlock-freeness
- reading:
- homework:
- find finite representations for downward-closed sets of vectors, and
show decidability of reachability of a given downward-closed set of configurations in a VAS
- show inter-reducibility of VAS reachability and of non-emptiness of S(G) ∩ R, for a given context-free grammar G and
a regular language R, where S(G) stands for the Szilard language (derivation language) of G, i.e., the set of sequences
of productions names in complete derivations of G
- lecture 4: Decidability of the reachability problem II; history of the problem
- tutorials: inter-reducibility of VAS reachability and of non-emptiness of S(G) ∩ R, for a given context-free grammar G and
a regular language R; interreducibility of reachability and liveness; PSPACE membership of reachability in 1-bounded VAS
- reading:
- homework:
- show PSPACE-hardness of reachability in 1-bounded VAS
- what is the complexity of reachability in acyclic 1-bounded VAS?
- show inter-reducibility of VAS reachability and of non-emptiness of S(L) ∩ K, for two given
regular languages L and K, where S(L) stands for the shuffle star of L
- lecture 5: Non-elementary lower bound for the reachability problem
- tutorials: NP-completeness of reachability for cycle-free, communication-free and and conflict-free PN; PSPACE-completeness for 1-bounded PN; EXPSPACE-completeness for reversible PN
- reading:
- lecture 6: Definition of timed automata, region construction for the the non-emptiness problem, undecidability of the universality problem
- tutorials: variants and extensions of timed automata;
(non-)closure of timed regular languages under operations;
undecidability of variuous membership problems;
NP-hardness of non-emptiness of 2-clock automata, PSPACE membership in the general case
- reading:
- homework:
- provide a polynomial-time decision procedure for non-emptiness of 1-clock automata
- prove PSPACE-hardness of non-emptiness in the general case
- for every n, find a timed language recognized by an n-clock automaton but not by an (n-1)-clock one
- lecture 7: Decision problems for timed automata with one clock: decidability via WQO, lower bound by lossy counter machines
- tutorials: extending the decision procedure, deciding if a 1-clock automaton is equivalent to a 0-clock automaton,
decidability of inclusion of 0-timed automata (clocks only compared to 0)
- reading:
Literature:
- J. Esparza, Decidability and complexity of Petri net problems — an introduction
- C. Rackoff, The covering and boundedness problems for vector addition systems
- J. Leroux, The general vector addition system reachability problem by Presburger inductive invariants
- J. Leroux, Vector Addition System Reachability Problem: A Short Self-Contained Proof
- S. Rao Kosaraju, Decidability of reachability in vector addition systems
- S.Lasota, VASS rechability in three steps
- S. Schmitz, The Complexity of Reachability in Vector Addition Systems
- W. Czerwiński, S. Lasota, R. Lazic, J. Leroux, F. Mazowiecki, The Reachability Problem for Petri Nets is Not Elementary
- R. Alur, D. L. Dill, A theory of timed automata
- P. Boyuer, An introduction to timed automata
- R. Alur, M. Parthasarathy, Decision problems for timed automata: a survey
- O. Finkel, On decision problems for timed automata
- J. Ouaknine, J. Worrell, On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap
- S. Lasota, I. Walukiewicz, Alternating timed automata
- P. Schnoebelen, Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets
