Max-Plus Linear Systems
Max-PlusLinear (MPL) models are a class of discrete-event systems used to characterize the dynamics of the timing related to successive events that synchronize autonomously. Nonautonomous versions of MPL models embed within their dynamics nondeterminism, namely a signal choice that is usually regarded as an exogenous control or schedule.
Abstractions of MPL models are characterized as finite-state Labeled Transition Systems (LTS). LTS are obtained first by partitioning the state space (and, for the nonautonomous model, by covering the input 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 based on dynamical transitions between the corresponding partitions of the MPL state space, and finally by labeling the LTS edges according to the one-step timing properties of the events of the original MPL model.
Themes: Max-plus Linear Systems
People: Muhammad Syifa'ul Mufid, Alessandro Abate
Software: VeriSiMPL
Publications:
- Formal Verification of Stochastic Max-Plus-Linear Systems, , {IEEE} Trans. Automat. Contr., Volume 61, Number 10, p.2861–2876, (2016)
- VeriSiMPL 2: An open-source software for the verification of max-plus-linear systems, , Discrete Event Dynamic Systems, Volume 26, Number 1, p.109–145, (2016)
- Computational techniques for reachability analysis of Max-Plus-Linear systems, , Automatica, Volume 53, p.293–302, (2015)
GET IN TOUCH WITH US
CONTACT US
Oxford Control and Verification (OXCAV) Group
C/O Department of Computer Science
Wolfson Building, Parks Rd, Oxford OX1 3QD
T: +44 (0) 18656 10767
Education - This is a contributing Drupal Theme
Design by WeebPal.
Design by WeebPal.