On Omega-Languages Defined by Mean-Payoff Conditions

In quantitative verification, system states/transitions have associated costs, and these are used to associate mean-payoff costs with infinite behaviors. In this paper, we propose to define -languages via Boolean queries over meanpayoff costs. Requirements concerning averages such as "the number of messages lost is negligible" are not -regular, but specifiable in our framework. We show that, for closure under intersection, one needs to consider multi-dimensional costs. We argue that the acceptance condition needs to examine the set of accumulation points of sequences of mean-payoffs of prefixes, and give a precise characterization of such sets. We propose the class of multi-threshold mean-payoff languages using acceptance conditions that are Boolean combinations of inequalities comparing the minimal or maximal accumulation point along some coordinate with a constant threshold. For this class of languages, we study expressiveness, closure properties, analyzability, and Borel c...

• Type: Conference
• Year: 2009
• Where: FOSSACS
• Authors: Rajeev Alur, Aldric Degorre, Oded Maler, Gera Weiss
• Keywords: Acceptance Conditions, Accumulation Point, FOSSACS 2009, Requirements Concerning Averages, Software Engineering