Regular Model Checking with Regular Relations

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.