man: more doc about TGBA and monitors

This was prompted by an exchange of emails with Caroline Lemieux.

* src/bin/man/ltl2tgba.x: Add notes and references.
* NEWS, THANKS: Update.

NEWS

@@ -1,5 +1,10 @@
 New in spot 1.2.4a (not yet released)
 
+  * Documentation
+
+    - The man page for ltl2tgba has some new notes and references
+      about TGBA and about monitors.
+
   * Bug fixes:
 
     - Fix simplification of bounded repetition in SERE formulas.

THANKS

@@ -2,6 +2,7 @@ We are grateful to these people for their comments, help, or
 suggestions.
 
 Akim Demaille
+Caroline Lemieux
 Christian Dax
 Ernesto Posse
 Étienne Renault

src/bin/man/ltl2tgba.x

@@ -1,5 +1,42 @@
 [NAME]
 ltl2tgba \- translate LTL/PSL formulas into Büchi automata
+[NOTE ON TGBA]
+
+TGBA stands for Transition-based Generalized Büchi Automaton.  The
+name was coined by Dimitra Giannakopoulou and Flavio Lerda in their
+FORTE'02 paper (From States to Transitions: Improving Translation of
+LTL Formulae to Büchi Automata), although similar automata have been
+used under different names long before that.
+
+As its name implies a TGBA uses a generalized Büchi acceptance
+condition, meanings that a run of the automaton is accepted iff it
+visits ininitely often multiple acceptance sets, and it also uses
+transition-based acceptance, i.e., those acceptance sets are sets of
+transitions.  TGBA are often more consise than traditional Büchi
+automata.  For instance the LTL formula \f(CWGFa & GFb\fR can be
+translated into a single-state TGBA while a traditional Büchi
+automaton would need 3 states.  Compare
+
+  % ltl2tgba 'GFa & GFb'
+
+with
+
+  % ltl2tgba --ba 'GFa & GFb'
+
+In the dot output produced by the above commands, the membership of
+the transitions to the various acceptance sets is denoted using names
+in braces.  The actuall names do not really matter as they may be
+produced by the translation algorithm or altered by any latter
+postprocessing.
+
+When the \fB\--ba\fR option is used to request a Büchi automaton, Spot
+builds a TGBA with a single acceptance set, and in which for any state
+either all outgoing transitions are accepting (this is equivalent to
+the state being accepting) or none of them are.  Double circles are
+used to highlight accepting states in the output, but the braces
+denoting the accepting transitions are still shown because the
+underling structure really is a TGBA.
+
 [NOTE ON LBTT'S FORMAT]
 The format, described at
 http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html,
@@ -10,7 +47,7 @@ internally, it will normally use the transition-based flavor of that
 format, indicated with a 't' flag after the number of acceptance sets.
 For instance:
 
-  % bin/ltl2tgba --lbtt 'GFp0 & GFp1 & FGp2'
+  % ltl2tgba --lbtt 'GFp0 & GFp1 & FGp2'
   2 2t                   // 2 states, 2 transition-based acceptance sets
   0 1                    // state 0: initial
   0 -1 t                 //   trans. to state 0, no acc., label: true
@@ -80,6 +117,38 @@ p[0-9]+ as double-quoted strings.
   0 -1 & ! "b" ! "a"
   -1
 
+[NOTE ON GENERATING MONITORS]
+
+The monitors generated with option \fB\-M\fR are finite state automata
+used to reject finite words that cannot be extended to infinite words
+compatible with the supplied formula.  The idea is that the monitor
+should progress alongside the system, and can only make decisions
+based on the finite prefix read so far.
+
+Monitors can be seen as Büchi automata in which all recognized runs are
+accepting.  As such, the only infinite words they can reject are those
+are not recognized, i.e., infinite words that start with a bad prefix.
+
+Because of this limited expressiveness, a monitor for some given LTL
+or PSL formula may accept a larger language than the one specified by
+the formula.  For instance a monitor for the LTL formula \f(CWa U b\fR
+will reject (for instance) any word starting with \f(CW!a&!b\fR as
+there is no way such a word can validate the formula, but it will not
+reject a finite prefix repeating only \f(CWa&!b\fR as such a prefix
+could be extented in a way that is comptible with \f(CWa U b\fR.
+
+For more information about monitors, we refer the readers to the
+following two papers (the first paper describes the construction of
+the second paper in a more concise way):
+.TP
+\(bu
+Deian Tabakov and Moshe Y. Vardi: Optimized Temporal Monitors for SystemC.
+Proceedings of RV'10.  LNCS 6418.
+.TP
+\(bu
+Marcelo d’Amorim and Grigoire Roşu: Efficient monitoring of
+ω-languages.  Proceedings of CAV'05.  LNCS 3576.
+
 [BIBLIOGRAPHY]
 If you would like to give a reference to this tool in an article,
 we suggest you cite one of the following papers: