On the Complexity of Verification of Time-Sensitive Distributed Systems: Technical Report

This paper develops a Multiset Rewriting language with explicit time for specifying and analyzing Time-Sensitive Distributed Systems (TSDS). Goals are often specified using explicit time constraints. A good trace is an infinite trace in which goals are perpetually satisfied, in spite of a possible environment interference. 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 further properties, recoverability (all compliant traces do not reach points-of-no-return) and reliability (system can always continue functioning using a good trace). Following our previous work (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. Furthermore, if we impose a bound on time (as in bounded model-checking), we show that for PTS, the reliability property is in the $\Delta_2^p$ class of the polynomial hierarchy, a subclass of PSPACE. We also show that bounded survivability is both NP-hard and coNP-hard.