Promptness and Bounded Fairness in Concurrent and Parameterized Systems

Jacobs, Swen, Sakr, Mouhammad and Zimmermann, Martin (2020) Promptness and Bounded Fairness in Concurrent and Parameterized Systems. In: VMCAI 2020.

Text 1911.03122.pdf - Submitted version Download (333kB) | Preview

Abstract

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)
Uncontrolled Keywords:	4613 Theory Of Computation, 46 Information and Computing Sciences
Depositing User:	Symplectic Admin
Date Deposited:	11 Dec 2019 09:13
Last Modified:	21 Jun 2024 10:24
DOI:	10.1007/978-3-030-39322-9_16
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3065136