Optimizing an LTS-Simulation Algorithm (Technical Report)

TL;DR

This paper introduces optimizations for an LTS-simulation algorithm that reduce complexity and improve performance, enabling more efficient computation of simulations over Kripke structures and tree automata.

Contribution

The paper presents novel optimizations that mitigate complexity blow-up related to alphabet size in LTS simulation algorithms, leading to faster and more memory-efficient procedures.

Findings

Significant speed-ups in simulation computation.

Memory savings demonstrated through experiments.

Enhanced asymptotic complexity for simulation over tree automata.

Abstract

When comparing the fastest algorithm for computing the largest simulation preorder over Kripke structures with the one for labeled transition systems (LTS), there is a noticeable time and space complexity blow-up proportional to the size of the alphabet of an LTS. In this paper, we present optimizations that suppress this increase of complexity and may turn a large alphabet of an LTS to an advantage. Our experimental results show significant speed-ups and memory savings. Moreover, the optimized algorithm allows one to improve asymptotic complexity of procedures for computing simulations over tree automata using recently proposed algorithms based on computing simulation over certain special LTS derived from a tree automaton.