doc: add suggestions for bibliographic references
* doc/org/tools.org, src/bin/man/genltl.x, src/bin/man/ltl2tgba.x, src/bin/man/ltl2tgta.x, src/bin/man/ltlcross.x, src/bin/man/ltlfilt.x, src/bin/man/randltl.x: Add bibliographic references, mostly to the ATVA'13 paper.
This commit is contained in:
Alexandre Duret-Lutz
parent
f65c621a55
commit
3e3d320de5
7 changed files with 84 additions and 8 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue