Computing Reachable Simulations

TL;DR

This paper introduces algorithms for computing reachable simulation relations and blocks, especially suited for infinite state systems, by interleaving reachability and simulation computations to improve efficiency.

Contribution

It presents a novel symbolic algorithm that efficiently computes reachable simulation relations, contrasting with prior work on bisimulation.

Findings

Algorithm effectively handles infinite state systems.

Interleaving reachability with simulation reduces computation complexity.

Provides theoretical insights into decidability and complexity of the problem.

Abstract

We study the problem of computing the reachable principals of simulation preorder and the reachable blocks of simulation equivalence. Following a theoretical investigation of the decidability and complexity aspects of this problem, which in particular highlights a stark contrast with the already settled case of bisimulation, we design algorithms to solve this problem by leveraging the idea of interleaving reachability and simulation computation while possibly avoiding the computation of all the reachable states or the whole simulation preorder. In particular, we put forward a symbolic algorithm processing state partitions and, in turn, relations between their blocks, which is suited for processing infinite state systems.