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

André de Matos Pedro; Martin Leucker; David Pereira; Jorge Sousa Pinto

doi:10.1109/TASE49443.2020.00016

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

André de Matos Pedro, Martin Leucker, David Pereira^*, Jorge Sousa Pinto

^*Corresponding author for this work

Institute of Software Engineering and Programming Languages

Abstract

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.

Original language	English
Title of host publication	TASE
Number of pages	8
Publication date	2020
Pages	49-56
DOIs	https://doi.org/10.1109/TASE49443.2020.00016
Publication status	Published - 2020

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 9 Industry, Innovation, and Infrastructure

Research Areas and Centers

Centers: Center for Artificial Intelligence Luebeck (ZKIL)

Access to Document

10.1109/TASE49443.2020.00016

Cite this

@inproceedings{aaf6b7fa5bd44ad682e57f8ad3150183,

title = "Real-time MTL with durations as SMT with applications to schedulability analysis.",

abstract = "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.",

author = "Pedro, \{Andr{\'e} de Matos\} and Martin Leucker and David Pereira and Pinto, \{Jorge Sousa\}",

note = "DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.",

year = "2020",

doi = "10.1109/TASE49443.2020.00016",

language = "English",

pages = "49--56",

booktitle = "TASE",

}

TY - GEN

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

AU - Pedro, André de Matos

AU - Leucker, Martin

AU - Pereira, David

AU - Pinto, Jorge Sousa

N1 - DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

PY - 2020

Y1 - 2020

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

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

U2 - 10.1109/TASE49443.2020.00016

DO - 10.1109/TASE49443.2020.00016

M3 - Conference contribution

SP - 49

EP - 56

BT - TASE

ER -

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

Abstract

UN SDGs

Research Areas and Centers

Access to Document

Fingerprint

Cite this