THE PROJECT HAS BEEN MOVED TO GITHUB, FOLLOW https://github.com/xblahoud/ltl3dra

LTL3DRA is a translator of a fragment of LTL formulae to deterministic Rabin automata. It is based on the popular tool named LTL3BA written by Tomas Babiak (available at https://sourceforge.net/projects/ltl3ba/).

The translation used in LTL3DRA is described in
T. Babiak, F. Blahoudek, M. Křetínský, and J. Strejček: Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment (2013)
In 11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013)

In order to compile LTL3DRA, the BuDDy library (http://sourceforge.net/projects/buddy/) is needed. Tested with buddy 2.4.

The benchmark used in "Comparison of LTL to Deterministic Rabin Automata Translators" paper published on LPAR19 can be found in Files/LPAR19-benchmarks (https://sourceforge.net/projects/ltl3dra/files/LPAR19-benchmarks/).

Project Activity

See All Activity >

License

GNU General Public License version 2.0 (GPLv2)

Follow LTL3DRA

LTL3DRA Web Site

Other Useful Business Software
Build Agents and Models on One Platform Icon
Build Agents and Models on One Platform

Everything you need to build production-ready agents and models. Access 200+ Google and third-party AI models and tools.

Gemini Enterprise Agent Platform is Google Cloud's comprehensive platform for developers to build, scale, govern, and optimize agents and models. Choose from Google's most advanced models and third-party models like Anthropic's Claude Model Family.
Start Free
Rate This Project
Login To Rate This Project

User Reviews

Be the first to post a review of LTL3DRA!

Additional Project Details

Registered

2013-08-04