__CTAV 2.0: Model Checking Metric
Temporal Logic MTL____0,____¡Þ____ for Timed B¨¹chi
Automata __

¡¡

CATV 2.0 is a
model checker for Metric Temporal Logic MTL0,¡Þ, which is an timed extension
of propositional linear temporal logic (PLTL) . The syntax of MTL0,¡Þ is as follows:
Formula := true | Atom | ! (Formula) |
O(Formula) | (Formula /\ Formula) | (Formula U[<=c] Formula) | (Formula
U[>=c] Formula) | (Formula
U[<c] Formula) | (Formula U[>c] Formula) where Atom is an atomic
proposition, ! is the negation operator (NOT), O is
the next operator, U is the until operator, and c is a nonnegative integer. The other operators, such as
the release operator R, the eventually operator <> and the always
operator [], can be defined in the usual way. For a given timed B¨¹chi automaton M and a given MTL0,¡Þ formula ¦Õ, CATV 2.0 can
check whether M satisfies ¦Õ.
¡¡ - CTAV 2.0 (ctav_windows.rar)
for Windows Platform
References: 1.
Guangyuan Li: Checking Timed B¨¹chi
Automata Emptiness Using LU-Abstractions. Proceedings of the 7th
International Conference on Formal Modeling and Analysis of Timed Systems
(FORMATS 2009), LNCS 5813, pp. 228-242, Springer, 2009. Last modified: 2016/01/20. Contact: ligy
at ios.ac.cn |