Biblio

Abstract We present an efficient computational procedure for finite abstraction of discrete-time mixed monotone systems by considering a rectangular partition of the state space. Mixed monotone systems are decomposable into increasing and decreasing components, and significantly generalize the well known class of monotone systems. We tightly overapproximate the one-step reachable set from a box of initial conditions by computing a decomposition function at only two points, regardless of the dimension of the state space. We first consider systems with a finite set of operating modes and then extend the formulation to systems with continuous control inputs. We apply our results to verify the dynamical behavior of a model for insect population dynamics and to synthesize a signaling strategy for a traffic network.

Abstract We study the problem of selecting offsets of the traffic signals in a network of signalized intersections to reduce queues of vehicles at all intersections. The signals in the network have a common cycle time and a fixed timing plan. It is assumed that the exogenous demands are constant or periodic with the same period as the cycle time and the intersections are under-saturated. The resulting queuing processes are periodic. These periodic processes are approximated by sinusoids. The sinusoidal approximation leads to an analytical expression of the queue lengths at every intersection as a function of the demands and the vector of offsets. The optimum offset vector is the solution of a quadratically constrained quadratic program (QCQP), which is solved via its convex semidefinite relaxation. Unlike existing techniques, our approach accommodates networks with arbitrary topology and scales well with network size. We illustrate the result in two case studies. The first is an academic example previously proposed in the literature, and the second case study consists of an arterial corridor network in Arcadia, California.

We study the control of monotone systems when the objective is to maintain trajectories in a directed set (that is, either upper or lower set) within a signal space. We define the notion of a directed alternating simulation relation and show how it can be used to tackle common bottlenecks in abstraction-based controller synthesis. First, we develop sparse abstractions to speed up the controller synthesis procedure by reducing the number of transitions. Next, we enable a compositional synthesis approach by employing directed assume-guarantee contracts between systems. In a vehicle traffic network example, we synthesize an intersection signal controller while dramatically reducing runtime and memory requirements compared to previous approaches.