• [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.


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:
    • 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
  • 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