Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages


home | help
LTL2TGBA(1)			 User Commands			   LTL2TGBA(1)

       ltl2tgba	- translate LTL/PSL formulas into BA1/4chi automata

       ltl2tgba	[OPTION...] [FORMULA...]

       Translate  linear-time  formulas	(LTL/PSL) into various types of	autom-

       By default it will apply	all  available	optimizations  to  output  the
       smallest	 Transition-based Generalized BA1/4chi Automata, output	in the
       HOA format.  If multiple	formulas are supplied, several	automata  will
       be output.

   Input options:
       -f, --formula=STRING
	      process the formula STRING

       -F, --file=FILENAME[/COL]
	      process each line	of FILENAME as a formula; if COL is a positive
	      integer, assume a	CSV file and read column COL; use  a  negative
	      COL to drop the first line of the	CSV file

	      read all formulas	using LBT's prefix syntax

	      parenthesized  blocks  that  cannot be parsed as subformulas are
	      considered as atomic properties

	      negate each formula

   Output automaton type:
       -B, --ba
	      BA1/4chi Automaton (implies -S)

       --cobuchi, --coBuchi
	      automaton	with co-BA1/4chi acceptance (will recognize a superset
	      of the input language if not co-BA1/4chi realizable)

       -C, --complete
	      output a complete	automaton

       -G, --generic
	      any acceptance condition is allowed

       -M, --monitor
	      Monitor (accepts all finite prefixes of the given	property)

       -p, --colored-parity[=any|min|max|odd|even|min odd|min even|max odd|max

       even]  colored automaton	with parity acceptance

       -P, --parity[=any|min|max|odd|even|min odd|min even|max odd|max even]
	      automaton	with parity acceptance

       -S, --state-based-acceptance, --sbacc
	      define the acceptance using states

       --tgba Transition-based Generalized BA1/4chi Automaton (default)

       -U, --unambiguous
	      output unambiguous automata

   Output format:
       -8, --utf8
	      enable  UTF-8  characters	 in  output  (ignored  with  --lbtt or

	      test for the additional property PROP and	output the  result  in
	      the  HOA	format (implies	-H).  PROP may be some prefix of 'all'
	      (default), 'unambiguous',	 'stutter-invariant',  'stutter-sensi-
	      tive-example', 'semi-determinism', or 'strength'.

       -d,  --dot[=1|a|A|b|B|c|C(COLOR)|e|E|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|
	      GraphViz's format.  Add letters for (1) force  numbered  states,
	      (a)  show	 acceptance  condition	(default), (A) hide acceptance
	      condition, (b) acceptance	sets as	bullets,  (B)  bullets	except
	      for BA1/4chi/co-BA1/4chi automata, (c) force circular nodes, (C)
	      color nodes with COLOR, (d) show origins when known,  (e)	 force
	      elliptic nodes, (E) force	rEctangular nodes, (f(FONT)) use FONT,
	      (g) hide edge labels, (h)	horizontal layout, (k) use  state  la-
	      bels  when  possible,  (K)  use transition labels	(default), (n)
	      show name, (N) hide name,	(o) ordered transitions,  (r)  rainbow
	      colors  for  acceptance  sets,  (R)  color  acceptance  sets  by
	      Inf/Fin, (s) with	SCCs, (t) force	 transition-based  acceptance,
	      (u)  hide	 true states, (v) vertical layout, (y) split universal
	      edges by color, (+INT) add INT to	all set	numbers,  (<INT)  dis-
	      play at most INT states, (#) show	internal edge numbers

       -H, --hoaf[=1.1|i|k|l|m|s|t|v]
	      Output  the  automaton  in HOA format (default).	Add letters to
	      select (1.1) version 1.1 of the format, (i) use implicit	labels
	      for  complete deterministic automata, (s)	prefer state-based ac-
	      ceptance when possible [default],	(t) force transition-based ac-
	      ceptance,	(m) mix	state and transition-based acceptance, (k) use
	      state labels when	possible, (l) single-line output, (v)  verbose

	      LBTT's  format (add =t to	force transition-based acceptance even
	      on BA1/4chi automata)

	      set the name of the output automaton

       -o, --output=FORMAT
	      send output to a file named FORMAT instead of  standard  output.
	      The  first  automaton  sent to a file truncates it unless	FORMAT
	      starts with '>>'.

       -q, --quiet
	      suppress all normal output

       -s, --spin[=6|c]
	      Spin neverclaim (implies	--ba).	 Add  letters  to  select  (6)
	      Spin's 6.2.4 style, (c) comments on states

       --stats=FORMAT, --format=FORMAT
	      output statistics	about the automaton

   Any FORMAT string may use the following interpreted sequences:
       %<     the  part	of the line before the formula if it comes from	a col-
	      umn extracted from a CSV file

       %>     the part of the line after the formula if	it comes from a	column
	      extracted	from a CSV file

       %%     a	single %

       %a     number of	acceptance sets

       %c, %[LETTERS]c
	      number  of SCCs; you may filter the SCCs to count	using the fol-
	      lowing LETTERS, possibly concatenated: (a)  accepting,  (r)  re-
	      jecting, (c) complete, (v) trivial, (t) terminal,	(w) weak, (iw)
	      inherently weak. Use uppercase letters to	negate them.

       %d     1	if the output is deterministic,	0 otherwise

       %e     number of	reachable edges

       %f     the formula, in Spot's syntax

       %F     name of the input	file

       %g, %[LETTERS]g
	      acceptance condition (in HOA syntax); add	brackets to  print  an
	      acceptance  name instead and LETTERS to tweak the	format:	(0) no
	      parameters, (a) accentuated, (b) abbreviated, (d)	style used  in
	      dot   output,   (g)  no  generalized  parameter,	(l)  recognize
	      Street-like and Rabin-like, (m) no main parameter, (p) no	parity
	      parameter, (o) name unknown acceptance as	'other', (s) shorthand
	      for 'lo0'.

       %h     the automaton in HOA format on a single  line  (use  %[opt]h  to
	      specify additional options as in --hoa=opt)

       %L     location in the input file

       %m     name of the automaton

       %n     number of	nondeterministic states	in output

       %p     1	if the output is complete, 0 otherwise

       %r     wall-clock time elapsed in seconds (excluding parsing)

       %R, %[LETTERS]R
	      CPU  time	 (excluding  parsing),	in seconds; Add	LETTERS	to re-
	      strict to(u) user	time, (s) system time, (p) parent process,  or
	      (c) children processes.

       %s     number of	reachable states

       %t     number of	reachable transitions

       %u, %[e]u
	      number of	states (or [e]dges) with universal branching

       %u, %[LETTER]u
	      1	 if the	automaton contains some	universal branching (or	a num-
	      ber of [s]tates or [e]dges with universal	branching)

       %w     one word accepted	by the output automaton

       %x, %[LETTERS]x
	      number of	atomic propositions declared in	 the  automaton;   add
	      LETTERS to list atomic propositions with (n) no quoting, (s) oc-
	      casional double-quotes with C-style  escape,  (d)	 double-quotes
	      with  C-style  escape,  (c) double-quotes	with CSV-style escape,
	      (p) between parentheses, any  extra  non-alphanumeric  character
	      will be used to separate propositions

   Simplification goal:
       -a, --any
	      no preference, do	not bother making it small or deterministic

       -D, --deterministic
	      prefer deterministic automata (combine with --generic to be sure
	      to obtain	a deterministic	automaton)

	      prefer small automata (default)

   Simplification level:
       --high all available optimizations (slow, default)

       --low  minimal optimizations (fast)

	      moderate optimizations

   Miscellaneous options:
       -x, --extra-options=OPTS
	      fine-tuning options (see spot-x (7))

       --help print this help

	      print program version

       Mandatory or optional arguments to long options are also	 mandatory  or
       optional	for any	corresponding short options.

       TGBA  stands  for Transition-based Generalized BA1/4chi 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 BA1/4chi	Automata), although similar automata have been
       used under different names long before that.

       As  its name implies a TGBA uses	a generalized BA1/4chi acceptance con-
       dition, 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 BA1/4chi	automata.  For
       instance	the LTL	formula	GFa & GFb can be  translated  into  a  single-
       state  TGBA while a traditional BA1/4chi	automaton would	need 3 states.

	   % ltl2tgba 'GFa & GFb'


	   % 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  --ba	option	is  used to request a BA1/4chi 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	denot-
       ing the accepting transitions are still	shown  because	the  underling
       structure really	is a TGBA.

       LBTT's format <
       automata.html> has support for both transition-based  and  state	 based
       generalized acceptance.

       Because Spot uses transition-based generalized BA1/4chi automata	inter-
       nally, it will normally use the transition-based	flavor of that format,
       indicated with a	't' flag after the number of acceptance	sets.  For in-

	   % 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
	   1 -1	| & p0 p2 & p1 p2 //   trans. to state 1, no acc., label: (p0&p2)|(p1&p2)
	   -1			  // end of state 0
	   1 0			  // state 1: not initial
	   1 0 1 -1 & &	p0 p1 p2  //   trans. to state 1, acc. 0 and 1,	label: p0&p1&p2
	   1 0 -1 & & p1 p2 ! p0  //   trans. to state 1, acc. 0, label: !p0&p1&p2
	   1 1 -1 & & p0 p2 ! p1  //   trans. to state 1, acc. 1, label: p0&!p1&p2
	   1 -1	& & p2 ! p0 ! p1  //   trans. to state 1, no acc., label: !p0&!p1&p2
	   -1			  // end if state 1

       Here, the two acceptance	sets are represented by	the numbers 0  and  1,
       and  they each contain two transitions (the first transition of state 1
       belongs to both sets).

       When both --ba and --lbtt options are used, the state-based  flavor  of
       the  format is used instead.  Note that the LBTT	format supports	gener-
       alized acceptance conditions on states, but Spot	only use  this	format
       for  BA1/4chi  automata,	where there is always only one acceptance set.
       Unlike in the LBTT documentation, we do not use the optional  's'  flag
       to  indicate  the  state-based  acceptance, this	way our	output is also
       compatible	     with	     that	     of		   LBT

	   % ltl2tgba --ba --lbtt FGp0
	   2 1		       // 2 states, 1 (state-based) accepance set
	   0 1 -1	       // state	0: initial, non-accepting
	   0 t		       //   trans. to state 0, label: true
	   1 p0		       //   trans. to state 1, label: p0
	   -1		       // end of state 0
	   1 0 0 -1	       // state	1: not initial,	in acceptance set 0
	   1 p0		       //   trans. to state 0, label: p0
	   -1		       // end if state 1

       You can force ltl2tgba to use the transition-based flavor of the	format
       even for	BA1/4chi automaton using --lbtt=t.

	   % ltl2tgba --ba --lbtt=t FGp0
	   2 1t		       // 2 states, 1 transition-based accepance set.
	   0 1		       // state	0: initial
	   0 -1	t	       //   trans. to state 0, no acc.,	label: true
	   1 -1	p0	       //   trans. to state 1, no acc.,	label: p0
	   -1		       // end of state 0
	   1 0		       // state	1: not initial
	   1 0 -1 p0	       //   trans. to state 1, acc. 0, label: p0
	   -1		       // end if state 1

       When representing a BA1/4chi automaton  using  transition-based	accep-
       tance, all transitions leaving accepting	states are put into the	accep-
       tance set.

       A final note concerns the name of the atomic propositions.  The	origi-
       nal  LBTT  and  LBT  formats  require these atomic propositions to have
       names such as 'p0', 'p32', ...  We extend the format to	accept	atomic
       proposition with	arbitrary names	that do	not conflict with LBT's	opera-
       tors (e.g. 'i' is the symbol of the implication operator	so it may  not
       be  used	 as an atomic proposition), or as double-quoted	strings.  Spot
       will always output atomic-proposition that do not match p[0-9]+ as dou-
       ble-quoted strings.

	   % ltl2tgba --lbtt 'GFa & GFb'
	   1 2t
	   0 1
	   0 0 1 -1 & "a" "b"
	   0 0 -1 & "b"	! "a"
	   0 1 -1 & "a"	! "b"
	   0 -1	& ! "b"	! "a"

       The monitors generated with option -M are finite	state automata used to
       reject finite words that	cannot be extended to infinite words  compati-
       ble  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	BA1/4chi 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

       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 a U	b will	reject
       (for  instance)	any word starting with !a&!b as	there is no way	such a
       word can	validate the formula, but it will not reject a	finite	prefix
       repeating only a&!b as such a prefix could be extented in a way that is
       comptible with a	U b.

       For more	information about monitors, we refer the readers to  the  fol-
       lowing  two  papers  (the first paper describes the construction	of the
       second paper in a more concise way):

       o      Deian Tabakov and	Moshe Y. Vardi:	 Optimized  Temporal  Monitors
	      for SystemC.  Proceedings	of RV'10.  LNCS	6418.

       o      Marcelo  d'Amorim	 and  Grigoire	RoAu:  Efficient monitoring of
	      I-languages.  Proceedings	of CAV'05.  LNCS 3576.

       If you would like to give a reference to	this tool in  an  article,  we
       suggest you cite	one of the following papers:

       o      Alexandre	 Duret-Lutz: LTL translation improvements in Spot 1.0.
	      Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March

       o      Alexandre	 Duret-Lutz: Manipulating LTL formulas using Spot 1.0.
	      Proceedings of ATVA'13.  LNCS 8172.

       o      TomA!A!  Babiak,	Thomas	Badie,	Alexandre  Duret-Lutz,	MojmAr
	      KAetAnskA1/2,  and  Jan StrejAek:	Compositional approach to sus-
	      pension and other	improvements to	LTL translation.   Proceedings
	      of SPIN'13.  LNCS	7976.

       o      Souheib  Baarir  and Alexandre Duret-Lutz: Mechanizing the mini-
	      mization of deterministic	generalized BA1/4chi  automata.	  Pro-
	      ceedings of FORTE'14.  LNCS 8461.

       Report bugs to <>.

       Copyright  (C)  2020   Laboratoire  de Recherche	et DA(C)veloppement de
       l'Epita.	   License   GPLv3+:   GNU   GPL   version    3	   or	 later
       This  is	 free  software:  you  are free	to change and redistribute it.
       There is	NO WARRANTY, to	the extent permitted by	law.


ltl2tgba (spot)	2.9.5		 November 2020			   LTL2TGBA(1)


Want to link to this manual page? Use this URL:

home | help