Monadic Second-order Logic for Parameterized Verification

Abstract

Much work in automatic verification considers families of similar finite-state systems. But an often overlooked property is that sometimes a single finite-state system can be used to describe a parameterized, infinite family of systems. Thus verification of unbounded state spaces can take place by reduction to finite ones.

The purpose of this article is to introduce Monadic Second-order Logic as a practical means of carrying out such reductions. The logic is a highly succinct alternative to the use of regular expressions. We have built a tool that acts as a decision procedure and translator to DFAs.

The potential applications are numerous. We discuss text processing, Boolean circuits, and distributed systems. Our main example is an automatic proof of properties for the ``Dining Philosophers with Encyclopedia'' example by Kurshan and MacMillan. We establish these properties for the parameterized case without the use of induction.