Reasoning about graded strategy quantifiers

To give an evidence of GSL usability, we investigate some basic questions about the Vanilla GSL[1g] fragment, that is the vanilla restriction of the well-studied One-Goal Strategy Logic fragment of SL augmented with graded strategy quantifiers. We show that the model-checking problem for this logic is PTime-complete. We also report on some positive results about the determinacy.