Abstract
We study concurrent games with finite-memory strategies where players are given a Bu?chi and a mean-payoff objective, which are related by a lexicographic order: a player first prefers to satisfy its Bu?chi objective, and then prefers to minimise costs, which are given by a mean-payoff function. In particular, we show that deciding the existence of a strict Nash equilibrium in such games is decidable, even if players’ deviations are implemented as infinite memory strategies.