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

Full description

Bibliographic Details
Main Author: Matos, Andre de (author)
Other Authors: Leucker, Martin (author), Pereira, David (author), Pinto, Jorge Sousa (author)
Format: conferenceObject
Language:eng
Published: 2020
Subjects:
Metric temporal logic
Schedulability analysis
Constraint programming
Satisfiability modulo theories
Online Access:http://hdl.handle.net/10400.22/18539
Country:Portugal
Oai:oai:recipp.ipp.pt:10400.22/18539

Internet

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

Similar Items