Transitive Closures of Regular Relations for Verifying Infinite-State Systems
Regular relations are relations on words represented by automata on pairs, a special case of length-preserving rational relations. They can be used to model transition relations of infinite-state systems, in which a state can be represented by a word. Examples of such systems are parameterized systems, FIFO channel systems and systems with stacks and integers. We discuss a technique for computing the transitive closure of a regular relation. The transitive closure of a relation represents the effect of applying the relation an arbitrary number of times. For example, if the relation denotes a loop in a program, the transitive closure denotes the effect of executing the loop an arbitrary number of times. We give a characterization of regular relations with a computable transitive closure in terms of a notion of local depth, intuitively meaning that a position in the word representing the state is only transformed a bounded number of times. For example, for a token passing relation, each position is transformed at most twice; once when receiving the token, and once when sending the token.