We investigate the problem of computing the reachable blocks of the simulation equivalence and its natural counterpart for the simulation preorder, referred to as the reachable simulation problem. Through a theoretica...
详细信息
We investigate the problem of computing the reachable blocks of the simulation equivalence and its natural counterpart for the simulation preorder, referred to as the reachable simulation problem. Through a theoretical investigation of this problem, we unveil a sharp contrast with the already settled case of bisimulation equivalence. Then, we design algorithms to solve the reachable simulation 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. Specifically, we propose algorithms achieving different guarantees on the precision of the output, and a symbolic algorithm that operates on state partitions and relations between their blocks, which is particularly well-suited for processing infinite-state systems.
We study the problem of computing the reachable principals of the simulation preorder and the reachable blocks of simulation equivalence. Following a theoretical investigation of this problem, which highlights a sharp...
详细信息
ISBN:
(纸本)9783031726200;9783031726217
We study the problem of computing the reachable principals of the simulation preorder and the reachable blocks of simulation equivalence. Following a theoretical investigation of this problem, which highlights a sharp 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.
暂无评论