Weighted Pushdown Systems with Indexed Weight Domains
Weighted Pushdown Systems with Indexed Weight Domains
复制标题
具有索引权重域的加权下推系统
DOI：
10.1007/978-3-642-36742-7_17
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Yasuhiko Minamide
中科院分区：
文献类型：
--
作者：
佐々木信彰;佐々木保幸;本西泰三;劉 平;水野一郎;岡照二;施学昌;伊佐田文彦;徳山美津恵;仲川勇二;Yasuhiko Minamide
加权下推系统的可达性分析是递归程序验证和分析中非常强大的技术。加权下推系统的每个转移规则都与表示规则权重的有界半环的元素相关联。然而，我们已经意识到有界性的限制过于严格，并且加权下推系统的公式对于某些应用来说不够通用。为了概括加权下推系统，我们首先引入堆栈签名的概念，它总结了下推系统计算的效果，并将下推系统公式化为堆栈签名幺半群上的自动机。然后，我们通过引入由幺半群索引的半环来推广加权下推系统，并将有界性弱化为局部有界性。
The reachability analysis of weighted pushdown systems is a very powerful technique in verification and analysis of recursive programs. Each transition rule of a weighted pushdown system is associated with an element of a bounded semiring representing the weight of the rule. However, we have realized that the restriction of the boundedness is too strict and the formulation of weighted pushdown systems is not general enough for some applications. To generalize weighted pushdown systems, we first introduce the notion of stack signatures that summarize the effect of a computation of a pushdown system and formulate pushdown systems as automata over the monoid of stack signatures. We then generalize weighted pushdown systems by introducing semirings indexed by the monoid and weaken the boundedness to local boundedness.