About This Item

Ask the MINDS@UW Librarian

Weighted Pushdown Systems and Weighted Transducers

Show full item record

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 
‚Äč

Part of

Show full item record

Search and browse




About MINDS@UW

Deposit materials

  1. Register to deposit in MINDS@UW
  2. Need deposit privileges? Contact us.
  3. Already registered? Have deposit privileges? Deposit materials.