Structural Reductions and Stutter Sensitive Properties

TL;DR

An approach that can reason using a partition of a property language into its stutter insensitive, shortening insensitive, lengthening insensitive and length sensitive parts to still use structural reductions even when working with arbitrary properties.

Abstract

Verification of properties expressed as $ω$-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a \emph{reduction} of a system. A reduction has the property that it can only shorten runs. Lipton's transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. We also present an approach that can reason using a partition of a property language into its stutter insensitive, shortening insensitive, lengthening insensitive and length sensitive parts to still use structural reductions even when working with arbitrary properties. An implementation and experimental evidence is provided showing most non-random properties sensitive to stutter are actually shortening or lengthening insensitive.

Figures (6)

• Figure 1: Example of reductions. (1) is a program with two threads and 3 variables. chan is a communication channel where send(int) insert a message and int recv() waits until a message is available and then consumes it. We assume that one can only observe whether $x$ or $y$ is zero denoted $p$ and $q$. (2) depicts the state-space represented as a Kripke structure. Each node is labelled by the values of atomic propositions $p$ and $q$. When an instruction is executed the values of these propositions may evolve. (3) represents the state-space of a structurally reduced version of the program where actions of thread $\beta$ "z=40;chan.send(z)" are fused into a single atomic operation. (4) represents the state-space of a program where the three actions of the original program "z=40;chan.send(z);y=chan.recv()" are now a single atomic step.
• Figure 1: Sensitivity to length of properties measured using several LTL benchmarks. We distinguish stutter insensitive (SI), lengthening insensitive (LI), shortening insensitive (ShI), and length sensitive (LS) formulae.
• Figure 2: $\Sigma^\omega$ is represented as a circle that is partitioned into equivalence classes of words ($\hat{r_0}, \hat{r_1} \ldots$). Each point in the space is a word, and some of the $\preccurlyeq$ relations are represented as arrows ; the red point is the shortest word $\underline{\hat{r}}$ in the equivalence class. Gray areas are inside the language, white are outside of it. Four languages are depicted: $\mathscr{L}_a$: equivalence classes are entirely inside or outside a stutter insensitive language, $\mathscr{L}_b$: the "bottom" of an equivalence class may belong to a shortening insensitive language, $\mathscr{L}_c$: the "top" of an equivalence class may belong to a lengthening insensitive language, $\mathscr{L}_d$: some languages are neither lengthening insensitive nor shortening insensitive.
• Figure 3: Pre and Post agglomeration rules, graphically represented. Figures to the left are before agglomeration and to the right after the transformation. Places in red cannot be part of the support of the property.
• Figure 4: Experiments on the MCC'2021 LTL benchmark using the two best tool of the MCC contest: Tapaal and ITS-tools. These plots show the results on the $9222$ examples (21% of the original $43989$ examples of the MCC) where the formula is shortening or lengthening insensitive (but not both) and the system can be reduced. Figures (a) and (c) contain the cases where the verdict of the semi-decisions procedures is reliable, and distinguish cases where the output is True (empty product) and False (non empty product). (b) and (d) display the cases where the verdict is not reliable and distinguish cases where the output is inconsistent with the ground truth from cases where they agree.

Theorems & Definitions (22)

• Definition 2.1: Word
• Definition 2.2: Shorter than
• proof
• Definition 2.4: Stutter equivalence
• Definition 2.5: Language
• Definition 2.6: Shortening insensitive
• Definition 2.7: Lengthening insensitive
• proof
• Definition 2.9: Reduction
• Theorem 2.10: Reduced Emptiness Checks