TGBA stands for for Transition-based Generalized Büchi Automaton.

It's an OmegaAutomaton where Büchi acceptance conditions are defined in terms of transitions instead of states. Also it uses generalized acceptance conditions, meaning there are several sets of transitions. A path in the automaton is accepted if it passes infinitely often by one transition of each acceptance set.

The acronym TGBA was coined by Dimitra Giannakopoulou and Flavio Lerda [#giannakopoulou.02.forte]. However TGBAs were used before that by Jean-Michel Couvreur [].

Serge Haddad and François Vernadat [#haddad.03.vps] complement each set of the acceptance condition to define promise automata. (The use of promises to translate LTL formulae was illustrated by Alexandre Duret-Lutz and Denis Poitrenaud [#duret.04.mascots].) Max Michel also described a comparable structure earlier [#michel.84.stacs].

Alexandre Duret-Lutz and Denis Poitrenaud. Spot: an extensible model checking library using transition-based generalized Büchi automata. In Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pages 76-83, Volendam, The Netherlands, October 2004. IEEE Computer Society Press.
[ .pdf ]

Jean-Michel Couvreur. On-the-fly verification of temporal logic. In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM'99), volume 1708 of Lecture Notes in Computer Science, pages 253-271, Toulouse, France, September 1999. ©Springer-Verlag.
[ .pdf ]

Dimitra Giannakopoulou and Flavio Lerda. From states to transitions: Improving translation of LTL formulae to Büchi automata. In D.A. Peled and M.Y. Vardi, editors, Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of Lecture Notes in Computer Science, pages 308-326, Houston, Texas, November 2002. ©Springer-Verlag.
[ .pdf ]

Serge Haddad and François Vernadat. Vérification de propriétés spécifiques. In Michel Diaz, editor, Vérification et mise en oeuvre des réseaux de Petri, Traité IC2, série Informatique et systèmes d'information, chapter 1. Hermes Science, January 2003.

Max Michel. Algèbre de machines et logique temporelle. In Max Fontet and Kurt Mehlhorn, editors, Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS'84), volume 166 of Lecture Notes in Computer Science, pages 287-298, Paris, April 1984. ©Springer-Verlag.

TGBA (last edited 2005-02-02 19:09:37 by AlexandreDuretLutz)

All text is available under the terms of the GNU Free Documentation License, see SpotWikiLicense for details.