并发分离逻辑的一种博弈语义
计算机科学中的逻辑
2017-10-09 v1 编程语言
摘要
在本文中，我们发展了并发分离逻辑的博弈论描述。对于代码与环境对抗的每一个执行轨迹，我们关联一个规范博弈，其中Eve代表代码，Adam代表环境。Eve和Adam的目的是将执行轨迹的每一个中间机器状态分解为三部分：代码部分、环境部分和可用共享资源部分。我们通过将该逻辑的每个推导树解释为这个规范博弈的获胜策略，建立了并发分离逻辑的可靠性。
引用
@article{arxiv.1710.02332,
title = {A Game Semantics of Concurrent Separation Logic},
author = {Paul-André Melliès and Léo Stefanesco},
journal= {arXiv preprint arXiv:1710.02332},
year = {2017}
}