To be Announced: Understanding and model checking Group Announcement Logic
Anders Kåre Eide · NORA - Norwegian Open Research Archives · 2019
In this master’s thesis we present a graphical model checking tool for group announcement logic called GALMC, capable of visualizing the process of checking formulas in a step-by-step fashion. We also define how to enumerate the set of ways a given coalition can restrict a model as well as present pseudocode algorithms describing how we translated these definitions in our model checker.