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 级的可靠性是固定的。