Provably Correct Fleet Operations and Vehicle SoS Integration with Assume-Guarantee Contracts

Project #5.28 begins 2026.

This project will develop theory and software to support the analysis and synthesis of vehicle fleets with provable guarantees of performance and safe SoS integration. This work will be based on the recently-introduced algebra of contracts.

Consider a collection of vehicles and human agents in a contested environment, each of them having certain capabilities. Given a mission to be accomplished, the problem is to enlist resources and assign them tasks to complete it, considering the capabilities and individual objectives of participants and adversaries. Addressing this problem generates the following research objectives:

Problem 1: extending the theory of contracts to reason about probability. Unmodeled dynamics, environment uncertainty, and the employment of data-driven components in complex systems require us to reason about probabilities in system design. The state of the art of support for probabilities in the algebra of contracts is limited to the manipulation of bounded probability. For example, consider the use of contracts to compute the specification of the perception component of a vehicle to make it satisfy a safety property with a desired probability bound. However, algorithms to compute the algebraic operations of contracts with probabilistic specifications do not exist. Developing this technology will enable us to relate the uncertainty of the system to that of its components and to be able to compute the likelihood of success of a given mission.

Problem 2: modeling vehicle capabilities for fleet analysis and design. Enlisting a vehicle in a fleet that has to satisfy a given mission requires the representation of the capabilities of each vehicle as a contract. In order to analyze teaming, the contracts generated for the vehicles have to contain enough information to enable us to answer whether the corresponding fleet satisfies the intended objectives. The representation of vehicle capabilities as contracts for fleet analysis and design is novel work.

Problem 3: provably correct mission design in contested environments. Suppose a mission has to be satisfied by enlisting agents that come with their own interests (e.g., other organizations, nations, etc.) and that must be performed amidst agents with conflicting interests. In this case, we must analyze the incentive mechanisms that must be designed to motivate agents to enlist their capabilities to benefit the fleet while satisfying their goals and to be robust against the strategic behavior of the antagonistic agents. The compositional analysis of such a mission requires the merger of the algebra of contracts with game theory. This is a novel direction of research that has not been pursued.

5.28