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…