To be Announced: Understanding and model checking Group Announcement Logic
Not peer reviewed
MetadataShow full item record
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.
PublisherThe University of Bergen
SubjectDynamic Epistemic LogicGroup Announcement LogicPublic Announcement LogicEpistemic logicModel checking
Copyright the Author. All rights reserved
Showing items related by title, author, creator and subject.
Ågotnes, Thomas; Ditmarsch, Hans van (Springer, 2010-11-03)Dynamic epistemic logic describes the possible information-changing actions available to individual agents, and their knowledge pre- and post conditions. For example, public announcement logic describes actions in the ...Peer reviewedJournal article
Diskin, Zinovy; Wolter, Uwe Egbert (Elsevier, 2008-11-21)Formal generalized sketches is a graph-based specification format that borrows its main ideas from categorical and ordinary first-order logic, and adapts them to software engineering needs. In the engineering jargon, it ...Journal article
Aartun, Vemund Innvær (The University of Bergen, 2016-06-01)This thesis will look at how to define a representation for the implementation of Cluedo and dynamic epistemic logic into Prolog. It looks at basics of modal logic, and definitions of dynamic epistemic logic. The thesis ...Master thesis