LTLNFBA is a tool that translate an LTL formula to Buchi automata. The tools is developed based onLTL2BAwith the tranlating algorihtm changed and new rules for improving the translation.

Download and Installation

Source code of the newest version of LTLNFBA can be downloaded here (ltlnfba(v1).tar.gzNOTE: the suffix to be changed to .tar.gz). To compile the source code, linux + gcc are required.

Introduction

Spin syntax as well as commands used inLTL2BAare all kept in LTLNFBA. So a user who can use LTL2BA can also use LTLNFBA.

Hereyou can find all the formulas involved in the experiment of LTNNFBA.