资 源 简 介
Given a formula of the Quantitative Temporal Logic (QTL) or its subclasses, like Metric Interval Temporal Logic (MITL), the tool produces an equisatisfiable CLTL-over-clocks formula.
The obtained formula can be solved by any CLTL-over-clocks solver (e.g., ae2zot).
The tool is based on the following papers:
A Tool for Deciding the Satisfiability of Continuous-time Metric Temporal Logic http://bit.ly/16eisdU
On the Satis fiability of Metric Temporal Logics over the Reals http://bit.ly/Xsg6UZ
Deciding Continuous-time Metric Temporal Logic with Counting Modalities http://bit.ly/11sODlg
Overview
The tool translates MITL or QTL into CLTL-over-clocks, which
can be checked for satisfiability by ae2zot.
CLTL-over-clocks is an extension of LTL where formulae may contain variables behaving as clocks which can be used to measure the time elapsing between events.
The toolkit has 3 layers where CL
