On termination and invariance for faulty channel machines
On termination and invariance for faulty channel machines
复制标题
关于故障通道机器的终止和不变性
DOI：
10.1007/s00165-012-0234-7
复制
发表时间：
2012
影响因子：
1
通讯作者：
Bouyer P
中科院分区：
文献类型：
--
作者：
Bouyer P
通道机由一个有限控制器和若干fifo通道组成；控制器可以从通道的头部读取消息，并将消息写入通道的尾部。本文主要研究具有插入错误的信道机，即在其信道中消息可以自发出现的信道机。我们考虑不变性问题：给定的插入通道机器是否具有无限的计算量，其所有配置都满足给定的谓词？我们证明，如果谓词在消息损失下关闭，则此问题是基元递归的。在此条件下，给出了不变性问题的非初等下界。最后，利用之前的结果，我们证明了度量时间逻辑的安全片段的可满足性问题是非初等的。
Achannel machineconsists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper we focus on channel machines withinsertion errors, i.e., machines in whose channels messages can spontaneously appear. We consider theinvarianceproblem: does a given insertion channel machine have an infinite computation all of whose configurations satisfy a given predicate? We show that this problem is primitive-recursive if the predicate is closed under message losses. We also give a non-elementary lower bound for the invariance problem under this restriction. Finally, using the previous result, we show that the satisfiability problem for the safety fragment of Metric Temporal Logic is non-elementary.
登录
查看更多内容
关于计算结构良好的常规模型检查中的不动点及其在有损信道系统中的应用
DOI：
--
发表时间：
2006
期刊：
Logic Programming and Automated Reasoning
影响因子：
--
作者：
C. Baier;N. Bertrand;P. Schnoebelen
通讯作者：
P. Schnoebelen
不可靠的渠道比完美的渠道更容易验证
影响因子：
1
作者：
Gérard Cécé;A. Finkel;S. Iyer
通讯作者：
S. Iyer
关于故障通道机器的终止
DOI：
--
发表时间：
2008
期刊：
Symposium on Theoretical Aspects of Computer Science
影响因子：
--
作者：
P. Bouyer;N. Markey;Joël Ouaknine;P. Schnoebelen;J. Worrell
通讯作者：
J. Worrell
影响因子：
1.1
作者：
Mayr, R
通讯作者：
Mayr, R
影响因子：
1.3
作者：
A. Finkel
通讯作者：
A. Finkel