Promptness and Bounded Fairness in Concurrent and Parameterized Systems

Jacobs, Swen, Sakr, Mouhammad and Zimmermann, Martin ORCID: 0000-0002-8038-2453
(2020) Promptness and Bounded Fairness in Concurrent and Parameterized Systems. In: VMCAI 2020.

[img] Text
1911.03122.pdf - Submitted version

Download (333kB) | Preview


We investigate the satisfaction of specifications in Prompt Linear Temporal Logic ) 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 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.

Item Type: Conference or Workshop Item (Unspecified)
Depositing User: Symplectic Admin
Date Deposited: 11 Dec 2019 09:13
Last Modified: 19 Jan 2023 00:13
DOI: 10.1007/978-3-030-39322-9_16
Related URLs: