Automatic generation of network invariants for the verification of iterative sequential systems

Abstract

In this paper we present new results on the verification of iterative sequential systems. We address bilateral interconnections and circular arrangements of cells, and extend our previous treatment [13] of unilateral systems. Our approach is based on the new definition of boundedness, given in terms of regularity of the union of an infinite number of languages. The definition of boundedness provides sufficient conditions for the equivalence of iterative systems to be decidable. It also provides network invariants for inductive proofs. This new framework allows the derivation of some previously known results as well as the new ones presented here.