BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260408T234616Z
UID:Seminar-dept-1247@lxserverA.csc.liv.ac.uk.csc.liv.ac.uk
ORGANIZER:CN=Lutz Oettershagen:MAILTO:Lutz.Oettershagen@liverpool.ac.uk
DTSTART:20241022T130000
DTEND:20241022T140000
SUMMARY:School Seminar Series
DESCRIPTION:Ron van der Meyden: Epistemic Model Checking and Synthesis of Byzantine Agreement Protocols\n\nLogics of knowledge and knowledge-based programs provide a way to give\n\nabstract descriptions of solutions to problems in fault-tolerant\n\ndistributed computing, and have been used to derive optimal protocols\n\nfor these problems with respect to a variety of failure\n\nmodels. Generally, these results have involved complex pencil and\n\npaper analyses with respect to the theoretical ``full-information\n\nprotocol" model of information exchange between network nodes. It is\n\nequally of interest to be able to establish the optimality of\n\nprotocols using weaker, but more practical, models of information\n\nexchange, or else identify opportunities to improve their performance.\n\nOver the last 20 years, automated verification and synthesis tools for\n\nthe logic of knowledge have been developed, such as the model checker\n\nMCK, that can be applied to this problem.\n\n\n\nThe talk will describe the application of MCK to automated analyses of\n\nthis kind.  A number of information-exchange models are considered,\n\nfor the problems of Eventual and Simultaneous Byzantine Agreement\n\nunder a range of failure types. MCK is used to automatically analyze\n\nthese models.  The results demonstrate that it is possible, for small\n\ninstances, to automatically identify optimization opportunities, and\n\nto automatically synthesize optimal protocols.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1247
LOCATION:Ashton Lecture Theatre
END:VEVENT
END:VCALENDAR