Parametrized Verification of Linear Networks Using Automata as Invariants

In this paper we proposed a formalism based on automata on two dimensional strings for specifying inductive invariants for proving correctness of families of linear and circular networks. We proved our inductive approach to be sound and complete (semantical completeness). We have illustrated our approach by simple examples.