MAPOTA is a one-year project, running in 2027 and funded by the Graduate School of Computer Science of Paris-Saclay University.
Model checking, that is, the formal specification and verification of computing systems, has seen lots of advances and applications in the last three decades. Nowadays, it is part of the design process of critical systems in industry.
Of particular interest is the model checking of real-time systems, where timing information and constraints play a decisive role. Here, timed automata have emerged as a formalism which is sufficiently expressive to be useful in industry and at the same time amenable to automatic verification. However, even for state-of-the-art tools such as Uppaal or TChecker, timed-automata model checking is at the very boundary of what modern computers can handle, so research into better algorithms and new paradigms in this area has great impact potential.
The goal of the MAPOTA project is to explore the use of max-plus polyhedra in the model checking of timed automata and to evaluate potential algorithmic improvements in precision and scalability.