Lieu :

Titre: Post Embedding Problems, Dickson’s Lemma, and Master Problems for Monotonic Counter Systems

Description du stage :

Lossy counter machines, aka LCMs, are a variant of Minsky counter machines where integer counters are unreliable and can lose any part of their contents without any warning. They are a prototypical instance of well-structured transition systems, where the underlying well-quasi-ordering (wqo) is the product ordering (ℕ^k,≤), cf. Dickson’s Lemma [FS01, Sch10a].

It is now recognized that lossy counter machines correspond to a fundamental level in complexity: the Ackermann level in the Fast-Growing Hierarchy [Sch10b, FFSS11]. This pivotal place is acknowledged by several works showing complexity lower bounds by reduction from LCM’s. However, problems on LCM’s are not as abstract and versatile as one could wish. For the corresponding complexity class, we lack a simple and elegant master problem like SAT (for NP) or Post Corresponding Problem (for Σ₁⁰).
The aim of this research internship is to discover and develop a new master problem equivalent to lossy counter systems reachability. The initial idea is to invent a variant of Post’s Embedding Problem (see [CS07, CS08a, CS10]) that relies on Dickson’s Lemma rather than Higman’s Lemma. This should opens new avenues for research, and the work can be continued in at least two main directions: (1) investigating the new master problem, and (2) connecting it (via two-way reductions) to problems in other areas.

This research program is directly connected to MPRI C2-9 course, on « Vérification de systèmes dynamiques et paramétrés », and is part of the ReacHard project (2011-2015) funded by ANR, on hard reachability problems. It should suit a theoretically-minded student with some taste for abstract algorithmic constructions like what is encountered in basic courses on recursion theory and computational complexity. The internship is an ideal opportunity for starting a PhD thesis funded by the ReacHard project.

Personne(s) encadrant le stage :

Références

[CS07]

P. Chambart and Ph. Schnoebelen. Post embedding problem is not primitive recursive, with applications to channel systems. In FST&TCS 2007, LNCS 4855, pages 265–276. Springer, 2007.

[CS08a]

P. Chambart and Ph. Schnoebelen. The ω-regular Post embedding problem. In FOSSACS 2008, volume 4962 of LNCS, pages 97–111. Springer, 2008.

[CS08b]

P. Chambart and Ph. Schnoebelen. The ordinal recursive complexity of lossy channel systems. In LICS 2008, pages 205–216. IEEE Comp. Soc. Press, 2008.

[CS10]

P.  Chambart and Ph. Schnoebelen. Pumping and counting on the regular Post embedding problem. In ICALP 2010, volume 6199 of LNCS, pages 64–75. Springer,2010.

[FFSS11]

D. Figueira, S. Figueira, S. Schmitz, and Ph. Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s lemma. In LICS 2011, pages 269–278. IEEE Comp. Soc. Press, 2011.

[FS01]

A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1–2):63–92, 2001.

[Sch10a]

Ph. Schnoebelen. Lossy counter machines decidability cheat sheet. In RP 2010, volume 6227 of LNCS, pages 51–75. Springer, 2010.

[Sch10b]

Ph. Schnoebelen. Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In MFCS 2010, volume 6281 of LNCS, pages 616–628. Springer, 2010.

Ce document a été traduit de L^AT_EX par H^EV^EA