Promptness and Bounded Fairness in Concurrent and Parameterized Systems

TL;DR

This paper explores how concurrent systems satisfy Prompt-LTL specifications with parametric bounds, establishing new decidability results for model checking in systems with multiple components.

Contribution

It introduces cutoff results for parameterized systems with quantitative Prompt-LTL specifications, revealing new decidable fragments of the model checking problem.

Findings

Established connection between bounded fairness and Prompt-LTL satisfaction

Proved first cutoff results for systems with parametric components

Identified new decidable fragments of parameterized model checking

Abstract

We investigate the satisfaction of specifications in Prompt Linear Temporal Logic (Prompt-LTL) by concurrent systems. Prompt-LTL is an extension of LTL that allows to specify parametric bounds on the satisfaction of eventualities, thus adding a quantitative aspect to the specification language. We establish a connection between bounded fairness, bounded stutter equivalence, and the satisfaction of Prompt-LTL\X formulas. Based on this connection, we prove the first cutoff results for different classes of systems with a parametric number of components and quantitative specifications, thereby identifying previously unknown decidable fragments of the parameterized model checking problem.