eng
episciences.org
Logical Methods in Computer Science
1860-5974
2016-06-29
Volume 12, Issue 2
10.2168/LMCS-12(2:9)2016
1641
journal article
Weighted Pushdown Systems with Indexed Weight Domains
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.
https://lmcs.episciences.org/1641/pdf
Computer Science - Formal Languages and Automata Theory
Computer Science - Programming Languages