IBM Logo
IBM Research Lab in Haifa
Hot Shots  
FV Research in HRL  

Download the presentation

Amir Pnueli

Weizmann Institute


Sticks and Stones: Making the Most of a Single Unbounded Dimension

The talk considers the problem of Uniform Algorithmic Verification of Parameterized Systems. As has been observed by several researchers, using regular expressions or equivalent formalisms (e.g. WS1S) as assertional language, we can perform symbolic model checking of systems of unbounded number of states.

We start by showing that the verification problem can be viewed as taking place in a space of 3 dimensions: Time, Control, and Data. We will illustrate how regular expressions can be naturally applied to deal with any of these dimensions in case it becomes unbounded. Unfortunately, extending the tool of regular expressions to 2 dimension leads to a language which is not adequate for model checking.

We therefore, consider alternate ways of dealing with systems which have both unbounded control and unbounded data. By appropriate abstractions and encoding it is frequently possible to encode these two dimensions within a single one. The method will be illustrated on parameterized versions of the Bakery and Peterson's algorithms for mutual exclusion.