Faster algorithms for quantitative verification in bounded treewidth graphs

DOI10.1007/s10703-021-00373-5OpenAlexW4214759105MaRDI QIDQ2058390

Andreas Pavlogiannis, Rasmus Ibsen-Jensen, Krishnendu Chatterjee

Publication date: 8 December 2021

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-021-00373-5

zbMATH Keywords

quantitative verificationminimum mean cycleconstant treewidth graphsinitial credit for energyminimum ratio cycle

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (1)

Efficient interprocedural data-flow analysis using treedepth and treewidth

Uses Software

• DaCapo
• DIMACS
• Soot
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Graph minors. III. Planar tree-width
• Handbook of weighted automata
• Optimal search for rationals
• New scaling algorithms for the assignment and minimum mean cycle problems
• S-functions for graphs
• A characterization of the minimum cycle mean in a digraph
• Efficient search for rationals
• All structured programs have small tree width and good register allocation
• Shortest paths in digraphs of small treewidth. I: Sequential algorithms
• Faster algorithms for quantitative verification in constant treewidth graphs
• Weighted automata and weighted MSO logics for average and long-time behaviors
• Synthesizing robust systems
• Approximating the minimum cycle mean
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth
• Quantitative Interprocedural Analysis
• Algorithms for algebraic path properties in concurrent systems of constant treewidth components
• From Model Checking to Model Measuring
• Quantitative abstraction refinement
• Quantitative languages
• Quantitative Multi-objective Verification for Probabilistic Systems
• Finding minimum cost to time ratio cycles with small integral transit times
• The Complexity of Mean-Payoff Automaton Expression
• Averaging in LTL
• Infinite Runs in Weighted Timed Automata with Energy Constraints
• New methods for deriving joint probability distributions of structure factors. I
• Graph minors. II. Algorithmic aspects of tree-width
• Two-way cost automata and cost logics over infinite trees
• Parallel algorithms with optimal speedup for bounded treewidth
• Pebble Weighted Automata and Weighted Logics
• Regular Functions and Cost Register Automata
• Quantitative Monadic Second-Order Logic
• Formalizing and Reasoning about Quality
• Depth-First Search and Linear Graph Algorithms
• SOFSEM 2005: Theory and Practice of Computer Science
• Quantitative Languages Defined by Functional Automata
• Computer Aided Verification

This page was built for publication: Faster algorithms for quantitative verification in bounded treewidth graphs