3 papers
cs.LO2020
Symbolic Reachability Analysis of High Dimensional Max-Plus Linear Systems
Muhammad Syifa'ul Mufid, Dieky Adzkiya, Alessandro Abate
This work discusses the reachability analysis (RA) of Max-Plus Linear (MPL) systems, a class of continuous-space, discrete-event models defined over the max-plus algebra. Given the…
eess.SY2020
Computation of the Transient in Max-Plus Linear Systems via SMT-Solving
Alessandro Abate, Alessandro Cimatti, Andrea Micheli +1
This paper proposes a new approach, grounded in Satisfiability Modulo Theories (SMT), to study the transient of a Max-Plus Linear (MPL) system, that is the number of steps leading…
cs.LO2019
Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions
Muhammad Syifa'ul Mufid, Dieky Adzkiya, Alessandro Abate
This paper introduces the abstraction of max-plus linear (MPL) systems via predicates. Predicates are automatically selected from system matrix, as well as from the specifications…