Reachability sets of parameterized rings as regular languages

AbstractWe present here a method for deriving a regular language that characterizes the set of reachable states of a given parameterized ring (made of N identical components). The method basically proceeds in two steps: first one generates a regular language L by inductive inference from a finite sample of reachable states; second one formally checks that L characterizes the whole set of reachable states