diff --git a/doc/org/tools.org b/doc/org/tools.org index 68c33a89b..a1cfae413 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -48,6 +48,35 @@ corresponding commands are hidden. - [[file:satmin.org][SAT-based minimization of Deterministic (Generalized) Büchi automata]] +* Citing + +If you want to refer to these tools in an article, please cite one of +the following articles: + +- *Manipulating LTL formulas using Spot 1.0*, /Alexandre Duret-Lutz/. + In Proc. of ATVA'13, LNCS 8172, pp. 442--445. Hanoi, Vietnam, + Oct. 2013. ([[http://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.13.atva][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.slides.pdf][slides]]) + + This focuses on =ltlfilt=, =randltl=, and =ltlcross=. + +- *LTL translation improvements in Spot*, /Alexandre Duret-Lutz/. + In Proc. of VECoS'11. Electronic Workshops in Computing. Tunis, Tunisia, Sep. 2011. + ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.11.vecos][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.slides.pdf][slides]]) + + This describes the translation from LTL to TGBA used by =ltl2tgba= + and =ltl2tgta=. + +- *Model checking using generalized testing automata*, /Ala Eddine Ben + Salem/, /Alexandre Duret-Lutz/, and /Fabrice Kordon/. In + Transactions on Petri Nets and Other Models of Concurrency (ToPNoC + VI), 7400:94--112, 2012. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#bensalem.12.topnoc][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/bensalem.12.topnoc.pdf][pdf]]) + + This describes the generalized testing automata produced by =ltl2tgta=. + + +Check the man page for each tool for additional references about the +algorithms or data sources used. + # LocalWords: num toc helloworld SRC LTL PSL randltl ltlfilt genltl # LocalWords: scalable ltl tgba Büchi automata tgta ltlcross eval # LocalWords: setenv concat getenv setq diff --git a/src/bin/man/genltl.x b/src/bin/man/genltl.x index 41f232bbe..cd83cbdcb 100644 --- a/src/bin/man/genltl.x +++ b/src/bin/man/genltl.x @@ -3,6 +3,13 @@ genltl \- generate LTL formulas from scalable patterns [DESCRIPTION] .\" Add any additional description here [BIBLIOGRAPHY] +If you would like to give a reference to this tool in an article, +we suggest you cite the following paper: +.TP +\(bu +Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. +Proceedings of ATVA'13. LNCS 8172. +.PP Prefixes used in pattern names refer to the following papers: .TP gh diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x index 554e2e96e..986e3a63d 100644 --- a/src/bin/man/ltl2tgba.x +++ b/src/bin/man/ltl2tgba.x @@ -80,5 +80,16 @@ p[0-9]+ as double-quoted strings. 0 -1 & ! "b" ! "a" -1 +[BIBLIOGRAPHY] +If you would like to give a reference to this tool in an article, +we suggest you cite one of the following papers: +.TP +\(bu +Alexandre Duret-Lutz: LTL translation improvements in Spot. Proceedings of VECoS'11. +.TP +\(bu +Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. +Proceedings of ATVA'13. LNCS 8172. + [SEE ALSO] .BR spot-x (7) diff --git a/src/bin/man/ltl2tgta.x b/src/bin/man/ltl2tgta.x index 05ae45973..02c5fc666 100644 --- a/src/bin/man/ltl2tgta.x +++ b/src/bin/man/ltl2tgta.x @@ -2,5 +2,13 @@ ltl2tgta \- translate LTL/PSL formulas into Testing Automata [DESCRIPTION] .\" Add any additional description here +[BIBLIOGRAPHY] +If you would like to give a reference to this tool in an article, +we suggest you cite the following paper: +.TP +\(bu +Ala Eddine Ben Salem, Alexandre Duret-Lutz, and Fabrice Kordon: Model +checking using generalized testing automata. Transactions on Petri +Nets and Other Models of Concurrency (ToPNoC VI), 7400:94-112, 2012. [SEE ALSO] .BR spot-x (7) diff --git a/src/bin/man/ltlcross.x b/src/bin/man/ltlcross.x index 3359e5eaa..27dca38ad 100644 --- a/src/bin/man/ltlcross.x +++ b/src/bin/man/ltlcross.x @@ -179,20 +179,26 @@ over the \fIN\fR products performed. .BR ltl2tgba (1) [BIBLIOGRAPHY] +If you would like to give a reference to this tool in an article, +we suggest you cite the following paper: +.TP +\(bu +Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. +Proceedings of ATVA'13. LNCS 8172. +.PP ltlcross is a Spot-based reimplementation of a tool called LBTT. LBTT was developped by Heikki Tauriainen at the Helsinki University of Technology. The main motivation for the reimplementation was to support PSL, and output more statistics about the translations. The sanity checks performed on the result of each translator (by -either LBTT or ltlcross) are described in the following paper. - +either LBTT or ltlcross) are described in the following paper: .TP -th02 +\(bu H. Tauriainen and K. Heljanko: Testing LTL formula translation into Büchi automata. Int. J. on Software Tools for Technology Transfer. Volume 4, number 1, October 2002. - +.PP LBTT did not implement Test 2 described in this paper. ltlcross implements a slight variation: when an automaton produced by some translator is deterministic, its complement is built and used for diff --git a/src/bin/man/ltlfilt.x b/src/bin/man/ltlfilt.x index 440e1397c..51a5313ec 100644 --- a/src/bin/man/ltlfilt.x +++ b/src/bin/man/ltlfilt.x @@ -3,15 +3,23 @@ ltlfilt \- filter files or lists of LTL/PSL formulas [DESCRIPTION] .\" Add any additional description here [BIBLIOGRAPHY] +If you would like to give a reference to this tool in an article, +we suggest you cite the following paper: .TP -1. +\(bu +Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. +Proceedings of ATVA'13. LNCS 8172. +.PP +The following papers describes algorithms used by ltlfilt: +.TP +\(bu Kousha Etessami: A note on a question of Peled and Wilke regarding stutter-invariant LTL. Information Processing Letters 75(6): 261-263 (2000). Describes the transformation behind the \fB\-\-remove\-x\fR option. .TP -2. +\(bu Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Powerset Construction for Restricted Classes of ω-Automata. Proceedings of ATVA'07. LNCS 4762. @@ -19,7 +27,7 @@ Powerset Construction for Restricted Classes of Describes the checks implemented by the \fB\-\-safety\fR, \fB\-\-guarantee\fR, and \fB\-\-obligation\fR options. .TP -3. +\(bu Ivana Černá, Radek Pelánek: Relating Hierarchy of Temporal Properties to Model Checking. Proceedings of MFCS'03. LNCS 2747. @@ -29,7 +37,7 @@ Describes the syntactic LTL classes matched by the \fB\-\-syntactic\-persistence\fR, and \fB\-\-syntactic\-recurrence\fR options. .TP -4. +\(bu Kousha Etessami, Gerard J. Holzmann: Optimizing Büchi Automata. Proceedings of CONCUR'00. LNCS 1877. diff --git a/src/bin/man/randltl.x b/src/bin/man/randltl.x index ed4e2eaeb..f5d125720 100644 --- a/src/bin/man/randltl.x +++ b/src/bin/man/randltl.x @@ -2,6 +2,13 @@ randltl \- generate random LTL/PSL formulas [DESCRIPTION] .\" Add any additional description here +[BIBLIOGRAPHY] +If you would like to give a reference to this tool in an article, +we suggest you cite the following paper: +.TP +\(bu +Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. +Proceedings of ATVA'13. LNCS 8172. [SEE ALSO] .BR genltl (1), .BR ltlfilt (1)