Faster algorithms for weighted recursive state machines
From MaRDI portal
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Analysis of algorithms and problem complexity (68Q25) Algebraic theory of languages and automata (68Q70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Abstract: Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the best-known complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project.
Recommendations
Cites work
- A Four Russians algorithm for regular expression pattern matching
- Computer Aided Verification
- Faster algorithms for algebraic path properties in recursive state machines with constant treewidth
- Faster algorithms for weighted recursive state machines
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- scientific article; zbMATH DE number 1670555 (Why is no real title available?)
- scientific article; zbMATH DE number 3768948 (Why is no real title available?)
- scientific article; zbMATH DE number 3610766 (Why is no real title available?)
- Interprocedural Analysis of Concurrent Programs Under a Context Bound
- Matrix-vector multiplication in sub-quadratic time (some preprocessing required)
- Model checking procedural programs
- Multiplying matrices faster than coppersmith-winograd
- Precise interprocedural dataflow analysis with applications to constant propagation
- Program Analysis Using Weighted Pushdown Systems
- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
- Reducing concurrent analysis under a context bound to sequential analysis
- Subcubic algorithms for recursive state machines
- The Mailman algorithm: a note on matrix-vector multiplication
- Tools and Algorithms for the Construction and Analysis of Systems
- Weighted pushdown systems and their application to interprocedural dataflow analysis
Cited in
(6)- Tight bounds for reachability problems on one-counter and pushdown systems
- Faster algorithms for algebraic path properties in recursive state machines with constant treewidth
- Faster algorithms for weighted recursive state machines
- Subcubic algorithms for recursive state machines
- Solving Multiple Dataflow Queries Using WPDSs
- Tools and Algorithms for the Construction and Analysis of Systems
This page was built for publication: Faster algorithms for weighted recursive state machines
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988644)
