VeriSiMPL: Verification via biSimulations of MPL Models

  • Dieky Adzkiya
  • Alessandro Abate
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)


VeriSiMPL (“very simple”) is a software tool to obtain finite abstractions of Max-Plus-Linear (MPL) models. MPL models (Sect. 2), specified in MATLAB, are abstracted to Labeled Transition Systems (LTS). The LTS abstraction is formally put in relationship with the concrete MPL model via a (bi)simulation relation. The abstraction procedure (Sect. 3) runs in MATLAB and leverages sparse representations, fast manipulations based on vector calculus, and optimized data structures such as Difference-Bound Matrices. LTS abstractions can be exported to structures defined in the PROMELA. This enables the verification of MPL models against temporal specifications within the SPIN model checker (Sect. 4). The toolbox is available at


Linear Temporal Logic Label Transition System Simulation Relation Precedence Graph Vector Calculus 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baccelli, F., Cohen, G., Olsder, G., Quadrat, J.P.: Synchronization and Linearity, An Algebra for Discrete Event Systems. John Wiley and Sons (1992)Google Scholar
  2. 2.
    Katz, R.: Max-plus (A,B)-invariant spaces and control of timed discrete-event systems. IEEE Trans. Autom. Control 52(2), 229–241 (2007)CrossRefGoogle Scholar
  3. 3.
    Plus, M.: Max-plus toolbox of Scilab (Online) (1998),
  4. 4.
    Adzkiya, D., De Schutter, B., Abate, A.: Abstraction and verification of autonomous max-plus-linear systems. In: Proc. 31st Amer. Control Conf., pp. 721–726 (2012)Google Scholar
  5. 5.
    Adzkiya, D., De Schutter, B., Abate, A.: Finite abstractions of nonautonomous max-plus-linear systems. In: Proc. 32nd Amer. Control Conf. (June 2013)Google Scholar
  6. 6.
    Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  7. 7.
    Yordanov, B., Belta, C.: Formal analysis of discrete-time piecewise affine systems. IEEE Trans. Autom. Control 55(12), 2834–2840 (2010)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Dieky Adzkiya
    • 1
  • Alessandro Abate
    • 2
  1. 1.Delft Center for Systems and ControlTU DelftThe Netherlands
  2. 2.Department of Computer ScienceUniversity of OxfordUK

Personalised recommendations