VeriSiMPL 2: An open-source software for the verification of max-plus-linear systems

被引：0
作者：
Dieky Adzkiya
Yining Zhang
Alessandro Abate
机构：
[1] Delft University of Technology,Delft Center for Systems and Control
[2] Institut Teknologi Sepuluh Nopember,Department of Mathematics
[3] University of Oxford,Department of Computer Science
来源：
Discrete Event Dynamic Systems | 2016年 / 26卷
关键词：
Max-plus algebra; Discrete-event systems; Piece-wise affine systems; Transition systems; Model abstractions; Difference-bound matrices; Bisimulations; Model checking;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
This work presents a technique to generate finite abstractions of autonomous Max-Plus-Linear (MPL) systems, a class of discrete-event systems employed to characterize the dynamics of the timing related to the synchronization of successive events. Abstractions of MPL systems are derived as finite-state transition systems. A transition system is obtained first by partitioning the state space of the MPL system into finitely many regions and then by associating a unique state of the transition system to each partitioning region. Relations among the states of the transition system are then set up based on the underlying dynamical transitions between the corresponding partitioning regions of the MPL state space. In order to establish formal equivalences, the obtained finite abstractions are proven either to simulate or to bisimulate the original MPL system. The approach enables the study of general properties of the original MPL system formalized as logical specifications, by verifying them over the finite abstraction via model checking. The article presents a new, extended and improved implementation of a software tool (available online) for the discussed formal abstraction of MPL systems, and is tested on a numerical benchmark against a previous version.
引用
收藏
页码：109 / 145
页数：36
相关论文
共 48 条
  • [1] Adzkiya D(2013)Finite abstractions of max-plus-linear systems IEEE Trans Autom Control 58 3039-3053
  • [2] De Schutter B(2015)Computational techniques for reachability analysis of max-plus-linear systems Automatica 53 293-302
  • [3] Abate A(2000)Discrete abstractions of hybrid systems Proc of the IEEE 88 971-984
  • [4] Adzkiya D(1958)On a routing problem Q Appl Math 16 87-90
  • [5] De Schutter B(2000)Observability and controllability of piecewise affine and hybrid systems IEEE Trans Autom Contro 45 1864-1876
  • [6] Abate A(2012)A max-plus model of ribosome dynamics during mRNA translation J Theor Biol 303 128-140
  • [7] Alur R(1999)Max-plus algebra and system theory: Where we are and where to go now Annu Rev Control 23 207-219
  • [8] Henzinger T(2000)On the ultimate behavior of the sequence of consecutive powers of a matrix in the max-plus algebra Linear Algebra Appl 307 103-117
  • [9] Lafferriere G(2001)Model predictive control for max-plus-linear discrete event systems Automatica 37 1049-1056
  • [10] Pappas GJ(2010)Duality between invariant spaces for max-plus linear discrete event systems SIAM J Control Optim 48 5606-5628
12345