From e5124faa13e1856e58bc9038515896d9f8f51b0b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 19 Aug 2014 14:52:51 +0200 Subject: [PATCH] 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 | 5 +++ THANKS | 1 + src/bin/man/ltl2tgba.x | 71 +++++++++++++++++++++++++++++++++++++++++- 3 files changed, 76 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 289c3ef2f..f8378d199 100644 --- a/NEWS +++ b/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. diff --git a/THANKS b/THANKS index 66d9e0a81..89d52b874 100644 --- a/THANKS +++ b/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 diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x index 3df465814..a26430c7d 100644 --- a/src/bin/man/ltl2tgba.x +++ b/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: