Undecidable problems in unreliable computations
Undecidable problems in unreliable computations
复制标题
DOI：
10.1016/s0304-3975(02)00646-1
复制
发表时间：
2003-03-17
影响因子：
1.1
通讯作者：
Mayr, R
中科院分区：
文献类型：
--
作者：
Mayr, R
有损耗的反机器定义为明斯基柜台机器，该机器的计数器中的值可以随时自发降低。虽然终止是有损耗的反机器可决定的，但结构性终止（每个输入的终止）是不可决定的。这种不可证明的结果具有深远的后果。有损耗的反机器可以用作证明许多问题的不可证明性的一般工具，例如：（1）通过不可靠的通道进行建模通信的系统（例如，模型检查有损的FIFO通道系统和有损耗的矢量添加系统） 。 （2）重置培养皿网的几个问题，例如结构终止，界限和结构界限。 （3）参数化问题，例如广播通信协议的公平性。 （c）2002年Elsevier Science B.V.发表
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 input) 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 broadcast communication protocols. (C) 2002 Published by Elsevier Science B.V.