Real-time MTL with durations as SMT with applications to schedulability analysis

This paper introduces a synthesis procedure for the satisfiability problem of RMTL-D formulas as SAT solving modulo theories. RMTL-D is a real-time version of metric temporal logic (MTL) extended by a duration quantifier allowing to measure time durations. For any given formula, a SAT instance modul...

Full description

Bibliographic Details
Main Author: Pedro, André de Matos (author)
Other Authors: Leucker, Martin (author), Pereira, David (author), Pinto, Jorge Sousa (author)
Format: conferencePaper
Language:eng
Published: 2020
Subjects:
Online Access:http://hdl.handle.net/1822/68771
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/68771