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 have been introduced by R. Mayr
in [May03] as a simplification of lossy channel
systems. Because they are unreliable, lossy counters are easier to
simulate in various models (timed automata, register automata, temporal
logics, etc.) and LCMs have been used to prove hardness of many apparently
unrelated questions.
However, the known results about LCMs are still very scarce. Existing
results focus on questions motivated by the verification of protocols or
distributed programs rather than on more fundamental questions, and most
provided answers are not more precise than « decidable » or « undecidable ».
By contrast, when LCMs are used to prove hardness results in other areas,
one would like to be able to choose from a wider range of hard questions,
provided with more precise answers.
For example, it is known from the literature that the question whether the
accessibility set Acc(M) of a LCM is finite is
undecidable [May03]. But in order to use this in reduction we
would like to know more precisely that the question is in fact Σ10-complete. What about
the question whether P⊆Acc(M) for P a
Presbuger-defined set of configurations? What about
Acc(M1)⊆Acc(M2)? These are all open
questions.
The aim of this research internship is to initiate a systematic study of
LCMs. It is expected that this research program will be continued under the
form of a PhD project but, during the Master Thesis part, we propose to
concentrate on the accessibility sets. For these sets, one can obtain various
results by using “incrementally bounded simulation” of Minsky machines, a coding
gadget from [DJS99, May03] that deserves further
explorations.
This research program is directly connected to
MPRI C2-9 course, on
« Vérification de systèmes dynamiques et paramétrés ». See
also [BMO+08, CS07, CS08, Dim09] for related works. 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.
Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe
Schnoebelen, and James Worrell.
On termination for faulty channel machines.
In Susanne Albers and Pascal Weil, editors, Proceedings of the
25th Annual Symposium on Theoretical Aspects of Computer Science
(STACS'08), pages 121–132, Bordeaux, France, February 2008. IBFI.
P. Chambart and Ph. Schnoebelen.
The
ordinal recursive complexity of lossychannel systems.
In Proc. 23rd IEEE Symp. Logic in Computer Science (LICS
2008), Pittsburgh, PA, USA, June 2008, pages 205–216. IEEE Comp. Soc.
Press, 2008.
C. Dufourd, P. Jancar, and Ph. Schnoebelen.
Boundedness of Reset P/T nets.
In Proc. 26th Int. Coll. Automata, Languages, and Programming
(ICALP '99), Prague, Czech Republic, July 1999, volume 1644 of Lecture
Notes in Computer Science, pages 301–310. Springer, 1999.