Regular Model Checking with Regular Relations
Vrunda Dave, Taylor Dohmen, Shankara Narayana Krishna, Ashutosh, Trivedi

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
