Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems

Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, Carolyn Talcott

TL;DR

This work addresses verification of Time-Sensitive Distributed Systems (TSDS) by developing a Timed Multiset Rewriting (MSR) framework and identifying a decidable fragment called Progressive Timed Systems (PTS), where only a finite number of actions can occur in any bounded time. It defines two core properties—realizability (existence of a good infinite trace) and survivability (all traces are good)—and analyzes their complexity, proving PSPACE-completeness for both in the unbounded case, with NP-complete realizability and $\Delta_2^p$ survivability under time-bounded conditions. The authors introduce $\delta$-configurations to abstract configurations and establish a bisimulation to reduce infinite-trace reasoning to a finite-state-like analysis, enabling tractable verification. The paper also demonstrates practical applicability through drone-inspired scenarios and reports that Maude can automate time-bounded verification within this framework, highlighting potential for scalable analysis of TSDS in real-world settings.

Abstract

Time-Sensitive Distributed Systems (TSDS), such as applications using autonomous drones, achieve goals under possible environment interference (\eg, winds). Moreover, goals are often specified using explicit time constraints which must be satisfied by the system \emph{perpetually}. For example, drones carrying out the surveillance of some area must always have \emph{recent pictures}, \ie, at most $M$ time units old, of some strategic locations. This paper proposes a Multiset Rewriting language with explicit time for specifying and analysing TSDSes. We introduce two properties, \emph{realizability} (some trace is good) and \emph{survivability} (where, in addition, all admissible traces are good). A good trace is an infinite trace in which goals are perpetually satisfied. We propose a class of systems called \emph{progressive 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 both the realizability and the survivability problems are PSPACE-complete. Furthermore, if we impose a bound on time (as in bounded model-checking), we show that for PTS, realizability becomes NP-complete, while survivability is in the $Δ_2^p$ class of the polynomial hierarchy. Finally, we demonstrate that the rewriting logic system Maude can be used to automate time bounded verification of PTS.

Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems

TL;DR

This work addresses verification of Time-Sensitive Distributed Systems (TSDS) by developing a Timed Multiset Rewriting (MSR) framework and identifying a decidable fragment called Progressive Timed Systems (PTS), where only a finite number of actions can occur in any bounded time. It defines two core properties—realizability (existence of a good infinite trace) and survivability (all traces are good)—and analyzes their complexity, proving PSPACE-completeness for both in the unbounded case, with NP-complete realizability and survivability under time-bounded conditions. The authors introduce -configurations to abstract configurations and establish a bisimulation to reduce infinite-trace reasoning to a finite-state-like analysis, enabling tractable verification. The paper also demonstrates practical applicability through drone-inspired scenarios and reports that Maude can automate time-bounded verification within this framework, highlighting potential for scalable analysis of TSDS in real-world settings.

Abstract

Time-Sensitive Distributed Systems (TSDS), such as applications using autonomous drones, achieve goals under possible environment interference (\eg, winds). Moreover, goals are often specified using explicit time constraints which must be satisfied by the system \emph{perpetually}. For example, drones carrying out the surveillance of some area must always have \emph{recent pictures}, \ie, at most time units old, of some strategic locations. This paper proposes a Multiset Rewriting language with explicit time for specifying and analysing TSDSes. We introduce two properties, \emph{realizability} (some trace is good) and \emph{survivability} (where, in addition, all admissible traces are good). A good trace is an infinite trace in which goals are perpetually satisfied. We propose a class of systems called \emph{progressive 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 both the realizability and the survivability problems are PSPACE-complete. Furthermore, if we impose a bound on time (as in bounded model-checking), we show that for PTS, realizability becomes NP-complete, while survivability is in the class of the polynomial hierarchy. Finally, we demonstrate that the rewriting logic system Maude can be used to automate time bounded verification of PTS.

Paper Structure

This paper contains 5 sections, 3 theorems, 7 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Timed Multiset Rewriting Systems
  3. Programming Drone Behavior using PTS
  4. Other Examples
  5. Quantitative Temporal Properties

Key Result

proposition thmcounterproposition

Let $\mathcal{A}$ be a balanced timed MSR. Let $\mathcal{S}_0$ be an initial configuration with exactly $m$ facts. For all possibly infinite traces $\mathcal{P}$ of $\mathcal{A}$ starting with $\mathcal{S}_0$, all configurations $\mathcal{S}_i$ in $\mathcal{P}$ have exactly $m$ facts.

Figures (1)

  • Figure 1: Macro rules specifying the scenario where drones take pictures of points of interest. Here $\mathcal{P}(p_1,\ldots,p_n)$ denotes $P(p_1,X_1,Y_1)@T_1, \ldots, P(p_n,X_n,Y_n)@T_n$. Moreover, we assume that the Drone stay in a grid of size $x_{max} \times y_{max}$ and have at most $e_{max}$ energy units.

Theorems & Definitions (6)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • proposition thmcounterproposition
  • definition thmcounterdefinition
  • proposition thmcounterproposition
  • proposition thmcounterproposition