tgba_determinize: improve citations in doc

* doc/spot.bib (klein.07.ciaa, redziejowski.12.fi): Add two entries.
* spot/twaalgos/determinize.hh: Use them.
This commit is contained in:
Alexandre Duret-Lutz 2020-02-16 08:20:21 +01:00
parent 80b04e10b5
commit de5704049d
2 changed files with 37 additions and 10 deletions

View file

@ -1,3 +1,4 @@
@InProceedings{ babiak.12.tacas, @InProceedings{ babiak.12.tacas,
author = {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r author = {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r
K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k
@ -384,6 +385,21 @@
doi = {10.4204/EPTCS.229.10} doi = {10.4204/EPTCS.229.10}
} }
@InCollection{ klein.07.ciaa,
year = {2007},
booktitle = {Proceedings of the 12th International Conference on the
Implementation and Application of Automata (CIAA'07)},
volume = {4783},
series = {Lecture Notes in Computer Science},
editor = {Jan Holub and Jan Žďárek},
doi = {10.1007/978-3-540-76336-9_7},
title = {On-the-Fly Stuttering in the Construction of Deterministic
$\omega$-Automata},
publisher = {Springer},
author = {Joachim Klein and Christel Baier},
pages = {51--61}
}
@InProceedings{ kretisnky.12.cav, @InProceedings{ kretisnky.12.cav,
author = {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza}, author = {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza},
title = {Deterministic Automata for the {(F,G)}-Fragment of {LTL}}, title = {Deterministic Automata for the {(F,G)}-Fragment of {LTL}},
@ -585,6 +601,17 @@
url = {http://www.eda.org/vfv/} url = {http://www.eda.org/vfv/}
} }
@Article{ redziejowski.12.fi,
author = {Roman Redziejowski},
title = {An improved construction of deterministic omega-automaton
using derivatives},
journal = {Fundamenta Informaticae},
year = {2012},
volume = {119},
number = {3-4},
pages = {393--496}
}
@InProceedings{ renault.13.tacas, @InProceedings{ renault.13.tacas,
author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
Kordon and Denis Poitrenaud}, Kordon and Denis Poitrenaud},

View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2019 Laboratoire de Recherche et // Copyright (C) 2015-2016, 2019-2020 Laboratoire de Recherche et
// Développement de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -34,20 +34,20 @@ namespace spot
/// The output will be a deterministic automaton using parity acceptance. /// The output will be a deterministic automaton using parity acceptance.
/// ///
/// This procedure is based on an algorithm by Roman Redziejowski /// This procedure is based on an algorithm by Roman Redziejowski
/// (Fundamenta Informaticae 119, 3-4 (2012)). Redziejowski's /// \cite redziejowski.12.fi . Redziejowski's algorithm is similar
/// algorithm is similar to Piterman's improvement of Safra's /// to Piterman's improvement of Safra's algorithm, except it is
/// algorithm, except it is presented on transition-based acceptance /// presented on transition-based acceptance and use simpler
/// and use simpler notations. We implement three additional /// notations. We implement three additional optimizations (they
/// optimizations (they can be individually disabled) based on /// can be individually disabled) based on
/// ///
/// - knowledge about SCCs of the input automaton /// - knowledge about SCCs of the input automaton
/// - knowledge about simulation relations in the input automaton /// - knowledge about simulation relations in the input automaton
/// - knowledge about stutter-invariance of the input automaton /// - knowledge about stutter-invariance of the input automaton
/// ///
/// The last optimization is an idea described by Joachim Klein & /// The last optimization is an idea implemented in
/// Christel Baier (CIAA'07) and implemented in ltl2dstar. In fact, /// [`ltl2dstar`](https://www.ltl2dstar.fr) \cite klein.07.ciaa . In
/// ltl2dstar even has a finer version (letter-based stuttering) /// fact, `ltl2dstar` even has a finer version (letter-based
/// that is not implemented here. /// stuttering) that is not implemented here.
/// ///
/// \param aut the automaton to determinize /// \param aut the automaton to determinize
/// ///