Abstract

Lossy counter machines are defined in analogy to lossy fifo-channel systems. They are counter machines with counters whose contents can spontaneously decrease at any time. Some variants of lossy counter machines are not Turing-powerful, since reachability and model checking with the temporal logics EF and EG is decidable for them. However, it is undecidable if there exists an initial configuration such that there is an infinite run. Thus structural termination and model checking with the temporal logics CTL and LTL is undecidable for all types of lossy counter machines.

Lossy counter machines can be used as a general tool to show the undecidability of many problems for lossy and non-lossy systems. Examples are verification of lossy fifo-channel systems, model checking lossy Petri nets, structural termination, boundedness and structural boundedness for reset Petri nets, and parametric problems like fairness of broadcast communication protocols.

References:

1. Richard Mayr. Lossy Counter Machines. Submitted to ICALP '99.
2. Richard Mayr. Lossy Counter Machines. Technical report TUM-I9827, TU-München, 1998.
3. Ahmed Bouajjani and Richard Mayr. Model Checking Lossy Vector Addition Systems. To appear in Proceedings of STACS '99: Symposium on Theoretical Aspects of Computer Science. Springer Verlag Lecture Notes in Computer Science.