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

This paper introduces a synthesis procedure for the satisfiability problem of RMTL- ∫ formulas as SAT solving modulo theories. RMTL- ∫ 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 mod...

ver descrição completa

Detalhes bibliográficos
Autor principal: Matos, Andre de (author)
Outros Autores: Leucker, Martin (author), Pereira, David (author), Pinto, Jorge Sousa (author)
Formato: conferenceObject
Idioma:eng
Publicado em: 2020
Assuntos:
Metric temporal logic
Schedulability analysis
Constraint programming
Satisfiability modulo theories
Texto completo:http://hdl.handle.net/10400.22/18539
País:Portugal
Oai:oai:recipp.ipp.pt:10400.22/18539

Texto Completo

http://hdl.handle.net/10400.22/18539

Registros relacionados