- Abstract:
- Lossy counter machines are defined as Minsky counter machines where the values in the counters can spontaneously decrease at any time. While termination is decidable for lossy counter machines, structural termination (termination for every imput) is undecidable. This undecidability result has far-reaching consequences. Lossy counter machines can be used as a general tool to prove the undecidability of many problems, for example: (1) The verification of systems that model communication through unreliable channels (e.g., model checking lossy fifo-channel systems and lossy vector addition systems). (2) Several problems for reset Petri nets, like structural termination, boundedness and structural boundedness. (3) Parameterized problems like fairness of braodcast communication protocols.
- Links To Paper
- No links available
- Bibtex format
- @Article{EDI-INF-RR-1199,
- author = {
Richard Mayr
},
- title = {Undecidable problems in unreliable computations},
- journal = {Theoretical Computer Science},
- year = 2003,
- month = {Mar},
- volume = {297 (1-3)},
- pages = {337-354},
- doi = {10.1016/S0304-3975(02)00646-1},
- }
|
