Qualitative Approximate Behavior Composition
This work addresses the problem of coordinating available components to approximate a desired target system, making it applicable to a wider range of cases, though it is incremental as it builds on classical settings without a new paradigm.
The paper tackles the behavior composition problem by developing an approach for approximate behavior composition, which allows for building controllers even when exact solutions are unsolvable, and shows how to compute maximal controllers and optimal approximations using ATL model checking.
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.