text: This paper describes the development of finite abstractions of Max-Plus-Linear (MPL) systems using tropical operations. The idea of tropical abstraction is inspired by the fact that an MPL system is a discrete-event model updating its state with operations in the tropical algebra. The abstract model is a finite-state transition system: we show that the abstract states can be generated by operations on the tropical algebra, and that the generation of transitions can be established by tropical multiplications of matrices. The complexity of the algorithms based on tropical algebra is discussed and their performance is tested on a numerical benchmark against an existing alternative abstraction approach.
  @cite_7: Max-Plus-Linear (MPL) systems are a class of discrete-event systems with a continuous state space characterizing the timing of the underlying sequential discrete events. These systems are predisposed to describe the timing synchronization between interleaved processes. MPL systems are employed in the analysis and scheduling of infrastructure networks, such as communication and railway systems, production and manufacturing lines, or biological systems. As a natural extension, Stochastic Max-Plus-Linear (SMPL) systems are MPL systems where the delays between successive events are characterized by random quantities. @PARASPLIT In practical applications SMPL systems are more realistic than simple MPL ones: for instance in a model for a railway network, train running times depend on driver behavior, on weather conditions, and on passenger numbers at stations. @PARASPLIT Verification is used to establish whether the system under consideration possesses certain properties expressed as formulae. As an example, reachability analysis is a fundamental problem in the area of formal methods, systems theory, and performance and dependability analysis. It is concerned with assessing whether a certain state of a system is attainable from given initial states of the system. @PARASPLIT Verification techniques and tools for finite-state systems have been widely investigated and developed in the past decades. However, if the system has a large number of states or even infinitely many states, in general we cannot apply such techniques directly. In this case we need to employ abstraction techniques to formally relate a concrete model to a finite abstraction of it, which is then amenable to be automatically verified by the relevant results in the literature. @PARASPLIT In this PhD thesis we develop novel abstraction techniques for MPL systems, and use them in an application to communication networks. Additionally we discuss reachability of MPL systems and abstraction techniques for SMPL systems. @PARASPLIT The abstraction and reachability algorithms for MPL systems developed in this thesis have been implemented as a MATLAB software tool, "Verification via biSimulations of MPL models'' (VeriSiMPL, as in "very simple''), which is freely available for download at http: www.sourceforge.net projects verisimpl .
summary: The computation of image and of inverse image of a DBM is described in @cite_7 . These computations are used to perform forward and backward reachability analysis, respectively. The worst-case complexity of both procedures is @math , where @math is the number of variables in @math excluding @math . A more detailed explanation about image and inverse image computation of a DBM is in Section 3.3.