Weight Monitoring with Linear Temporal Logic: Complexity and Decidability

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Abstract

Many important performance and reliability measures can be formalized as the accumulated values of weight functions. In this paper, we introduce an extension of linear time logic including past (LTL) with new operators that impose constraints on the accumulated weight along path fragments. The fragments are characterized by regular conditions formalized by deterministic finite automata (monitor DFA). This new logic covers properties expressible by several recently proposed formalisms. We study the model-checking problem for weighted transition systems, Markov chains and Markov decision processes with rational weights. While the general problem is undecidable, we provide algorithms and sharp complexity bounds for several sublogics that arise by restricting the monitoring DFA.

Details

OriginalspracheEnglisch
TitelCSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)v
Herausgeber (Verlag)Association for Computing Machinery (ACM), New York
Seiten1-10
ISBN (Print)978-1-4503-2886-9
PublikationsstatusVeröffentlicht - 2014
Peer-Review-StatusJa

Konferenz

TitelJoint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
KurztitelCSL-LICS '14
Veranstaltungsnummer
Dauer14 - 18 Juli 2014
BekanntheitsgradInternationale Veranstaltung
Ort
StadtWien
LandÖsterreich

Externe IDs

ORCID /0000-0002-5321-9343/work/142236737
Scopus 84905985299
ORCID /0000-0003-1724-2586/work/165453602

Schlagworte

Schlagwörter

  • weight monitoring, complexity, linear temporal logic, decidability