Promptness and Bounded Fairness in Concurrent and Parameterized Systems

被引：1

作者：

Jacobs, Swen ^{[1
]}

Sakr, Mouhammad ^{[1
,2
]}

Zimmermann, Martin ^{[3
]}

机构：

[1] CISPA Helmholtz Ctr Informat Secur, Saarbrucken, Germany

[2] Saarland Univ, Saarbrucken, Germany

[3] Univ Liverpool, Liverpool, Merseyside, England

来源：

VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2020 | 2020年 / 11990卷

基金：

英国工程与自然科学研究理事会;

关键词：

MODEL CHECKING;

D O I：

10.1007/978-3-030-39322-9_16

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：337 / 359

页数：23

共 34 条

[1]

Alur R., 2001, ACM T COMPUT LOG, V2, P388, DOI [DOI 10.1145/377978.377990, 10.1145/377978.377990.]

[2] Parameterized model checking of rendezvous systems [J].

Aminof, Benjamin ;

Kotek, Tomer ;

Rubin, Sasha ;

Spegni, Francesco ;

Veith, Helmut .

DISTRIBUTED COMPUTING, 2018, 31 (03) :187-222

[3]

Aminof B, 2014, LECT NOTES COMPUT SC, V8318, P262, DOI 10.1007/978-3-642-54013-4_15

[4]

[Anonymous], 1986, P 1 S LOG COMP SCI C

[5]

[Anonymous], 2017, CEUR WORKSH P ICTCS

[6] Tight Cutoffs for Guarded Protocols with Fairness [J].

Ausserlechner, Simon ;

Jacobs, Swen ;

Khalimov, Ayrat .

VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2016, 2016, 9583 :476-494

[7]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[8]

Bloem R., 2015, DECIDABILITY PARAMET, DOI DOI 10.2200/S00658ED1V01Y201508DCT013

[9] Parameterized Synthesis Case Study: AMBA AHB [J].

Bloem., Roderick ;

Jacobs, Swen ;

Khalimov, Ayrat .

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (157) :68-83

[10]

Bouajjani A., 2000, LNCS, P403

← 1 2 3 4 →