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
References:
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.