Synthesizing Skeletons for Reactive Systems

TL;DR

This paper introduces a novel analysis technique called skeletons for reactive systems, which visualizes which parts of a system's implementation are determined or still open based on temporal specifications, aiding in verification and synthesis.

Contribution

It presents algorithms for verifying and learning skeletons from LTL specifications, enabling better understanding and repair of underspecified reactive system requirements.

Findings

Skeletons represent output possibilities with three-valued logic.

Algorithms efficiently verify and synthesize skeletons from LTL specifications.

Technique helps identify and fix underspecified critical system behaviors.

Abstract

We present an analysis technique for temporal specifications of reactive systems that identifies, on the level of individual system outputs over time, which parts of the implementation are determined by the specification, and which parts are still open. This information is represented in the form of a labeled transition system, which we call skeleton. Each state of the skeleton is labeled with a three-valued assignment to the output variables: each output can be true, false, or open, where true or false means that the value must be true or false, respectively, and open means that either value is still possible. We present algorithms for the verification of skeletons and for the learning-based synthesis of skeletons from specifications in linear-time temporal logic (LTL). The algorithm returns a skeleton that satisfies the given LTL specification in time polynomial in the size of the minimal skeleton. Our new analysis technique can be used to recognize and repair specifications that underspecify critical situations. The technique thus complements existing methods for the recognition and repair of overspecifications via the identification of unrealizable cores.