The paper is authored by Rüdiger Ehlers, who heads the ACPS research group of the Institute of Software and Systems Engineering of TU Clausthal. It deals with the problem of fostering the understandability of reactive system implementations that were automatically synthesized from their specification. More concretely, the paper describes a new method to compute *invariants* that all synthesized systems that conform to a given specification must fulfill. These invariants then document how a system needs to behave in order to be correct. Such documentation is then useful for the integration of the synthesized controller into a bigger system and for later maintenance of the integrated system.
The paper is open access and can be read at https://doi.org/10.1007/978-3-031-71162-6_9. An implementation of the new approach presented in the paper is available as open source as part of the reactive synthesis tool slugs, which can be obtained from https://github.com/verifiablerobotics/slugs.
Distinguished Paper Award
The paper "Understanding Synthesized Reactive Systems Through Invariants" was awarded the *distinguished paper* recognition at the 26th International Symposium International Conference on Formal Methods, which took place from the 11th to 13th September 2024 in Milano, Italy.
