Monadic Second-order Logic for Parameterized Verification

Open Access
Publisher Website
Google Scholar
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.

This publication has 0 references indexed in Scilit: