Lossy Counter Machines Decidability Cheat Sheet

Lossy counter machines (LCM's) are a variant of Minsky counter machines based on weak (or unreliable) counters in the sense that they can decrease nondeterministically and without notification. This model, introduced by R. Mayr [TCS 297:337-354 (2003)], is not yet very well known, even though it has already proven useful for establishing hardness results.In this paper we survey the basic theory of LCM's and their verification problems, with a focus on the decidability/undecidability divide.