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
Custom VMs From 1 to 96 vCPUs With 99.95% Uptime Icon
Custom VMs From 1 to 96 vCPUs With 99.95% Uptime

General-purpose, compute-optimized, or GPU/TPU-accelerated. Built to your exact specs.

Live migration and automatic failover keep workloads online through maintenance. One free e2-micro VM every month.
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