Regular Model Checking with Regular Relations

TL;DR

This paper extends regular model checking by incorporating regular relations specified via monadic second-order logic and streaming string transducers, enabling more powerful analysis of infinite state systems.

Contribution

It introduces omega-NSSTs to capture regular relations on infinite strings and proves the decidability of regular type checking in this extended framework.

Findings

Regular relations are more powerful than rational relations for model checking.

Decidability of regular type checking for omega-NSSTs is established in PSPACE.

The approach leverages closure properties of regular relations under composition.

Abstract

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.