  Regular model checking is an exploration technique for infinite state systems
where state spaces are represented as regular languages and transition
relations are expressed using rational relations over infinite (or finite)
strings. We extend the regular model checking paradigm to permit the use of
more powerful transition relations: the class of regular relations, of which
the rational relations are a strict subset. We use the language of monadic
second-order logic on infinite strings to specify such relations and adopt
streaming string transducers (SSTs) as a suitable computational model. We
introduce nondeterministic SSTs over infinite strings and show that they
precisely capture the relations definable in MSO. We further explore
theoretical properties of omega-NSSTs required to effectively carry out regular
model checking. In particular, we establish that the regular type checking
problem for omega-NSSTs is decidable in PSPACE. Since the post-image of a
regular language under a regular relation may not be regular (or even
context-free), approaches that iteratively compute the image can not be
effectively carried out in this setting. Instead, we utilize the fact that
regular relations are closed under composition, which, together with our
decidability result, provides a foundation for regular model checking with
regular relations.
