Lossy counter machines decidability cheat sheet
Philippe Schnoebelen ( LSV, CNRS & ENS de Cachan, France )
- 16:30 18th October 2011 ( week 2, Michaelmas Term 2011 )Lecture Theatre B
Lossy counter machines (LCM's) are a variant of Minsky counter machines 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 talk we survey the basic theory of LCM's and their verification problems, with a focus on the decidability/undecidability divide.
Speaker bio
Dr. Schnoebelen's field of interest is model-checking, i.e., the algorithmic and semantical questions raised by the automated verification of abstract models for systems and software. His main interests within this general area are the question of temporal logic model-checking, and the verification of infinite-state models, in particular "well-structured systems".Dr. Schnoebelen received PhD in Computer Science, INP Grenoble, in 1990, and was a CNRS Researcher in Grenoble from 1990 until 1996. Since 2003, he has been the director of the Lab. Specification & Verification (LSV) in Cachan.
Share this:
