Compositionality and Reachability with Conditions on Path Lengths
Compositionality and Reachability with Conditions on Path Lengths
复制标题
具有路径长度条件的组合性和可达性
DOI：
10.1142/s0129054109006929
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
W. Thomas
中科院分区：
文献类型：
--
作者：
Ingo Felscher;W. Thomas
在模型检验中，被研究的系统通常以产品的形式出现。Feferman和Vaught在1959年开发的合成方法适合这种情况，可以用来从因子中的信息推导出乘积中公式的真实性。在Wohrle和托马斯（2004）的早期工作的基础上，我们研究了具有可达性谓词的一阶逻辑在非同步产品（即具有有限数量同步转移的同步产品）上的可达性。我们扩展了可达性谓词的条件，相应的路径的长度，制定Presburger算法。对于同步产品，这些增强的可达性谓词，我们证明了一个组合定理，然后表明，存在严重的局限性，概括这一结果。
In model-checking the systems under investigation often arise in the form of products. The compositional method, developed by Feferman and Vaught in 1959, fits to this situation and can be used to deduce the truth of a formula in the product from information in the factors. Building on earlier work of Wohrle and Thomas (2004), we study first-order logic with reachability predicates over finitely synchronized products (i.e. synchronized products with a finite number of synchronization transitions). We extend the reachability predicates by conditions on the length of the corresponding paths, formulated in Presburger arithmetic. For finitely synchronized products with these enhanced reachability predicates we prove a composition theorem and then show that severe limitations exist for generalisations of this result.