A Simpler Alternative: Minimizing Transition Systems Modulo Alternating Simulation Equivalence

TL;DR

This paper introduces a simplified method for reducing finite-state transition systems using alternating simulation equivalence, enabling smaller abstractions while preserving control synthesis properties.

Contribution

It presents an algorithm to produce minimal abstractions based on alternating simulation equivalence, offering a less restrictive alternative to existing methods.

Findings

ASE can produce smaller abstractions than alternating bisimulations.

The algorithm guarantees minimal AS equivalent abstractions.

Application to control systems demonstrates practical benefits.

Abstract

This paper studies the reduction (abstraction) of finite-state transition systems for control synthesis problems. We revisit the notion of alternating simulation equivalence (ASE), a more relaxed condition than alternating bisimulations, to relate systems and their abstractions. As with alternating bisimulations, ASE preserves the property that the existence of a controller for the abstraction is necessary and sufficient for a controller to exist for the original system. Moreover, being a less stringent condition, ASE can reduce systems further to produce smaller abstractions. We provide an algorithm that produces minimal AS equivalent abstractions. The theoretical results are then applied to obtain (un)schedulability certificates of periodic event-triggered control systems sharing a communication channel. A numerical example illustrates the results.