CASAAL: a tool for translating Metric Temporal Logic MTL0, into timed Büchi automata and deterministic timed Büchi automata.


The syntax of  MTL0, is as follows:

  Formula := true | Atom | ! (Formula) | O(Formula) | (Formula /\ Formula) | (Formula U Formula) | (Formula U[<c] Formula) | (Formula U[<=c] Formula) | (Formula U[>c] Formula) | (Formula U[>=d]  Formula)

Where Atom is an atomic proposition, ! is the negation operator (NOT), O is the next operator, U is the until operator, c is a nonnegative integer and d is a positive integer.


The other operators, such as the release operator R, the eventually operator <> and the always operator [], can be defined in the usual way.

Examples:  true U[>=1] (!p \/ (false R[<1] q)),  (<>[>=1] a) \/ ([][<=2] b),  (a U[<2] b) U c,  [](p-> <>[<=2]q) 


Operating system: Microsoft Windows.

Usage: In the command line, run the following command.

casaal  [-under/over]  formula.txt





1.        Guangyuan Li, Peter G. Jensen, Kim G. Larsen, Axel Legay and Danny B. Poulsen: Practical Controller Synthesis for MTL{0,},  In Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software(SPIN 2017), pp102-111, 2017.

2.        Peter Bulychev, Alexandre David, Kim G. Larsen, Guangyuan Li: Efficient controller synthesis for a fragment of MTL0,∞. Acta Informatica, DOI 10.1007/s00236-013-0189-z, Springer, 2013.

3.        Peter Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Guangyuan Li, Danny B. Poulsen, Amelie Stainer: Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic. 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), LNCS 7180, pp. 168-182, 2012.