Promptness and Bounded Fairness in Concurrent and Parameterized Systems

Jacobs, Swen and Sakr, Mouhammad and Zimmermann, Martin
(2020) Promptness and Bounded Fairness in Concurrent and Parameterized Systems.
In: VMCAI 2020.
Conference: VMCAI Verification, Model Checking and Abstract Interpretation
(In Press)

[img]
Preview
 Text
paper.pdf
Download (499kB) | Preview

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 onthe 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.

Item Type: Conference or Workshop Item (A Paper) (Paper)
Divisions: Swen Jacobs (SJ)
Conference: VMCAI Verification, Model Checking and Abstract Interpretation
Depositing User: Swen Jacobs
Date Deposited: 27 Feb 2020 13:06
Last Modified: 13 Oct 2022 08:25
Primary Research Area: NRA2: Reliable Security Guarantees
URI: https://publications.cispa.saarland/id/eprint/3010

Actions

Actions (login required)

View Item View Item
CISPA is powered by EPrints 3 which is developed by the School of Electronics and Computer Science at the University of Southampton. More information and software credits.