Weighted Pushdown Systems and Weighted Transducers
Akash Lal, Tayssir Touili, Nicholas Kidd, and Thomas Reps
Pushdown Systems (PDSs) are an important formalism for modeling
programs. Reachability analysis on PDSs has been used extensively for
program verification. A key result, which made PDSs popular in the
model-checking community was that the set of reachable stack
configurations starting from a regular set of configurations is also
regular. A more general result was given by Caucal who showed that a
PDS's reachability relation, which maps stack configurations to their
reachable set of stack configurations, can be encoded using a
finite-state transducer. In this paper, we generalize the result to
weighted pushdown systems, which have proven to be very useful for model
checking as well as dataflow analysis. The same algorithm provides an
efficient construction of transducers for ordinary (unweighted) PDSs. We
also give a direct saturation algorithm for constructing transducers for
single-state PDSs.
(Click here to access the paper:
PDF.)
University of Wisconsin