qtlsolver

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