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