Performing Bisimulation Minimisation To Parity Game Strategies To Improve Controller Quality

Reactive synthesis is the process of creating a controller out of a high-level specification. Recently, new research created a way of converting a linear temporal logic specification to an and-inverter graph. In this process, a parity game is created and solved to obtain a strategy which is directly translated into an and-inverter graph. However, the strategy of the parity game could have some redundant states. Reducing the number of states will result in a smaller graph and therefore a smaller and more efficient controller. This paper investigates how much parity game strategies can be reduced in the reactive synthesis process. Around half of the strategies can be reduced in size and when reduction is possible on average 28% of the strategy is reduced.