Show simple item record

dc.contributor.authorLal, Akashen_US
dc.contributor.authorTouili, Tayssiren_US
dc.contributor.authorKidd, Nicholasen_US
dc.contributor.authorReps, Thomasen_US
dc.description.abstractPushdown 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.en_US
dc.publisherUniversity of Wisconsin-Madison Department of Computer Sciencesen_US
dc.titleWeighted Pushdown Systems and Weighted Transducersen_US
dc.typeTechnical Reporten_US

Files in this item


This item appears in the following Collection(s)

  • CS Technical Reports
    Technical Reports Archive for the Department of Computer Sciences at the University of Wisconsin-Madison

Show simple item record