Petri games are a multi-player game model for distributed systems: the players are represented as tokens on a Petri net and grouped into environment players and system players. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the entire causal history of the other players. In the basic setting, the goal of the system players is to avoid a set of bad global states (markings) against any move of the environment. The question whether the system players have a winning strategy for achieving this goal is in general undecidable, but for a series of subclasses, it has been shown to be decidable, mostly in exponential time. The causal history of places is represented by unfolding the underlying Petri net. A strategy is obtained by cutting decisions that are under control of the system out of the unfolding. In general, unfoldings and thus strategies are infinite. The idea for obtaining a finite winning strategy is to identify repetitions in the unfolding, where the strategy can copy previous decisions. In the context of checking the reachability of markings in Petri nets via unfoldings, last known markings are a suitable criterion for such repetitions. However, for Petri games this is in most cases too weak. In this paper, we propose a stronger notion of repetition, where last known markings are enhanced by equivalence classes of counters recording how many transitions one player has taken in the causal past of another player. We show that it is decidable whether a finite strategy obtained via this criterion of repetition is winning. The proof investigates a labeled transitions system corresponding to the given Petri game. The existence of a winning strategy is encoded as a SAT solving problem.