A decidable recursive logic forweighted transition systems

Kim Guldstrand Larsen, Radu Mardare, Bingtian Xue

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

2 Citations (Scopus)

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.

LanguageEnglish
Title of host publicationTheoretical Aspects of Computing – ICTAC 2014
Subtitle of host publicationProceedings of 11th International Colloquium Bucharest, Romania, September 17-19, 2014
EditorsGabriel Ciobanu, Dominique Méry
Place of PublicationCham
PublisherSpringer
Pages460-476
Number of pages17
ISBN (Print)9783319108810, 9783319108827
DOIs
Publication statusPublished - 23 Sep 2014

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume8687
ISSN (Print)0302-9743

Fingerprint

Transition Systems
Logic
Syntactics
Real time systems
Costs
Multi-modal Logic
Logical property
Labeled Transition System
Resources
Timed Automata
Satisfiability Problem
Express
First-order
Real-time
Operator

Keywords

  • labelled weighted transition system
  • maximal fixed point computation
  • multi-modal logic

Cite this

Larsen, K. G., Mardare, R., & Xue, B. (2014). A decidable recursive logic forweighted transition systems. In G. Ciobanu, & D. Méry (Eds.), Theoretical Aspects of Computing – ICTAC 2014: Proceedings of 11th International Colloquium Bucharest, Romania, September 17-19, 2014 (pp. 460-476). (Lecture Notes in Computer Science; Vol. 8687). Cham: Springer. https://doi.org/10.1007/978-3-319-10882-7_27
Larsen, Kim Guldstrand ; Mardare, Radu ; Xue, Bingtian. / A decidable recursive logic forweighted transition systems. Theoretical Aspects of Computing – ICTAC 2014: Proceedings of 11th International Colloquium Bucharest, Romania, September 17-19, 2014. editor / Gabriel Ciobanu ; Dominique Méry. Cham : Springer, 2014. pp. 460-476 (Lecture Notes in Computer Science).
@inproceedings{95f5d030a3de416b8064432866abe719,
title = "A decidable recursive logic forweighted 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, maximal fixed point computation, multi-modal logic",
author = "Larsen, {Kim Guldstrand} and Radu Mardare and Bingtian Xue",
year = "2014",
month = "9",
day = "23",
doi = "10.1007/978-3-319-10882-7_27",
language = "English",
isbn = "9783319108810",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "460--476",
editor = "Gabriel Ciobanu and Dominique M{\'e}ry",
booktitle = "Theoretical Aspects of Computing – ICTAC 2014",

}

Larsen, KG, Mardare, R & Xue, B 2014, A decidable recursive logic forweighted transition systems. in G Ciobanu & D Méry (eds), Theoretical Aspects of Computing – ICTAC 2014: Proceedings of 11th International Colloquium Bucharest, Romania, September 17-19, 2014. Lecture Notes in Computer Science, vol. 8687, Springer, Cham, pp. 460-476. https://doi.org/10.1007/978-3-319-10882-7_27

A decidable recursive logic forweighted transition systems. / Larsen, Kim Guldstrand; Mardare, Radu; Xue, Bingtian.

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - A decidable recursive logic forweighted transition systems

AU - Larsen, Kim Guldstrand

AU - Mardare, Radu

AU - Xue, Bingtian

PY - 2014/9/23

Y1 - 2014/9/23

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 - maximal fixed point computation

KW - multi-modal logic

UR - http://www.scopus.com/inward/record.url?scp=84921790649&partnerID=8YFLogxK

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

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

M3 - Conference contribution book

SN - 9783319108810

SN - 9783319108827

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

CY - Cham

ER -

Larsen KG, Mardare R, Xue B. A decidable recursive logic forweighted transition systems. In Ciobanu G, Méry D, editors, Theoretical Aspects of Computing – ICTAC 2014: Proceedings of 11th International Colloquium Bucharest, Romania, September 17-19, 2014. Cham: Springer. 2014. p. 460-476. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-10882-7_27