A Feedback Arc Set for Spot



Spot is an extensible model checking library using transition-based generalized Büchi automata (TGBA). It contains many state-of-the-art algorithms. In this paperwe focus on two algorithms that create automata with more transitions than necessary. These constructions can be enhanced by computing a feedback arc set (FAS): a set of edges which, when removed from the graph, leave a directed acyclic graph. Ideally, we want a minimal FAS, but this problem is NP-hard. We adapted and improved a heuristic proposed by Eades et al. that approximates a minimal FAS in linear time. We show that the integration of this heuristic in the complementation of deterministic Büchi automata and in the conversion of Rabind automata to Büchi automata reduces the size of the output up to 31% in our experiments. These results depend greatly on the number of cycles and accepting states in the input automaton.