# Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions

## TL;DR

This paper presents a new predicate abstraction approach for max-plus linear systems, enabling efficient bounded model checking of time-difference specifications and providing explicit bounds on verification completeness.

## Contribution

It introduces an automatic predicate abstraction method for MPL systems and enhances BMC with explicit completeness bounds based on system properties.

## Key findings

- Predicate abstractions improve verification efficiency.
- Explicit bounds on completeness threshold are derived.
- Experimental results show superiority over existing algorithms.

## Abstract

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 under consideration. We focus on verifying time-difference specifications, which encompass the relation between successive events in MPL systems. We implement a bounded model checking (BMC) procedure over a predicate abstraction of the given MPL system, to verify the satisfaction of time-difference specifications. Our predicate abstractions are experimentally shown to improve on existing MPL abstractions algorithms. Furthermore, with focus on the BMC algorithm, we can provide an explicit upper bound on the completeness threshold by means of the transient and the cyclicity of the underlying MPL system.