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.

ASTEC seminar
February 29, 2000

Place: Information technology, Uppsala University
Room: 1549
Time: 13.15 - 14.00 (+ coffee and discussion)

Help on how get here and MIC campus drawing.

There will be an extended period for discussions after the seminar nourished by cookies and coffee.

Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 1 hour.