Towards a Model Checking Tool for Strategy Logic with Simple Goals (short paper)?

In this work, we raise the need for an implementation of a model checker for Strategy Logic with Simple Goals (SL[SG]), a recentlyintroduced fragment of Strategy Logic (SL). Notably, SL[SG] subsumes the logic ATL and is strictly contained in SL[1G], a well-known fragment of SL. Thus, the model checker for SL[1G] in MCMAS can handle SL[SG] formulas as well. However we show that, for SL[SG] formulas that are in ATL, one can save space and time by using the MCMAS model checker for ATL. As the model checking complexity for both SL[SG] and ATL is PTIME-complete, there is hope that an implementation in MCMAS for SL[SG] would work as fast as that for ATL.