Abstraction and verification of Discrete Event and Hybrid Systems
|Project members:||dr. D. Adzkiya, MSc (Dieky), prof.dr.ir. B. De Schutter (Bart), Dr.ir. A. Abate (Alessandro)|
|Keywords:||Discrete-event systems, Hybrid systems|
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. MPL models are predisposed to describe the timing synchronization between interleaved processes, under the assumption that timing events are linearly dependent (within the max-plus algebra) on previous event occurrences and (for nonautonomous models) on exogenous schedules. MPL models are widely employed in the analysis and scheduling of infrastructure networks, such as communication and railway systems, production and manufacturing lines, or biological systems. They cannot model concurrency and are related to a subclass of Timed Petri Nets, namely Timed-Event Graphs.
Classical dynamical analysis of MPL models is grounded on their algebraic or geometric features. It allows investigating model properties such as its transient behavior, its periodic regimes, or its ultimate dynamical behavior. This work explores a new, alternative approach to analysis that is based on finite-state abstractions of autonomous and nonautonomous MPL models. Furthermore, by employing a novel representation of the quantities into play (regions over the state and the control spaces, as well as model dynamics), this work seeks to synthesize techniques that are computationally agile.