References & Citations
Computer Science > Logic in Computer Science
Title: Promptness and Bounded Fairness in Concurrent and Parameterized Systems
(Submitted on 8 Nov 2019 (v1), last revised 15 Nov 2019 (this version, v2))
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.
Submission history
From: Swen Jacobs [view email][v1] Fri, 8 Nov 2019 08:38:57 GMT (56kb)
[v2] Fri, 15 Nov 2019 13:38:57 GMT (60kb)
Link back to: arXiv, form interface, contact.