Source-linked AI summary
From Spot 2.0 to Spot 2.10: What's New?
Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, Henrich Lauko
TL;DR
Some Spot 2.0 algorithms could not handle arbitrary acceptance conditions, limiting the library's support for those automata. This paper describes Spot's evolution, including its graph representation, Python interface, and support for alternating automata. It also identifies a constraint on parallel processing: BuDDy is not thread safe.
Problem
In Spot 2.0, some algorithms could read automata with arbitrary acceptance conditions but could not operate on all of them.
Source: §1 · p. 1Method
Results
Spot's twa_graph uses integer-designated states and edges, and its alternating-automata support represents universal branching through destination groups.
Source: §3 · p. 4Takeaways & Limitations
A web application built using Spot supports LTL teaching and serves as a research tool for formula properties and comparisons.
Source: §7 · p. 9BuDDy is inherently not thread safe, preventing parallel processing on automata.
Source: §8 · p. 11
Abstract
from arXiv · showhide
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.
1 Availability, Purpose, and Evolution
Spot provides LTL and ω-automata functionality through a C++17 library, command-line tools, and Python bindings. Since Spot 2.0 introduced arbitrary acceptance conditions, the library has expanded its algorithms and accumulated 56 releases, including 10 major releases.
1 Availability, Purpose, and Evolution
- Spot is available as a C++17 library, command-line tools, and Python bindings, and is distributed under GPLv3.Packages are available for several Linux distributions and Conda-Forge, among others.Source: §1 · p. 1
- Spot 2.0 introduced support for ω-automata with arbitrary Emerson-Lei acceptance conditions, expressed using Fin and Inf color constraints.At that point, not all algorithms handled the full generality of those conditions.Source: §1 · p. 1
- A generic emptiness check replaced the need to use remove_fin() for automata whose acceptance conditions were not Fin-less.Arbitrary acceptance support also enabled Alternating Cycle Decomposition, with applications including parity conversion, degeneralization, and typeness checks.Source: §1 · p. 2
- Spot has had 56 releases since version 2.0, of which 10 are major releases that add features.The paper's release highlights omit many micro-optimizations and usability improvements.Source: §1 · p. 2
2 Use-cases of Spot, and Related Tools
Spot is used to translate LTL formulas into automata and as a research and development toolbox. Its Python interface and compatibility with related tools support a range of research and application workflows.
2 Use-cases of Spot, and Related Tools
- Spot is used to translate LTL formulas into automata and as a toolbox for formula and automaton generation, verification, simplification, and syntax conversion.It is also used as a baseline for research on ω-automata algorithms and in newer applications [e.g., 33, 32, 25, 18; 12, 13].Source: §2 · pp. 2, 4
- Owl and Spot share a command-line workflow built around chained commands and communicate via the HOA format, while GOAL centers on graphical automaton editing.GOAL can also be used from the command line through scripts in a custom language.Source: §2 · p. 4
- Spot's Python interface exposes algorithms and data structures, allowing users to leverage Python's ecosystem and prototype algorithms quickly.The paper identifies this as Spot's most important interfacing feature.Source: §2 · p. 4
3 Automata Representation
Spot's twa_graph stores an explicit automaton using integer-indexed states and edges, while twa provides an on-the-fly exploration interface. The graph representation combines successor lists with edge records and stores properties that algorithms can exploit.
3 Automata Representation
- twa offers an abstract on-the-fly interface for querying the initial state and transitions from known states, without first knowing how many states are reachable.Subclasses can represent Promela or Divine state spaces, and users can create subclasses for structures such as Kripke structures.Source: §3 · p. 4
- twa_graph stores an explicit automaton as two C++ vectors: a state vector holding first and last outgoing-edge indices, and an edge vector holding edge fields and successor links.The linked successor lists use edge 0 as a terminator; outgoing edges of a state need not be adjacent in the edge vector.Source: §3 · pp. 4–5
- twa_graph assigns integer identifiers to states and edges, which can simplify interfaces and let algorithms use them as array indices.The graph class was introduced in Spot 2.0.Source: §3 · p. 4
- Automata store structural-property fields that algorithms can read and use as hints, but in-place modifications must update them to avoid bugs.For example, knowing that an automaton is weak lets product() use fewer colors.Source: §3 · pp. 5–6
4 Introduction of Alternating Automata
Spot added alternating ω-automata support by extending twa_graph rather than introducing a new class. Its representation encodes universal destination groups, and its alternation-removal procedures use breakpoint and powerset constructions in different settings.
4 Introduction of Alternating Automata
- Spot added alternating ω-automata in version 2.3 by reserving the sign bit of a transition's destination to mark universal branching, without changing algorithms for automata without it.Algorithms can use univ_dests() to iterate through the destinations of an edge.Source: §4 · p. 6
- Universal destination groups are stored in a destinations vector and identified by signed destination values; the figure renders them in pink.The complement of a signed value indexes the group, whose stored size is followed by its destination state numbers.Source: §4 · p. 6, Figure 2 · p. 7
- Spot's mixed alternation-removal approach uses the powerset construction for very weak automata in the relevant SCC cases, and that construction is known to work for ordered automata.Ordered automata have only self-loops as rejecting cycles.Source: §4 · p. 7
- The second alternation-removal procedure takes a weak automaton and combines breakpoint construction on rejecting SCCs with more than one state and powerset construction on other SCCs.Spot also has an on-the-fly Breakpoint construction for alternating Büchi automata, producing a non-alternating Büchi automaton with at most 3n states.Source: §4 · p. 7
5 Extending Automata via Named Properties
Spot’s named properties let users attach extra data to automata, supporting both metadata and algorithm byproducts, with type correctness left to the programmer.
5 Extending Automata via Named Properties
- Named properties attach arbitrary data to an automaton through set_named_prop and retrieve it by name with get_named_prop.The programmer is responsible for ensuring the retrieved property has the correct type.Source: §5 · p. 8
- Properties include display metadata such as automaton names and highlights, as well as algorithm byproducts such as product-states pairs of original states.Source: §5 · p. 8
- Named properties can also provide additional semantics that let an automaton represent a game or a Mealy machine.Source: §5 · p. 8
6 Games, Mealy Machines, and LTL Synthesis
Spot’s LTL synthesis tool, ltlsynt, was introduced in version 2.5, and its inner workings were progressively redesigned and publicly exposed through version 2.10.
6 Games, Mealy Machines, and LTL Synthesis
- Spot introduced ltlsynt in version 2.5 and progressively redesigned and exposed its inner workings through version 2.10.Source: §6 · p. 8
- Games are represented by the state-player property and are limited to two players; Spot solves safety games and parity max odd games.Solving adds state-winner and strategy properties to identify each state’s winner and the edge its owner should follow.Source: §6 · p. 8
- A solved game’s winning strategy can be extracted as a Mealy machine and encoded as an AIGER circuit, with synthesis-output specifying output propositions.The game example distinguishes winning regions and strategies for the two players.Source: §6 · pp. 8–9, Figure 3 · p. 9
7 Online Application for LTL Formulas
Spot’s web application provides browser access to selected LTL and automata features and serves both teaching and research.
7 Online Application for LTL Formulas
- The web application transforms LTL formulas into automata, displays formula properties, and compares formulas with a Venn diagram.Its property views include hierarchy membership, safety/liveness classification, Rabin and Streett indices, and stutter-invariance.Source: §7 · p. 9, Figure 4 · p. 10
- Built using a React frontend with Spot running on the server, the web application exposes a subset of Spot’s features.Source: §7 · p. 9, Figure 4 · p. 10
- The application has been found useful for teaching about LTL and its relation to automata, as well as for research.Source: §7 · p. 9
8 Shortcomings and one Future Direction
Spot’s edge representation has memory and color-count constraints, while its use of BDD labels limits parallel processing and motivates an experimental alternative.
8 Shortcomings and one Future Direction
- Each edge takes 20 bytes: its acceptance colors use a 32-bit bit-vector, its label a 32-bit BDD identifier, and three other fields 32-bit integers.Source: §8 · p. 10
- The 32-color limit can be reached easily; enlarging it at compile time increases per-edge memory and runtime, so algorithms aim to avoid unnecessary colors.For weak automata, product() may produce fewer than x+y colors when combining automata with x and y colors.Source: §8 · p. 10
- BuDDy’s global unicity table and caches make it inherently non-thread-safe, preventing parallel processing on automata.Spot uses a customized BuDDy with more compact BDD nodes and recursion-free rewrites for most operations.Source: §8 · pp. 10–11
- Spot’s experimental twacube represents edges as cubes using two bit-vectors and is used in some parallel emptiness checks.Source: §8 · p. 11