A Component-oriented Framework for Autonomous Agents

TL;DR

This paper introduces a component-oriented, automaton-based framework for designing autonomous agents, enabling compositional reasoning about system behavior with preferences and formal verification using extended Linear Temporal Logic.

Contribution

It presents a novel automaton-based paradigm incorporating preferences for compositional design and extends Linear Temporal Logic for diagnosing undesired behaviors in autonomous systems.

Findings

Framework supports compositional design of autonomous agents.

Extended Linear Temporal Logic aids in diagnosing undesired behaviors.

Preferences provide fallback mechanisms at runtime and reasoning tools at design-time.

Abstract

The design of a complex system warrants a compositional methodology, i.e., composing simple components to obtain a larger system that exhibits their collective behavior in a meaningful way. We propose an automaton-based paradigm for compositional design of such systems where an action is accompanied by one or more preferences. At run-time, these preferences provide a natural fallback mechanism for the component, while at design-time they can be used to reason about the behavior of the component in an uncertain physical world. Using structures that tell us how to compose preferences and actions, we can compose formal representations of individual components or agents to obtain a representation of the composed system. We extend Linear Temporal Logic with two unary connectives that reflect the compositional structure of the actions, and show how it can be used to diagnose undesired behavior by tracing the falsification of a specification back to one or more culpable components.