Making Weighted Containment Feasible: A Heuristic Based on Simulation and Abstraction

Simulation and Abstraction Guy Avni and Orna Kupferman School of Computer Science and Engineering, Hebrew University, Israel Weighted automata map input words to real numbers and are useful in reasoning about quantitative systems and specifications. The containment problem for weighted automata asks, given two weighted automata A and B, whether for all words w, the value that A assigns to w is less than or equal to the value B assigns to w. The problem is of great practical interest, yet is known to be undecidable. Efforts to approximate weighted containment by weighted variants of the simulation pre-order still have to cope with large state spaces. One of the leading approaches for coping with large state spaces is abstraction. We introabstraction-refinement paradigm for weighted automata and show that it nicely combines with weighted simulation, giving rise to a feasible approach for the containment problem. The weighted-simulation pre-order we define is based on a quantitative tw...

• Type: Journal
• Year: 2012
• Where: CONCUR
• Authors: Guy Avni, Orna Kupferman
• Keywords: CONCUR 2012, Containment Problem, Distributed And Parallel Computing, Hebrew University, Quantitative Systems