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...

ver descrição completa

Detalhes bibliográficos
Autor principal: Pedro, André de Matos (author)
Outros Autores: Leucker, Martin (author), Pereira, David (author), Pinto, Jorge Sousa (author)
Formato: conferencePaper
Idioma:eng
Publicado em: 2020
Assuntos:
Texto completo:http://hdl.handle.net/1822/68771
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/68771