Quantitative fair simulation games IST Austria Technical Report Chatterjee, Krishnendu ; https://orcid.org/0000-0002-4561-241X Henzinger, Thomas A ; https://orcid.org/0000−0002−2985−7724 Otop, Jan Velner, Yaron ddc:004 Simulation is an attractive alternative for language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. For non-deterministic automata, while language inclusion is PSPACE-complete, simulation can be computed in polynomial time. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. Again, while fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable for mean-payoff automata and the decidability is open for discounted-sum automata, whereas the (quantitative) simulation reduce to mean-payoff games and discounted-sum games, which admit pseudo-polynomial time algorithms. In this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games. For example, whereas for mean-payoff and discounted-sum games, the players do not need memory to play optimally; we show in contrast that for simulation games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal strategies for both players require infinite memory in general, and (ii) for discounted-sum objectives, optimal strategies need not exist for both players. While the simulation games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory requirements for mean-payoff objectives) as compared to their counterpart without Büchi acceptance conditions, we still present pseudo-polynomial time algorithms to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff and weighted discounted-sum automata. IST Austria 2014 info:eu-repo/semantics/other doc-type:other technical_report http://purl.org/coar/resource_type/c_18gh https://research-explorer.ista.ac.at/record/5428 https://research-explorer.ista.ac.at/download/5428/5521 Chatterjee K, Henzinger TA, Otop J, Velner Y. <i>Quantitative Fair Simulation Games</i>. IST Austria; 2014. doi:<a href="https://doi.org/10.15479/AT:IST-2014-315-v1-1">10.15479/AT:IST-2014-315-v1-1</a> eng info:eu-repo/semantics/altIdentifier/doi/10.15479/AT:IST-2014-315-v1-1 info:eu-repo/semantics/altIdentifier/issn/2664-1690 info:eu-repo/semantics/openAccess