# Formal Synthesis of Control Strategies for Positive Monotone Systems

## TL;DR

This paper presents a formal method for synthesizing control strategies for positive monotone systems using signal temporal logic, formulating the problem as a MILP and applying it to traffic management scenarios.

## Contribution

It introduces a MILP-based approach for control synthesis for positive monotone systems with STL specifications, establishing conditions where open-loop controls suffice and developing a robust predictive framework.

## Key findings

- Control policies can be synthesized via MILP for STL specifications.
- Open-loop control policies are often sufficient for satisfaction.
- Application to traffic management demonstrates practical effectiveness.

## Abstract

We design controllers from formal specifications for positive discrete-time monotone systems that are subject to bounded disturbances. Such systems are widely used to model the dynamics of transportation and biological networks. The specifications are described using signal temporal logic (STL), which can express a broad range of temporal properties. We formulate the problem as a mixed-integer linear program (MILP) and show that under the assumptions made in this paper, which are not restrictive for traffic applications, the existence of open-loop control policies is sufficient and almost necessary to ensure the satisfaction of STL formulas. We establish a relation between satisfaction of STL formulas in infinite time and set-invariance theories and provide an efficient method to compute robust control invariant sets in high dimensions. We also develop a robust model predictive framework to plan controls optimally while ensuring the satisfaction of the specification. Illustrative examples and a traffic management case study are included.