eduzhai > Applied Sciences > Engineering >

Symbolic Reachability Analysis of High Dimensional Max-Plus Linear Systems

  • king
  • (0) Download
  • 20210505
  • Save

... pages left unread,continue reading

Document pages: 7 pages

Abstract: This work discusses the reachability analysis (RA) of Max-Plus Linear (MPL)systems, a class of continuous-space, discrete-event models defined over themax-plus algebra. Given the initial and target sets, we develop algorithms toverify whether there exist trajectories of the MPL system that, starting fromthe initial set, eventually reach the target set. We show that RA can be solvedsymbolically by encoding the MPL system, as well as initial and target setsinto difference logic, and then checking the satisfaction of the resultinglogical formula via an off-the-shelf satisfiability modulo theories (SMT)solver. The performance and scalability of the developed SMT-based algorithmsare shown to clearly outperform state-of-the-art RA algorithms for MPL systems,newly allowing to investigate RA of high-dimensional MPL systems: theverification of models with more than 100 continuous variables shows theapplicability of these techniques to MPL systems of industrial relevance.

Please select stars to rate!


0 comments Sign in to leave a comment.

    Data loading, please wait...