Institute of Computer Science and Applied Mathematics
in the Faculty of Engineering of the Christian-Albrechts-Universität zu Kiel

Theoretical Computer Science

Dr.rer.nat. Carsten Fritz, Diplom-Informatiker

Email:

fritz@ti.informatik.uni-kiel.de

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

C. Fritz: Simulation-Based Simplification of omega-Automata. Dissertation zur Erlangung des akademischen Grades Doktor der Naturwissenschaften der Technischen Fakultät der Christian-Albrechts-Universität zu Kiel, 2005 (edited 2006).
Slides of my disputation talk (MS PowerPoint, in German, 1905 KB)

Technical reports

C. Fritz, Th. Wilke: Simulation Relations for Alternating Büchi Automata. Extended technical report. July 2002. A revised version is published in Theoretical Computer Science (see below). An older version can be found here.
C. Fritz, Concepts of Automata Construction from LTL. Technical Report.

Articles in conference proceedings (refereed)

C. Fritz, Th. Wilke: State Space Reductions for Alternating Büchi Automata: Quotienting by Simulation Equivalences (© Springer-Verlag). Paper at FSTTCS02. [bib]. (This is an extended abstract of the above report and the TCS article.)
C. Fritz, Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata (© Springer-Verlag). Paper at CIAA 2003. [bib]. This is a description of the algorithm used in LTL -> NBA (see below).
C. Fritz, Concepts of Automata Construction from LTL. Paper at LPAR 2005. [bib]. The above techrep is the long version. Please contact me if you would like to read the article version but your institution does not have a Springer-Link license.
C. Fritz, Th. Wilke: Simulation Relations for Alternating Parity Automata and Parity Games. Paper at DLT 2006. [bib]

Journal article

C. Fritz, Th. Wilke, Simulation Relations for Alternating Büchi Automata. Article in Theoretical Computer Science. [bib]. Please contact me if you would like to read the article but your institution does not have a TCS license.

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 $k \cdot 2^n$ 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 $2^{n+k}$ , 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:

What do they know about you?
Man spricht deutsh!? Lassen Sie Google diese Seite übersetzen. Auf eigenes Risiko!