CTAV 3.0: Model Checking Metric Temporal Logic MTL0,∞ for Timed Büchi Automata
|
CATV 3.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 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. For a given timed Büchi automaton M and a given MTL0,∞ formula φ, CATV 3.0 can
check whether M satisfies φ. Download 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. 2.
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. Last modified: 2019/01/20. Contact: ligy
at ios.ac.cn |