Dr.rer.nat. Carsten Fritz,
Diplom-Informatiker
PGP Public Key Version: GnuPG v1.0.4 (GNU/Linux)
PGP Public Key Version: 2.6.3ia
If possible, please do not use the old PGP 2.6.3ia public key any longer.
Bis Februar 2006 war ich wissenschaftlicher Mitarbeiter und Doktorand am
Lehrstuhl für Theoretische
Informatik.
My work at the Christian-Albrechts-University ended in February 2006. You can
still contact me via the above e-mail address, though.
Project Automatenminimierung (Automata
Minimization):
Ph.D. Thesis / Dissertation
Technical reports
Articles in conference proceedings (refereed)
Journal article
Implementation
-
LTL -> NBA:
A prototypical implementation of an algorithm that translates LTL formulae
to equivalent nondet. Büchi automata. Simulation relations for
intermediate alternating BA are computed and used to minimize the result.
You can access LTL -> NBA via CGI. This link is to
an improved version where the upper bound for the number of states is
roughly
where
is the length of the formula and
is
the number of U- and F-subformulas. The old LTL -> NBA via CGI yields an
upper bound of about
, but the resulting automata are sometimes
smaller, nevertheless.
You can also download LTL -> NBA's
source code. Please note the enclosed license file.
Other LTL-to-NBA implementations can be found
here
(by Denis Oddoux) and
here (by
Kousha Etessami).
-
Testing protocols: I have run a number of tests to
compare my above implementation to
TMP and
LTL2BA.
I have used the tool lbtt
of Heikki Tauriainen. You can
download the protocols: LTLtest1.txt.gz,
LTLtest2.txt.gz,
LTLtest3.txt.gz,
LTLtest4.txt.gz,
LTLtest4TMPonly.txt.gz.
For your own experiments and for comparison, you can grep the formulas from
the protocols or use the formula list Test/l1000-15-3-05.ltl shipped with
Wring-1.1.0. A test
run of LTL -> NBA on l1000-15-3-05.ltl:
l1000-15-3-05.ltl.out.txt.gz
Other publications: