Parameterized Verification of Systems with Global Synchronization and Guards
Parameterized Verification of Systems with Global Synchronization and Guards
复制标题
DOI：
10.1007/978-3-030-53288-8_15
复制
发表时间：
2020-06-13
期刊：
影响因子：
--
通讯作者：
Samanta R
中科院分区：
文献类型：
--
作者：
Jaber N;Jacobs S;Wagner C;Kulkarni M;Samanta R
受使用共识或其他协议协议进行全局协调的分布式应用程序的启发，我们为参数化系统定义了一个新的计算模型，该模型基于通用的全局同步原语，并允许全局转换保护。我们的模型推广了许多现有的文献模型，包括广播协议和保护协议。我们证明了无保护系统的可达性性质是可决定的，并给出了有保护系统的可达性性质保持可决定的充分条件。此外，我们还研究了可达性属性的截止点，并在许多受目标应用程序启发的情况下为小截止点提供了充分的条件。
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.
影响因子：
1.1
作者：
Finkel, A;Suhnoebelen, P
通讯作者：
Suhnoebelen, P
DOI：
10.1007/s10009-015-0406-x
发表时间：
2016-10-01
影响因子：
1.5
作者：
Abdulla, Parosh;Haziza, Frederic;Holik, Lukas
通讯作者：
Holik, Lukas
影响因子：
1.3
作者：
Aminof, Benjamin;Kotek, Tomer;Veith, Helmut
通讯作者：
Veith, Helmut