diff --git a/doc/spot.bib b/doc/spot.bib index 5405a2322..9f18ad2a9 100644 --- a/doc/spot.bib +++ b/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}}, @@ -804,6 +830,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}, diff --git a/spot/tl/ltlf.hh b/spot/tl/ltlf.hh index 4235590c6..1042e2f65 100644 --- a/spot/tl/ltlf.hh +++ b/spot/tl/ltlf.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement +// 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 alive marks the diff --git a/spot/twaalgos/complement.hh b/spot/twaalgos/complement.hh index 330bff664..902f11363 100644 --- a/spot/twaalgos/complement.hh +++ b/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, - /// S. Schewe, J. Strejček, and MH. Tsai (TACAS'16). + /// Uses the NCSB algorithm described by F. Blahoudek, et al. + /// \cite blahoudek.16.atva SPOT_API twa_graph_ptr complement_semidet(const const_twa_graph_ptr& aut, bool show_names = false);