Parameterized Verification of Systems with Global Synchronization and Guards

被引：8

作者：

Jaber, Nouraldin ^{[1
]}

Jacobs, Swen ^{[2
]}

Wagner, Christopher ^{[1
]}

Kulkarni, Milind ^{[1
]}

Samanta, Roopsha ^{[1
]}

机构：

[1] Purdue Univ, W Lafayette, IN 47907 USA

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

来源：

COMPUTER AIDED VERIFICATION (CAV 2020), PT I | 2020年 / 12224卷

基金：

美国国家科学基金会;

关键词：

MODEL CHECKING; SYMMETRY;

D O I：

10.1007/978-3-030-53288-8_15

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Inspired by distributed applications that use consensus or other agreement protocols for global coordination, we define a new computational model for parameterized systems that is based on a general global synchronization primitive and allows for global transition guards. Our model generalizes many existing models in the literature, including broadcast protocols and guarded protocols. We show that reachability properties are decidable for systems without guards, and give sufficient conditions under which they remain decidable in the presence of guards. Furthermore, we investigate cutoffs for reachability properties and provide sufficient conditions for small cutoffs in a number of cases that are inspired by our target applications.

引用

页码：299 / 323

页数：25

共 50 条

[21] Parameterized Verification under TSO with Data Types [J].

Abdulla, Parosh Aziz ;

Atig, Mohamad Faouzi ;

Furbach, Florian ;

Godbole, Adwait A. ;

Hendi, Yacoub G. ;

Krishna, Shankara N. ;

Spengler, Stephan .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, TACAS 2023, 2023, 13993 :588-606

[22] Parameterized Verification under TSO is PSPACE-Complete [J].

Abdulla, Parosh Aziz ;

Atig, Mohamed Faouzi ;

Rezvan, Rojin .

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL)

[23] Forcing Monotonicity in Parameterized Verification: From Multisets to Words [J].

Abdulla, Parosh Aziz .

SOFSEM 2010: THEORY AND PRACTICE OF COMPUTER SCIENCE, PROCEEDINGS, 2010, 5901 :1-15

[24] Verification of Parameterized Communicating Automata via Split-Width [J].

Fortin, Marie ;

Gastin, Paul .

FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2016), 2016, 9634 :197-213

[25] A unified view of parameterized verification of abstract models of broadcast communication [J].

Giorgio Delzanno .

International Journal on Software Tools for Technology Transfer, 2016, 18 :475-493

[26] Parameterized Verification under Release Acquire is PSPACE-complete [J].

Krishna, Shankaranarayanan ;

Godbole, Adwait ;

Meyer, Roland ;

Chakraborty, Soham .

PROCEEDINGS OF THE 2022 ACM SYMPOSIUM ON PRINCIPLES OF DISTRIBUTED COMPUTING, PODC 2022, 2022, :482-492

[27] A unified view of parameterized verification of abstract models of broadcast communication [J].

Delzanno, Giorgio .

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2016, 18 (05) :475-493

[28] Correctness verification of synchronization based workflow model [J].

Cai, J ;

Zhao, W ;

Zhang, SK ;

Wang, LF .

ICEBE 2005: IEEE INTERNATIONAL CONFERENCE ON E-BUSINESS ENGINEERING, PROCEEDINGS, 2005, :527-530

[29] A Hybrid Method for the Verification and Synthesis of Parameterized Self-Stabilizing Protocols [J].

Tahat, Amer ;

Ebnenasir, Ali .

LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2014), 2015, 8981 :201-218

[30] On the Verification of Livelock-Freedom and Self-Stabilization on Parameterized Rings [J].

Klinkhamer, Alex ;

Ebnenasir, Ali .

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2019, 20 (03)

← 1 2 3 4 5 →