论文标题
关于参数化并发系统的不变性问题
On an Invariance Problem for Parameterized Concurrent Systems
论文作者
论文摘要
我们考虑由复制的有限状态流程组成的并发系统，这些过程通过与用户定义的拓扑的网络中的联合交互进行同步。使用具有乘法结缔的资源逻辑和归纳定义的谓词指定该系统，让人联想到分离逻辑。我们考虑的问题是，该逻辑中的给定公式是否定义了一个不变的，即遵循任意触发的相互作用序列的公式模型是否会转换为同一公式的另一个模型。该属性称为\ emph {Havoc不变性}，在证明在运行时改变网络结构的重新配置程序的正确性是典型的。我们证明，破坏不变问题是$ ϕ \型号ψ$可降低的，询问$ ϕ $的任何模型是否也是$ψ$的型号。尽管总体而言，发现不可决定的破坏性不变性，但这种降低允许证明逻辑的一般片段的破坏不变性在2exp中，并且存在2Exp Expect Indailment问题。
We consider concurrent systems consisting of replicated finite-state processes that synchronize via joint interactions in a network with user-defined topology. The system is specified using a resource logic with a multiplicative connective and inductively defined predicates, reminiscent of Separation Logic. The problem we consider is if a given formula in this logic defines an invariant, namely whether any model of the formula, following an arbitrary firing sequence of interactions, is transformed into another model of the same formula. This property, called \emph{havoc invariance}, is quintessential in proving the correctness of reconfiguration programs that change the structure of the network at runtime. We show that the havoc invariance problem is many-one reducible to the entailment problem $ϕ\models ψ$, asking if any model of $ϕ$ is also a model of $ψ$. Although, in general, havoc invariance is found to be undecidable, this reduction allows to prove that havoc invariance is in 2EXP, for a general fragment of the logic, with a 2EXP entailment problem.
