PV1 ⊧ DetLPcomparator of two weighted automata

Application domain/field

• Quantitative inclusion
• Discounted-Sum automata (DS-automata)

Expected input

• Weighted automata $P$
• Weighted automata $Q$
• Discount-factor $d>1$

Format:

• Weighted automata should be in .txt files according to a specific format described in the code.
• The discount-factor can be passed when calling the python script.

Expected output

True if $P{\subseteq }_{d}Q$

Internals

Linear-programming based DS-inclusion DS-inclusion: quantitative inclusion for discounted-sum weighted automata Quantitative inclusion: comparing quantitative dimensions between systems such as energy consumption and worst-case execution time. Uses GLPSOL, Reduce.