Yasuhiko Minamide - Weighted Pushdown Systems with Indexed Weight Domains

lmcs:1641 - Logical Methods in Computer Science, June 29, 2016, Volume 12, Issue 2 - https://doi.org/10.2168/LMCS-12(2:9)2016
Weighted Pushdown Systems with Indexed Weight DomainsArticle

Authors: 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.


    Volume: Volume 12, Issue 2
    Published on: June 29, 2016
    Submitted on: May 2, 2014
    Keywords: Computer Science - Formal Languages and Automata Theory,Computer Science - Programming Languages

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1587 times.
    This article's PDF has been downloaded 414 times.