This paper develops a Multiset Rewriting language with explicit time for the specification and analysis of Time-Sensitive Distributed Systems (TSDS). Goals are often specified using explicit time constraints. A good trace is an infinite trace in which the goals are satisfied perpetually despite possible interference from the environment. In our previous work (FORMATS 2016), we discussed two desirable properties of TSDSes, realizability (there exists a good trace) and survivability (where, in addition, all admissible traces are good). Here we consider two additional properties, recoverability (all compliant traces do not reach points-of-no-return) and reliability (the system can always continue functioning using a good trace). Following (FORMATS 2016), we focus on a class of systems called Progressing Timed Systems (PTS), where intuitively only a finite number of actions can be carried out in a bounded time period. We prove that for this class of systems the properties of recoverability and reliability coincide and are PSPACE-complete. Moreover, if we impose a bound on time (as in bounded model-checking), we show that for PTS the reliability property is in the $\Pi_2^p$ class of the polynomial hierarchy, a subclass of PSPACE. We also show that the bounded survivability is both NP-hard and coNP-hard.


翻译:本文开发了一个多功能重写语言, 明确用于时间敏感分布系统( TSDS) 的规格和分析。 目标通常使用明确的时间限制来指定。 良好的跟踪是一个无限的痕迹, 尽管可能受到环境的干扰, 仍然可以永久地实现目标。 在先前的工作( FORMATS 2016)中, 我们讨论了TSDS的两种可取属性, 即可变性( 存在良好的跟踪) 和可生存性( 此外, 所有可允许的痕迹都很好 ) 。 我们在这里考虑另外两个属性, 即可恢复性( 所有符合要求的痕迹都没有到达不归点) 和可靠性( 系统总是可以继续使用良好的追踪功能 ) 。 之后( FORMATS 2016) 我们侧重于被称为进步时间系统( PTSDS) 的一类系统( PTSSS), 其中只有有限数量的行动可以在受约束的时期内进行。 我们证明对于这类系统来说, 恢复性和可靠性的特性是同步的, 并且如果我们对时间施加约束( 受约束的模型检查), 我们显示PTSIS 级的可靠性是固定的。

0
下载
关闭预览

相关内容

专知会员服务
41+阅读 · 2021年4月2日
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
CCF推荐 | 国际会议信息10条
Call4Papers
8+阅读 · 2019年5月27日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
计算机类 | LICS 2019等国际会议信息7条
Call4Papers
3+阅读 · 2018年12月17日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
计算机类 | 期刊专刊截稿信息9条
Call4Papers
4+阅读 · 2018年1月26日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
Arxiv
0+阅读 · 2021年11月5日
Arxiv
0+阅读 · 2021年11月4日
Arxiv
3+阅读 · 2017年12月1日
VIP会员
相关资讯
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
CCF推荐 | 国际会议信息10条
Call4Papers
8+阅读 · 2019年5月27日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
计算机类 | LICS 2019等国际会议信息7条
Call4Papers
3+阅读 · 2018年12月17日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
计算机类 | 期刊专刊截稿信息9条
Call4Papers
4+阅读 · 2018年1月26日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
Top
微信扫码咨询专知VIP会员