bib: more references

* doc/spot.bib (blahoudek.16.atva, degiacomo.13.ijcai): New entries.
* spot/tl/ltlf.hh, spot/twaalgos/complement.hh: Use them.

doc/spot.bib

@@ -82,6 +82,20 @@
   doi		= {10.1007/978-3-642-36742-7_3}
 }
 
+@InProceedings{	  blahoudek.16.atva,
+  author	= {Franti{\v{s}}ek Blahoudek and Matthias Heizmann and Sven
+		  Schewe and Jan Strej{\v{c}}ek and Ming-Hsien Tsai},
+  editor	= {Marsha Chechik and Jean-Fran{\c{c}}ois Raskin},
+  title		= {Complementing Semi-deterministic {B\"u}chi Automata},
+  booktitle	= {Proceedings of the 22th International Conférence on Tools
+		  and Algorithms for the Construction and Analysis of
+		  Systems},
+  year		= 2016,
+  publisher	= {Springer},
+  pages		= {770--787},
+  doi		= {10.1007/978-3-662-49674-9_49}
+}
+
 @InProceedings{	  bloemen.16.hvc,
   title		= {Multi-core SCC-Based LTL Model Checking},
   author	= {Vincent Bloemen and {van de Pol}, {Jan Cornelis}},
@@ -283,6 +297,18 @@
   doi		= {10.1007/978-3-642-04761-9_19}
 }
 
+@InProceedings{	  degiacomo.13.ijcai,
+  author	= {Giuseppe De Giacomo and Moshe Y. Vardi},
+  title		= {Linear Temporal Logic and Linear Dynamic Logic on Finite
+		  Traces},
+  booktitle	= {Proceedings of the 23rd International Joint Conference on
+		  Artificial Intelligence (IJCAI'13)},
+  year		= 2013,
+  editor	= {Francesca Rossi},
+  pages		= {854--860},
+  month		= aug
+}
+
 @InProceedings{	  duret.11.vecos,
   author	= {Alexandre Duret-Lutz},
   title		= {{LTL} Translation Improvements in {Spot}},
@@ -795,6 +821,22 @@
   doi		= {10.1007/978-3-642-36742-7_42}
 }
 
+@InProceedings{	  renkin.20.atva,
+  author	= {Florian Renkin and Alexandre Duret-Lutz and Adrien
+		  Pommellet},
+  title		= {Practical ``Paritizing'' of {E}merson-{L}ei Automata},
+  booktitle	= {Proceedings of the 18th International Symposium on
+		  Automated Technology for Verification and Analysis
+		  (ATVA'20)},
+  year		= {2020},
+  volume	= {12302},
+  series	= {Lecture Notes in Computer Science},
+  pages		= {127--143},
+  month		= oct,
+  publisher	= {Springer},
+  doi		= {10.1007/978-3-030-59152-6_7}
+}
+
 @InProceedings{	  rozier.07.spin,
   author	= {Kristin Y. Rozier and Moshe Y. Vardi},
   title		= {LTL Satisfiability Checking},

spot/tl/ltlf.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2016 Laboratoire de Recherche et Développement de
+// Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement
-// l'Epita (LRDE).
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -27,7 +27,7 @@ namespace spot
   /// \brief Convert an LTLf into an LTL formula.
   ///
   /// This is based on De Giacomo & Vardi (IJCAI'13) reduction from
-  /// LTLf (finite-LTL) to LTL.
+  /// LTLf (finite-LTL) to LTL. \cite degiacomo.13.ijcai
   ///
   /// In this reduction, finite words are extended into infinite words
   /// in which a new atomic proposition <code>alive</code> marks the

spot/twaalgos/complement.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2015, 2017, 2019 Laboratoire de Recherche et
+// Copyright (C) 2013-2015, 2017, 2019, 2022 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -49,8 +49,8 @@ namespace spot
   ///
   /// The automaton \a aut should be semideterministic.
   ///
-  /// Uses the NCSB algorithm described by F. Blahoudek, M. Heizmann,
+  /// Uses the NCSB algorithm described by F. Blahoudek, et al.
-  /// S. Schewe, J. Strejček, and MH. Tsai (TACAS'16).
+  /// \cite blahoudek.16.atva
   SPOT_API twa_graph_ptr
   complement_semidet(const const_twa_graph_ptr& aut, bool show_names = false);