From Spot 2.0 to Spot 2.10: What's New?

TL;DR

This paper reviews the six-year evolution of the Spot library, highlighting new features like acceptance transformations, alternating automata, and LTL synthesis, demonstrating its expanding capabilities in automata manipulation.

Contribution

It provides a comprehensive overview of the recent developments and new functionalities added to the Spot library since version 2.0, emphasizing its advancements.

Findings

Added support for acceptance transformations

Introduction of alternating automata and games

Enhanced LTL synthesis features

Abstract

Spot is a C ++ 17 library for LTL and $\omega$-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support $\omega$-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more. We also shed some lights on the data-structure used to store automata.