Revisiting MU-puzzle. A case study in finite countermodels verification

26^th October 2017, 14:00
Alexei Lisitsa

Abstract

In this talk we will consider well-known MU puzzle from Goedel, Escher, Bach: An Eternal Golden Braid book (GEB) by D. Hofstadter, as an infinite state safety verification problem. We demonstrate fully automated solution (for the first time?) using finite countermodels method (FCM).
We highlight advantages of FCM and compare it with common alternatives.