Satisfiability and Canonisation of Timely Constraints

TL;DR

This paper models and analyzes the problem of satisfying timing constraints in multi-agent systems using graph theory, providing characterizations, algorithms, and canonical forms for efficient coordination.

Contribution

It introduces a graph-theoretic framework for satisfiability of timely constraints, reducing the problem to shortest-path and negative cycle detection, and constructs canonical representatives for constraint classes.

Findings

Satisfiability characterized by all-pairs shortest paths.

Existence of minimal satisfying functions for constraints.

Reduction of classification and comparison to shortest-path problems.

Abstract

We abstractly formulate an analytic problem that arises naturally in the study of coordination in multi-agent systems. Let I be a set of arbitrary cardinality (the set of actions) and assume that for each pair of distinct actions (i,j), we are given a number \delta(i,j). We say that a function t, specifying a time for each action, satisfies the timely constraint {\delta} if for every pair of distinct actions (i,j), we have t(j)-t(i) <= \delta(i,j) (and thus also t(j)-t(i) >= -\delta(j,i)). While the approach that first comes to mind for analysing these definitions is an analytic/geometric one, it turns out that graph-theoretic tools yield powerful results when applied to these definitions. Using such tools, we characterise the set of satisfiable timely constraints, and reduce the problem of satisfiability of a timely constraint to the all-pairs shortest-path problem, and for finite I, furthermore to the negative-cycle detection problem. Moreover, we constructively show that every satisfiable timely constraint has a minimal satisfying function - a key milestone on the way to optimally solving a large class of coordination problems - and reduce the problem of finding this minimal satisfying function, as well as the problems of classifying and comparing timely constraints, to the all-pairs shortest-path problem. At the heart of our analysis lies the constructive definition of a "nicely-behaved" representative for each class of timely constraints sharing the same set of satisfying functions. We show that this canonical representative, as well as the map from such canonical representatives to the the sets of functions satisfying the classes of timely constraints they represent, has many desired properties, which provide deep insights into the structure underlying the above definitions.