A Decidable Recursive Logic for Weighted Transition Systems

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

Resumé

In this paper we develop and study the Recursive Weighted Logic (RWL), a multi-modal logic that expresses qualitative and quantitative properties of labelled weighted transition systems (LWSs). LWSs are transition systems labelled with actions and real-valued quantities representing the costs of transitions with respect to various resources. RWL uses first-order variables to measure local costs. The main syntactic operators are similar to the ones of timed logics for real-time systems. In addition, our logic is endowed, with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We prove that unlike in the case of the timed logics, the satisfiability problem for RWL is decidable. The proof uses a variant of the region construction technique used in literature with timed automata, which we adapt to the specific settings of RWL. This paper extends previous results that we have demonstrated for a similar but much more restrictive logic that can only use one variable for each type of resource to encode logical properties.
OriginalsprogEngelsk
TitelTheoretical Aspects of Computing – ICTAC 2014 : 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings
RedaktørerGabriel Ciobanu, Dominique Méry
Antal sider17
Vol/bind8687
ForlagSpringer Publishing Company
Publikationsdato2014
Sider460-476
ISBN (Trykt)978-3-319-10881-0
ISBN (Elektronisk)978-3-319-10882-7
DOI
StatusUdgivet - 2014
Begivenhed11th International Colloquium on Theoretical Aspects of Computing - Central University Library of Bucharest, Bucharest, Rumænien
Varighed: 17 sep. 201419 sep. 2014
Konferencens nummer: 11

Konference

Konference11th International Colloquium on Theoretical Aspects of Computing
Nummer11
LokationCentral University Library of Bucharest
LandRumænien
ByBucharest
Periode17/09/201419/09/2014
NavnLecture Notes in Computer Science
ISSN0302-9743

Fingerprint

Syntactics
Real time systems
Costs

Citer dette

Xue, B., Larsen, K. G., & Mardare, R. I. (2014). A Decidable Recursive Logic for Weighted Transition Systems. I G. Ciobanu, & D. Méry (red.), Theoretical Aspects of Computing – ICTAC 2014: 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings (Bind 8687, s. 460-476). Springer Publishing Company. Lecture Notes in Computer Science https://doi.org/10.1007/978-3-319-10882-7_27
Xue, Bingtian ; Larsen, Kim Guldstrand ; Mardare, Radu Iulian. / A Decidable Recursive Logic for Weighted Transition Systems. Theoretical Aspects of Computing – ICTAC 2014: 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings. red. / Gabriel Ciobanu ; Dominique Méry. Bind 8687 Springer Publishing Company, 2014. s. 460-476 (Lecture Notes in Computer Science).
@inproceedings{29295da8a3d54d22bc42e75424a5aa03,
title = "A Decidable Recursive Logic for Weighted Transition Systems",
abstract = "In this paper we develop and study the Recursive Weighted Logic (RWL), a multi-modal logic that expresses qualitative and quantitative properties of labelled weighted transition systems (LWSs). LWSs are transition systems labelled with actions and real-valued quantities representing the costs of transitions with respect to various resources. RWL uses first-order variables to measure local costs. The main syntactic operators are similar to the ones of timed logics for real-time systems. In addition, our logic is endowed, with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We prove that unlike in the case of the timed logics, the satisfiability problem for RWL is decidable. The proof uses a variant of the region construction technique used in literature with timed automata, which we adapt to the specific settings of RWL. This paper extends previous results that we have demonstrated for a similar but much more restrictive logic that can only use one variable for each type of resource to encode logical properties.",
keywords = "labelled weighted transition system, multi-modal logic, maximal fixed point computation",
author = "Bingtian Xue and Larsen, {Kim Guldstrand} and Mardare, {Radu Iulian}",
year = "2014",
doi = "10.1007/978-3-319-10882-7_27",
language = "English",
isbn = "978-3-319-10881-0",
volume = "8687",
series = "Lecture Notes in Computer Science",
publisher = "Springer Publishing Company",
pages = "460--476",
editor = "Gabriel Ciobanu and Dominique M{\'e}ry",
booktitle = "Theoretical Aspects of Computing – ICTAC 2014",
address = "United States",

}

Xue, B, Larsen, KG & Mardare, RI 2014, A Decidable Recursive Logic for Weighted Transition Systems. i G Ciobanu & D Méry (red), Theoretical Aspects of Computing – ICTAC 2014: 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings. bind 8687, Springer Publishing Company, Lecture Notes in Computer Science, s. 460-476, Bucharest, Rumænien, 17/09/2014. https://doi.org/10.1007/978-3-319-10882-7_27

A Decidable Recursive Logic for Weighted Transition Systems. / Xue, Bingtian; Larsen, Kim Guldstrand; Mardare, Radu Iulian.

Theoretical Aspects of Computing – ICTAC 2014: 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings. red. / Gabriel Ciobanu; Dominique Méry. Bind 8687 Springer Publishing Company, 2014. s. 460-476 (Lecture Notes in Computer Science).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - A Decidable Recursive Logic for Weighted Transition Systems

AU - Xue, Bingtian

AU - Larsen, Kim Guldstrand

AU - Mardare, Radu Iulian

PY - 2014

Y1 - 2014

N2 - In this paper we develop and study the Recursive Weighted Logic (RWL), a multi-modal logic that expresses qualitative and quantitative properties of labelled weighted transition systems (LWSs). LWSs are transition systems labelled with actions and real-valued quantities representing the costs of transitions with respect to various resources. RWL uses first-order variables to measure local costs. The main syntactic operators are similar to the ones of timed logics for real-time systems. In addition, our logic is endowed, with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We prove that unlike in the case of the timed logics, the satisfiability problem for RWL is decidable. The proof uses a variant of the region construction technique used in literature with timed automata, which we adapt to the specific settings of RWL. This paper extends previous results that we have demonstrated for a similar but much more restrictive logic that can only use one variable for each type of resource to encode logical properties.

AB - In this paper we develop and study the Recursive Weighted Logic (RWL), a multi-modal logic that expresses qualitative and quantitative properties of labelled weighted transition systems (LWSs). LWSs are transition systems labelled with actions and real-valued quantities representing the costs of transitions with respect to various resources. RWL uses first-order variables to measure local costs. The main syntactic operators are similar to the ones of timed logics for real-time systems. In addition, our logic is endowed, with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We prove that unlike in the case of the timed logics, the satisfiability problem for RWL is decidable. The proof uses a variant of the region construction technique used in literature with timed automata, which we adapt to the specific settings of RWL. This paper extends previous results that we have demonstrated for a similar but much more restrictive logic that can only use one variable for each type of resource to encode logical properties.

KW - labelled weighted transition system

KW - multi-modal logic

KW - maximal fixed point computation

U2 - 10.1007/978-3-319-10882-7_27

DO - 10.1007/978-3-319-10882-7_27

M3 - Article in proceeding

SN - 978-3-319-10881-0

VL - 8687

T3 - Lecture Notes in Computer Science

SP - 460

EP - 476

BT - Theoretical Aspects of Computing – ICTAC 2014

A2 - Ciobanu, Gabriel

A2 - Méry, Dominique

PB - Springer Publishing Company

ER -

Xue B, Larsen KG, Mardare RI. A Decidable Recursive Logic for Weighted Transition Systems. I Ciobanu G, Méry D, red., Theoretical Aspects of Computing – ICTAC 2014: 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings. Bind 8687. Springer Publishing Company. 2014. s. 460-476. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-10882-7_27