Synthesizing Skeletons for Reactive Systems
This work addresses the challenge of underspecification in reactive systems for developers and verification engineers, complementing existing methods for overspecification repair.
The paper tackles the problem of identifying which parts of a reactive system's implementation are fixed by its temporal specification and which remain flexible, representing this information as a labeled transition system called a skeleton. It presents algorithms for verifying and synthesizing skeletons from LTL specifications in polynomial time relative to the minimal skeleton size, enabling recognition and repair of underspecified critical situations.
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.