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.
Artifact: https://zenodo.org/record/6521395.
M. Colange, A. Gbaguidi Aisse, T. Medioni, C. Gillard and H. Lauko—Previously at LRDE.
You have full access to this open access chapter, Download conference paper PDF
Similar content being viewed by others
1 Availability, Purpose, and Evolution
Spot is a library for LTL and \(\omega \)-automata manipulation, distributed under a GPLv3 license. Its source code is available from https://spot.lrde.epita.fr/. We provide packages for some Linux distributions like Debian and Fedora, but other packages can also be found for Conda-Forge [17] (for Linux & Darwin), Arch Linux, FreeBSD...
Spot can be used via three interfaces: a C++17 library, a set of command-line tools that give easy access to many features of the library, and Python bindings, that makes prototyping and interactive work very attractive. Our web site now contains many examples of how to perform some tasks using these three interfaces, and we have a public mailing list for questions.
In our last tool paper [21], Spot 2.0 had just converted from being a library for working on Transition-based Generalized Büchi Automata and had become a library supporting \(\omega \)-automata with arbitrary Emerson-Lei [22, 41] acceptance conditions, as enabled by the development of the HOA format [5].
In the HOA format, transitions can carry multiple colors, and acceptance conditions are expressed as a positive Boolean formulas over atoms like \(\mathsf {Fin}(i)\) or \(\mathsf {Inf}(i)\) that tell if a color should be seen finitely or infinitely often for a run to be accepting. Table 1 gives some examples.
While Spot 2.0 was able to read automata with arbitrary acceptance conditions, not all of its algorithms were able to support such a generality. For instance testing an automaton for emptiness or finding an accepting word, would only work on automata with “\(\mathsf {Fin}\)-less” acceptance conditions. For other conditions, Spot 2.0 would rely on a procedure called remove_fin() to convert automata with arbitrary acceptance conditions into “\(\mathsf {Fin}\)-less” acceptance conditions [9]. This was ultimately fixed by developing a generic emptiness check [6]. Additionally the support for arbitrary acceptance conditions has allowed us to implement many useful algorithms; the most recent being the Alternating Cycle Decomposition [15, 16] a powerful data structure with many applications (conversion to parity acceptance, degeneralization, typeness checks...)Footnote 1.
There have been 56 releases of Spot since version 2.0, but only 10 of these are major releases. Releases are numbered 2.x.y where y is updated for minor upgrades that mostly fix bugs, and x is updated for major release that add new features. (The leading 2 would be incremented in case of a serious redesign of the API.) Table 2 summarizes the highlights of the various releases in chronological order. Not appearing in this list are many micro-optimizations and usability improvements that Spot has accumulated over the years.
2 Use-cases of Spot, and Related Tools
As it is a library, there are many ways to use Spot. We are mostly aware of such uses via citationsFootnote 2. Historical and frequent uses-cases are to use Spot for translating LTL formulas to automata (Winners of the sequential LTL and parallel LTL tracks of RERS’19 challenge [26] both used Spot to translate the properties into automata, many competitors on the Model Checking Contest [28] also use Spot this way), or to use it as a research/development toolbox, since it provides helper tools for generation of random formulas/automata, verification of LTL-to-automata translation, simplifications, syntax conversions, etc. Nowadays, the algorithms for \(\omega \)-automata implemented in Spot are often used as baseline for studying better algorithms [e.g., 25, 32, 18, 33], but we also see some new applications built on top of \(\omega \)-automata algorithms from Spot [e.g., 12, 13].
The projects that have the largest intersections of features with Spot seem to be GOAL [43] and Owl [30]. These are two Java-based frameworks that deal with similar objects and provide a range of algorithms. Owl and Spot share a similar and traditional Unix view of the command-line experience, where multiple commands are expected to be chained with pipes, and they both communicate smoothly via the HOA format [5]. GOAL is centered on a graphical interface in which the user can edit automata, and apply algorithms listed in menu entries. Using GOAL from the command-line is possible by writing short scripts in a custom language.
As far as interfacing goes, the most important feature of Spot is probably that it exposes its algorithms and data structures in Python. Beside being usable as a glue language between various tools, this allows us (1) to leverage Python’s ecosystem and (2) to quickly prototype new algorithms in Python.
3 Automata Representation
In this section and the next three, we focuses on how the storage of automata evolved to support alternation, games, and Mealy machines.
The main automaton class of Spot is called twa_graph and inherits from the twa class. The letters twa stand for Transition-based \(\omega \)-Automaton.
The class twa implements an abstract interface that allows on-the-fly exploration of an automaton similar to what had been present in Spot from the start: essentially, one can query the initial state, and query the transitions leaving any known state. In particular, before exploring the state-space of a twa, it is unknown how many states are reachable. Various subclasses of twa are provided in Spot, for instance to represent the state-space of Promela or Divine models [21]. Users may create subclasses, for instance to create a Kripke structure on-the-fly.Footnote 3
The class twa_graph, introduced in Spot 2.0, implements an explicit, graph-based, representation of an automaton, in which states and edges are designated by integers. This makes for a much simpler interfaceFootnote 4 and usually simplifies the data structures used in algorithms (since states and edges can be used as indices in arrays). The data structure is best illustrated by using the show_storage() method of the Python bindings, as shown by Fig. 1. A twa_graph is stored as two C++ vectors: a vector of states, and a vector of edges. For each state, the first vector stores two edge numbers: succ is the first outgoing edge, and succ_tail is the last one. These number are indices into the edge vector, which stores five pieces of information per edge. Four of them are related to the identity of the edge: src, dst, cond, acc are respectively the source, destination, guard, and color sets of the edge. The remaining field, next_succ gives the next outgoing edge, effectively creating a linked list of all edges leaving a given state. There is no edge 0: this value is used as terminator for such lists. Outgoing edges of the same state are not necessarily adjacent in that structure. When a new edge is added to the automaton, it is simply appended to the edge vector, and the succ_tail field of the state is used to update the previous end of the list.
To iterate over successors of state 1 in C++ or Python, one can ignore the above linked list implementation and write one of the following loops:
The twa_graph::out methods simply returns a lightweight temporary object which can be iterated upon using iterators that will follow the linked list. Then the object e is effectively a reference to a column of the edge vector.
As seen on Fig. 1, the automaton additionally stores an initial state (Spot only supports a single initial state), a number of colors (num_sets), an acceptance condition, a list of atomic propositions (Spot only supports alphabets of the form \(2^{ AP }\)), and 10 fields storing structural properties of the automaton.
These property fields have only three possible values: they default to maybe, but can be set to no or yes by algorithms that work on the automaton. They can also be read and written in the HOA format. For instance if prop_universal is set to yes, it means that automaton does not have any existential choice (a.k.a. non-determinism). Spot’s is_deterministic() algorithm can return in constant time if prop_universal is known, otherwise it will inspect the automaton and set that property before returning, so that the next call to is_deterministic() will be instantaneous. Some algorithms know how to take advantage of any hint they get from those properties: for instance the product() of two automata is optimized to use fewer colors when one of the arguments is known to be weak (i.e., in an SCC all transitions have the same colors).
Note that algorithms that modify an automaton in place have to remember to update those properties. This has caused a couple of bugs over the years.
4 Introduction of Alternating Automata
Support for alternating \(\omega \)-automata, as defined in the HOA format, was added to Spot in version 2.3 without introducing a new class. Rather, the twa_graph class was extended to support alternation in such a way that existing algorithms would not require any modification to continue working on automata without universal branching. This was done by reserving the sign bit of the destination state number of each transition to signal universal branching.
Figure 2 shows an example of Alternating automaton (top-left) with co-Büchi acceptance. In many works on alternating automata, it is conventional to not represent accepting sinks, and instead have transition without destination. The top-right picture shows that Spot has a rendering option to hide accepting sinks.
The bottom of the figure shows that the automaton has prop_state_acc set, which means that the automaton is meant to be interpreted as using state-based acceptance. Colors are still stored on edges internally, but all edges leaving a state have the same colors. Seeing that the condition is co-Büchi (\(\mathsf {Fin}(0)\)), the display code automatically switched to the convention of using double-circles for rejecting states.
Destinations with the sign bit set are called universal destination groups and appear as pink in the figure. There are two groups here: ~0 and ~3. The complement of these numbers can be used as indices in the dests vector, that actually store the destination groups. At the given index, one can read the size n of the destination group, followed by the state number of the n destinations.
Algorithms that work on alternating automata need to be able to iterate over all destinations of an edge. The process of checking the sign bit of the destination to decide if its a group, and to iterate on that group is hidden by the univ_dests() method:
Note that this code works on non-universal branches as well: if e.dst is unsigned, univ_dests(e) will simply iterate on that unique value.
Spot has two alternation removal procedures. One is an on-the-fly implementation of the Breakpoint construction [37] which transforms an n-state alternating Büchi automaton into a non-alternating Büchi automaton with at most \(3^n\) states. For very weak alternating automata, it is known that a powerset-based procedure can produce a transition-based generalized Büchi automaton with \(2^n\) states [23]; in fact that algorithm even works on ordered automata [11], i.e., alternating automata where the only rejecting cycles are self-loops. The second alternation removal procedure of Spot is a mix between these two procedures but does not work on the fly: it takes a weak automaton as input, and uses the break-point construction on rejectings SCCs that have more than one state, and uses the powerset construction for other SCCs.
5 Extending Automata via Named Properties
Spot’s automata have a mechanism to attach arbitrary data to automata, called named properties. (This is similar to the notion of attributes in the R language.) An object can be attached to the automaton with:
and later retrieved with:
Ensuring that mytype is the correct type for the retrieved property is the programmer’s responsibility.
Spot has grown a list of many such properties over time.Footnote 5 For instance automaton-name stores a string that would be displayed as the name of the automaton. The highlight-edges and highlight-states properties can be used to color edges and states. The state-names is a vector of strings that gives a name to each state, etc. While those examples are mostly related to the graphical rendering of the automata, some algorithms store useful byproducts as properties. For instance the product() algorithm will define a product-states named property that store a vector of pairs of the original states.
These named properties are sometimes used to provide additional semantics to the automaton, for instance to obtain a game or a Mealy machine.
6 Games, Mealy Machines, and LTL Synthesis
The application of Spot to LTL synthesis was introduced in Spot 2.5 in the form of the ltlsynt tool [35], but the inner workings of this tool were progressively redesigned and publicly exposed until version 2.10.
An automaton can now be turned into a game by attaching the state-player property to it.Footnote 6 Only two-player games are supported, so state-player should be a \(\texttt {std::vector<bool>}\). Currently, Spot has solvers for safety games and for games with parity max odd acceptance, but we plan to at least generalize the latter to any kind of parity condition. Once a game has been solved, it contains two new named properties: state-winner (a \(\texttt {std::vector<bool>}\) indexed by state numbers indicating the player winning in each state), and strategy (a \(\texttt {std::vector<unsigned>}\) that gives for each state the edge that its owner should follow to win).
Figure 3 shows an example of game generated by ltlsynt, and how we can display the winning strategy once the game is solved. The winning strategy can be extracted and converted into a Mealy machine, which is just an automaton that uses the synthesis-output property to specify which atomic propositions belong to the output. Such a Mealy machine can then be encoded into an AND-inverter graph, and saved into the AIGER format [7]. Here L0 represents a latch, i.e., one bit of memory, that stores the previous value of a so that the circuit can output b if and only if a is true in the present and in the previous step.
7 Online Application for LTL Formulas
The Python ecosystem makes it easy to develop web interfaces for convenient access to a subset of features of Spot. For instance Fig. 4 shows screenshots of a web application built using a React frontend, and running Spot on the server. It can transform LTL formulas into automata, can display many properties of a formula (membership to the Manna & Pnueli hierarchy [34], Safety/Liveness classification [2], Rabin and Streett indices [14], stutter-invariance [36]), or simply compare two formulas using a Venn diagram.
This application has been found to be useful for teaching about LTL and its relation with automata, but is also a helpful research tool.
8 Shortcomings and One Future Direction
While Spot has been used for many applications, there are two recurrent issues: they are related to the types used for some fields of the edge vector (see Figs. 1–2). By default, the set of colors that labels an edge (the acc field) is stored as a 32-bit bit-vector, the transition label (cond, a formula over \(2^ AP \)), is stored as a BDD identified by a unique 32-bit integer, and the other three fields (src, dst, next_succ) are all 32-bit integers. One edge therefore takes 20 bytes.
While limiting the number of states to 32-bit integers has never been a problem so far, the limit of 32 colors can be hit easily. Spot 2.6 added a compile-time option to enlarge the number of supported colors to any multiple of 32; this evidently has a memory cost (and therefore also a runtime cost) as the acc field will be larger for each edge. However this constraint generally means that all the algorithms we implement try to be “color-efficient”, i.e., to not introduce useless colors. For instance while the product of an automaton with x colors and an automaton with y colors is usually an automaton with \(x+y\) colors, the product() implementation will output fewer colors in presence of a weak automaton.
The use of BDDs as edge labels causes another type of issues. Spot uses a customized version of the BuDDy library, with additional functions, and several optimizations (more compact BDD nodes for better cache friendliness, most operations have been rewritten to be recursion-free). However BuDDy is inherently not thread safe, because of its global unicity table and caches. This prevents us from doing any kind of parallel processing on automata. A long term plan is to introduce a new class twacube that represent an automaton in which edges are cubes (i.e., conjunctions of literals) represented using two bit-vectors. Such a class was experimentally introduced in Spot 2.10 and is currently used in some parallel emptiness check procedures [38].
Notes
- 1.
- 2.
Our previous tool paper [21] has over 250 citations according to Google scholar.
- 3.
As demonstrated by https://spot.lrde.epita.fr/tut51.html.
- 4.
Contrast on-the-fly and explicit APIs at https://spot.lrde.epita.fr/tut50.html.
- 5.
- 6.
https://spot.lrde.epita.fr/tut40.html illustrates how a game can be used to decide if a state simulates another one.
References
1800-2017 - IEEE Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language. IEEE (2018)
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)
Baarir, S., Duret-Lutz, A.: Mechanizing the minimization of deterministic generalized Büchi automata. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 266–283. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43613-4_17
Baarir, S., Duret-Lutz, A.: SAT-based minimization of deterministic \(\omega \)-automata. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 79–87. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_6
Babiak, T., et al.: The Hanoi omega-automata format. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479–486. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_31
Baier, C., Blahoudek, F., Duret-Lutz, A., Klein, J., Müller, D., Strejček, J.: Generic emptiness check for fun and profit. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 445–461. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31784-3_26
Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical Report 11/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)
Blahoudek, F., Heizmann, M., Schewe, S., Strejček, J., Tsai, M.-H.: Complementing semi-deterministic Büchi automata. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 770–787. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_49
Bloemen, V., Duret-Lutz, A., van de Pol, J.: Model checking with generalized Rabin and Fin-less automata. Int. J. Soft. Tools Technol. Transfer 21(3), 307–324 (2019). https://doi.org/10.1007/s10009-019-00508-4
Boker, U., Kupferman, O.: Co-Büching them all. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 184–198. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19805-2_13
Boker, U., Kupferman, O., Rosenberg, A.: Alternation removal in Büchi automata. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 76–87. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14162-1_7
Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 350–367. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35182-2_25
Bruyère, V., Raskin, J.-F., Tamines, C.: Pareto-rational verification (2022). https://arxiv.org/abs/2202.13485
Carton, O., Maceiras, R.: Computing the Rabin index of a parity automaton. Informatique théorique et applications 33(6), 495–505 (1999). http://www.numdam.org/item/ITA_1999__33_6_495_0/
Casares, A., Colcombet, T., Fijalkow, N.: Optimal transformations of games and automata using Muller conditions. In: ICALP 2021, vol. 198, pp. 1–14 (2021)
Casares, A., Duret-Lutz, A., Meyer, K.J., Renkin, F., Sickert, S.: Practical applications of the alternating cycle decomposition. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. LNCS, vol. 13244, pp. 99–117. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99527-0_6
Conda-Forge Community: The conda-forge project: community-based software distribution built on the conda package format and ecosystem, July 2015. https://doi.org/10.5281/zenodo.4774216
Doveri, K., Ganty, P., Mazzocchi, N.: FORQ-based language inclusion formal testing. In: Shoham, S., Vizel, Y. (eds.) CAV 2022, LNAI, vol. 13372, pp. yy–zz (2022). https://doi.org/10.1007/978-3-031-13188-2_9
Duret-Lutz, A.: Manipulating LTL formulas using spot 1.0. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 442–445. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02444-8_31
Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized Büchi automata. In: MASCOTS 2004, pp. 76–83. IEEE Computer Society Press (2004)
Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0—a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_8
Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8(3), 275–306 (1987)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_6
Giacomo, G.D., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI 2013, pp. 854–860 (2013)
Havlena, V., Lengál, O., Šmahlíková, B.: Complementing Büchi automata with Ranker. In: Shoham, S., Vizel, Y. (eds.) CAV 2022, LNAI, vol. 13372, pp. yy–zz (2022). https://doi.org/10.1007/978-3-031-13188-2_9
Jasper, M., et al.: RERS 2019: combining synthesis with real-world models. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 101–115. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_7
Klein, J., Baier, C.: On-the-fly stuttering in the construction of deterministic \(\omega \)-automata. In: Holub, J., Žd’árek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 51–61. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-76336-9_7
Kordon, F., et al.: Complete results for the 2021 edition of the model checking contest, June 2021. http://mcc.lip6.fr/2021/results.php
Křetínský, J., Esparza, J.: Deterministic automata for the (F, G)-fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7–22. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_7
Křetínský, J., Meggendorfer, T., Sickert, S.: Owl: a Library for \(\omega \)-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543–550. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_34
Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic \(\omega \) automata vis-a-vis deterministic Buchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol. 834, pp. 378–386. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58325-4_202
Křetínský, J., Meggendorfer, T., Waldmann, C., Weininger, M.: Index appearance record with preorders. Acta Informatica, 1–34 (2021). https://doi.org/10.1007/s00236-021-00412-y
Löding, C., Pirogov, A.: New optimizations and heuristics for determinization of Büchi automata. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 317–333. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31784-3_18
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC 1990, pp. 377–410. ACM (1990)
Michaud, T., Colange, M.: Reactive synthesis from LTL specification with spot. In: SYNT 2018 (2018). http://www.lrde.epita.fr/dload/papers/michaud.18.synt.pdf
Michaud, T., Duret-Lutz, A.: Practical stutter-invariance checks for \(\omega \)-regular languages. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 84–101. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23404-5_7
Miyano, S., Hayashi, T.: Alternating finite automata on \(\omega \)-words. Theoret. Comput. Sci. 32, 321–330 (1984)
Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Variations on parallel explicit model checking for generalized Büchi automata. Int. J. Softw. Tools Technol. Transfer (STTT) 19(6), 653–673 (2017)
Renkin, F., Duret-Lutz, A., Pommellet, A.: Practical “paritizing’’ of emerson-Lei automata. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 127–143. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-59152-6_7
Renkin, F., Schlehuber, P., Duret-Lutz, A., Pommellet, A.: Improvements to ltlsynt. Presented at the SYNT 2021 Workshop, Without Proceedings, July 2021. https://www.lrde.epita.fr/~adl/dl/adl/renkin.21.synt.pdf
Safra, S., Vardi, M.Y.: On \(\omega \)-automata and temporal logic. In: STOC 1989, pp. 127–137. ACM (1989)
Tauriainen, H.: A randomized testbench for algorithms translating linear temporal logic formulæ into Büchi automata. In: CS &P 1999, pp. 251–262 (1999)
Tsai, M.-H., Tsay, Y.-K., Hwang, Y.-S.: GOAL for games, omega-automata, and logics. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 883–889. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_62
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Duret-Lutz, A. et al. (2022). From Spot 2.0 to Spot 2.10: What’s New?. In: Shoham, S., Vizel, Y. (eds) Computer Aided Verification. CAV 2022. Lecture Notes in Computer Science, vol 13372. Springer, Cham. https://doi.org/10.1007/978-3-031-13188-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-031-13188-2_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-13187-5
Online ISBN: 978-3-031-13188-2
eBook Packages: Computer ScienceComputer Science (R0)