We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology of the system (e.g.\ pipeline, ring). The logic can be easily embedded in monadic second order logic of finitely many successors, and is therefore decidable. Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires to infer an inductive invariant that contains all reachable states of all system instances, and no unsafe state. We present a method to automatically synthesize inductive invariants directly from the formula describing the interactions, without costly fixed point iterations. We experimentally prove that this invariant is strong enough to verify safety properties of a large number of systems including textbook examples (dining philosophers, synchronization schemes), classical mutual exclusion algorithms, cache-coherence protocols and self-stabilization algorithms, for an arbitrary number of components.


翻译:我们认为参数化并存系统是由一定数量但未知的元件组成的参数化共生系统,这些元件是复制一套特定的有限状态自动成形系统获得的。各元件通过执行原子相互作用进行交流,其参与者同时更新其状态。我们采用了一种互动逻辑,以具体说明相互作用的类型(例如,共和会议、广播)和系统的地形学(例如,管道、环)。逻辑可以很容易地嵌入为数有限的许多继承者的单数第二顺序逻辑,因此是可以分解的。证明这种参数化系统的安全特性,例如僵局自由或相互排斥,需要推导一种含有所有系统实例所有可达状态的演化变异性,而不是不安全状态。我们从描述相互作用的公式中提出一种直接自动合成变异性的方法,而没有昂贵的固定点的迭代。我们实验证明,这种变性足以核实大量系统的安全特性,包括教科书实例(哲学家、同步计划)、典型的相互排斥算法、缓存-聚合协议和自我稳定算法,作为任意数字。

0
下载
关闭预览

相关内容

IFIP TC13 Conference on Human-Computer Interaction是人机交互领域的研究者和实践者展示其工作的重要平台。多年来,这些会议吸引了来自几个国家和文化的研究人员。官网链接:http://interact2019.org/
【Cell】神经算法推理,Neural algorithmic reasoning
专知会员服务
28+阅读 · 2021年7月16日
专知会员服务
60+阅读 · 2020年3月19日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
58+阅读 · 2019年10月17日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
CCF推荐 | 国际会议信息6条
Call4Papers
9+阅读 · 2019年8月13日
CCF推荐 | 国际会议信息8条
Call4Papers
9+阅读 · 2019年5月23日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Arxiv
0+阅读 · 2021年10月27日
Arxiv
0+阅读 · 2021年10月26日
Arxiv
8+阅读 · 2021年2月19日
Arxiv
6+阅读 · 2018年10月3日
VIP会员
相关资讯
CCF推荐 | 国际会议信息6条
Call4Papers
9+阅读 · 2019年8月13日
CCF推荐 | 国际会议信息8条
Call4Papers
9+阅读 · 2019年5月23日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Top
微信扫码咨询专知VIP会员