Regular Model Checking for Systems with Effectively Regular Reachability Relation

TL;DR

This paper extends regular model checking to analyze almost-sure and recurrent reachability in systems with effectively regular reachability relations, providing new decidability and complexity results for safety and liveness properties.

Contribution

It introduces methods for verifying almost-sure and recurrent reachability in regular transition systems, expanding the scope of regular model checking techniques.

Findings

Decidability results for almost-sure reachability and recurrent reachability.

Complexity bounds for verifying safety, liveness, and almost-sure properties.

Extension of regular abstraction frameworks to new property classes.

Abstract

Regular model checking is a well-established technique for the verification of regular transition systems (RTS): transition systems whose initial configurations and transition relation can be effectively encoded as regular languages. In 2008, To and Libkin studied RTSs in which the reachability relation (the reflexive and transitive closure of the transition relation) is also effectively regular, and showed that the recurrent reachability problem (whether a regular set $L$ of configurations is reached infinitely often) is polynomial in the size of RTS and the transducer for the reachability relation. We extend the work of To and Libkin by studying the decidability and complexity of verifying almost-sure reachability and recurrent reachability -- that is, whether $L$ is reachable or recurrently reachable w.p. 1. We then apply our results to the more common case in which only a regular overapproximation of the reachability relation is available. In particular, we extend recent complexity results on verifying safety using regular abstraction frameworks -- a technique recently introduced by Czerner, the authors, and Welzel-Mohr -- to liveness and almost-sure properties.