Finite abstractions of nonautonomous Max-Plus-Linear systems

This work puts forward a technique to generate finite abstractions of nonautonomous Max-Plus-Linear (MPL) models, a known class of discrete-event systems characterizing the timing related to event counters. Nonautonomous models embed an external input (namely a nondeterministic choice, regarded as an exogenous control signal) in the dynamics. Abstractions are characterized as finite-state Labeled Transition Systems (LTS). LTS are obtained first by partitioning the state space of the MPL model and by associating states of the LTS to the introduced partitions, then by defining relations among the states of the LTS, corresponding to the dynamical (nonautonomous) transitions between the MPL state partitions, and finally by labeling the LTS edges according to the one-step timing properties related to the events of the original MPL model. In order to establish formal equivalences, the finite LTS abstraction is proven either to simulate or to bisimulate the original MPL model. The computational performance of the abstraction procedure is tested on a numerical benchmark. The approach enables the study of properties of the original MPL model by verifying equivalent specifications over the finite LTS abstraction.