Formal Analysis and Verification of Max-Plus Linear Systems

TL;DR

This paper introduces a new logical framework and optimized verification methods for Max-Plus Linear systems, enabling automatic analysis of their properties with improved efficiency and expressiveness.

Contribution

It proposes Time-Difference LTL (TDLTL) for specifying properties of MPL systems and develops both model checking and SMT-based approaches for their verification.

Findings

The SMT-based approach outperforms traditional model checking in efficiency.

The proposed methods handle complex temporal properties of MPL systems.

Experimental results demonstrate significant improvements over existing techniques.

Abstract

Max-Plus Linear (MPL) systems are an algebraic formalism with practical applications in transportation networks, manufacturing and biological systems. In this paper, we investigate the problem of automatically analyzing the properties of MPL, taking into account both structural properties such as transient and cyclicity, and the open problem of user-defined temporal properties. We propose Time-Difference LTL (TDLTL), a logic that encompasses the delays between the discrete time events governed by an MPL system, and characterize the problem of model checking TDLTL over MPL. We first consider a framework based on the verification of infinite-state transition systems, and propose an approach based on an encoding into model checking. Then, we leverage the specific features of MPL systems to devise a highly optimized, combinational approach based on Satisfiability Modulo Theory (SMT). We experimentally evaluate the features of the proposed approaches on a large set of benchmarks. The results show that the proposed approach substantially outperforms the state of the art competitors in expressiveness and effectiveness, and demonstrate the superiority of the combinational approach over the reduction to model checking.