Qualitative Approximate Behavior Composition

TL;DR

This paper introduces a novel approach for approximate behavior composition using simulation, enabling the construction of controllers that closely approximate target behaviors in cases where exact realization is impossible.

Contribution

It develops a framework for approximate behavior composition based on simulation, extending classical methods to handle unsolvable problems and computing optimal approximations via ATL model checking.

Findings

Maximal controllers and closest target modules are characterized.

Optimal approximations are shown to be unique.

The approach is sound and complete with respect to imported controllers.

Abstract

The behavior composition problem involves automatically building a controller that is able to realize a desired, but unavailable, target system (e.g., a house surveillance) by suitably coordinating a set of available components (e.g., video cameras, blinds, lamps, a vacuum cleaner, phones, etc.) Previous work has almost exclusively aimed at bringing about the desired component in its totality, which is highly unsatisfactory for unsolvable problems. In this work, we develop an approach for approximate behavior composition without departing from the classical setting, thus making the problem applicable to a much wider range of cases. Based on the notion of simulation, we characterize what a maximal controller and the "closest" implementable target module (optimal approximation) are, and show how these can be computed using ATL model checking technology for a special case. We show the uniqueness of optimal approximations, and prove their soundness and completeness with respect to their imported controllers.