Weighted Pushdown Systems and Weighted Transducers

File(s):

Author(s): Lal, Akash; Touili, Tayssir; Kidd, Nicholas; Reps, Thomas
Publisher: University of Wisconsin-Madison Department of Computer Sciences
Date: Mar 15, 2012
Abstract: 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.
Permanent link: http://digital.library.wisc.edu/1793/60536
Export: Export to RefWorks