Using symmetry of processes to enable model repair.

What is it about?

Distributed programs often consist of running identical processes across multiple machines. Kripke structures are built to capture the state-space of the distributed program and are often quite large (exponential in the number of processes). By using this symmetry we can construct a smaller model of our state-space that preserves certain logical formulae. Moreover, we have a mathematical correspondence between submodels of the smaller model and certain submodels of the larger model that enables us to repair our program for symmetric formulae.

Featured Image