Soft component automata: Composition, compilation, logic, and verification

The design of a complex system warrants a compositional methodology, i.e., composing simple components to obtain a system that meaningfully exhibits their collective behavior. 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 algebraic structures on preferences and actions, we can compose formal representations of individual components or agents to obtain a representation of the composed system, exhibiting intuitively meaningful behavior.

We extend linear temporal logic with two unary connectives that reflect the compositional structure of actions, and show that it is decidable whether all behaviors of a given automaton satisfy a formula of this extended logic. We then show how this logic can be used to diagnose undesired behavior by tracing the falsification of a specification back to one or more culpable components. Lastly, we implement a toolchain that compiles our automata to Maude, allowing us to apply the rich model checking capability of Maude to verify agent behavior.