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...
| Main Author: | |
|---|---|
| Other Authors: | , , |
| Format: | conferenceObject |
| Language: | eng |
| Published: |
2020
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/10400.22/18539 |
| Country: | Portugal |
| Oai: | oai:recipp.ipp.pt:10400.22/18539 |
| Summary: | 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 modulo the theory of arrays, uninterpreted functions with equality and non-linear real-arithmetic is synthesized and may then be further investigated using appropriate SMT solvers. We show the benefits of using RMTL- ∫ with the given SMT encoding on a diversified set of examples that include in particular its application in the area of schedulability analysis. Therefore, we introduce a simple language for formalizing schedulability problems and show how to formulate timing constraints as RMTL- ∫ formulas. Our practical evaluation based on our synthesis and Z3 as back-end SMT solver also shows the feasibility of the overall approach. |
|---|