Nature language to LTL formula via a finetuned LLM

Natural language description:

Task_1.1 and Task_1.2 can be done in any order, Task_1.1 and Task_1.2 must be completed before Task_1.3, Task_1.3 must be completed before Task_1.4.


Possible output from the translator:

Finally Task_1.1 And Finally Task_1.2 And Finally (Task_1.3 And Finally Task_1.4) And (Not Task_1.3 Until Task_1.1) And (Not Task_1.3 Until Task_1.2)