Decidability and Expressiveness of Recursive Weighted Logic

Bingtian Xue; Kim Guldstrand Larsen; Radu Iulian Mardare

doi:10.1007/978-3-662-46823-4_18

Decidability and Expressiveness of Recursive Weighted Logic

Bingtian Xue, Kim Guldstrand Larsen, Radu Iulian Mardare

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

2 Citations (Scopus)

Abstract

Labelled weighted transition systems (LWSs) are transition systems labelled with actions and real numbers. The numbers represent the costs of the corresponding actions in terms of resources. RecursiveWeighted Logic (RWL) is a multimodal logic that expresses qualitative and quantitative properties of LWSs. It is endowed with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We demonstrate that RWL is sufficiently expressive to characterize weighted-bisimilarity of LWSs. In addition, we prove that the logic is decidable, i.e., the satisfiability problem for RWL can be algorithmically solved.

Original language	English
Title of host publication	Perspectives of Systems Informatics : 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014
Editors	Andrei Voronkov, Irina Virbitskaite
Publisher	Springer
Publication date	2015
Pages	216-231
ISBN (Print)	978-3-662-46822-7
ISBN (Electronic)	978-3-662-46823-4
DOIs	https://doi.org/10.1007/978-3-662-46823-4_18
Publication status	Published - 2015
Event	International Ershov Informatics Conference: PSI 2014 - St. Petersburg, Russian Federation Duration: 24 Jun 2014 → 27 Jun 2014 Conference number: 9th

Conference

Conference	International Ershov Informatics Conference
Number	9th
Country/Territory	Russian Federation
City	St. Petersburg
Period	24/06/2014 → 27/06/2014

Series	Lecture Notes in Computer Science
Number	8974
ISSN	0302-9743

Keywords

labelled weighted transition system
maximal fixed point
Hennessy- Milner property
satisfiability

Access to Document

10.1007/978-3-662-46823-4_18

AUB Link

Search for the material in Aalborg University Library's search engine

IDEA4CPS: Foundations for Cyber-Physical Sytems
Larsen, K. G., Skou, A., Nielsen, B., Bulychev, P., Ravn, A. P. & Poulsen, D. B.
01/04/2011 → 30/04/2015
Project: Research

Cite this

Xue, Bingtian ; Larsen, Kim Guldstrand ; Mardare, Radu Iulian. / Decidability and Expressiveness of Recursive Weighted Logic. Perspectives of Systems Informatics: 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. editor / Andrei Voronkov ; Irina Virbitskaite. Springer, 2015. pp. 216-231 (Lecture Notes in Computer Science; No. 8974).

@inproceedings{3d0b33f8b9f84d54b2b9a3a71607af8b,

title = "Decidability and Expressiveness of Recursive Weighted Logic",

abstract = "Labelled weighted transition systems (LWSs) are transition systems labelled with actions and real numbers. The numbers represent the costs of the corresponding actions in terms of resources. RecursiveWeighted Logic (RWL) is a multimodal logic that expresses qualitative and quantitative properties of LWSs. It is endowed with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We demonstrate that RWL is sufficiently expressive to characterize weighted-bisimilarity of LWSs. In addition, we prove that the logic is decidable, i.e., the satisfiability problem for RWL can be algorithmically solved.",

keywords = "labelled weighted transition system, maximal fixed point, Hennessy- Milner property, satisfiability",

author = "Bingtian Xue and Larsen, {Kim Guldstrand} and Mardare, {Radu Iulian}",

year = "2015",

doi = "10.1007/978-3-662-46823-4_18",

language = "English",

isbn = "978-3-662-46822-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "8974",

pages = "216--231",

editor = "Andrei Voronkov and Irina Virbitskaite",

booktitle = "Perspectives of Systems Informatics",

address = "Germany",

note = "International Ershov Informatics Conference : PSI 2014 ; Conference date: 24-06-2014 Through 27-06-2014",

}

Xue, B, Larsen, KG & Mardare, RI 2015, Decidability and Expressiveness of Recursive Weighted Logic. in A Voronkov & I Virbitskaite (eds), Perspectives of Systems Informatics: 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Springer, Lecture Notes in Computer Science, no. 8974, pp. 216-231, International Ershov Informatics Conference, St. Petersburg, Russian Federation, 24/06/2014. https://doi.org/10.1007/978-3-662-46823-4_18

Decidability and Expressiveness of Recursive Weighted Logic. / Xue, Bingtian; Larsen, Kim Guldstrand; Mardare, Radu Iulian.
Perspectives of Systems Informatics: 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. ed. / Andrei Voronkov; Irina Virbitskaite. Springer, 2015. p. 216-231 (Lecture Notes in Computer Science; No. 8974).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

T1 - Decidability and Expressiveness of Recursive Weighted Logic

AU - Xue, Bingtian

AU - Larsen, Kim Guldstrand

AU - Mardare, Radu Iulian

N1 - Conference code: 9th

PY - 2015

Y1 - 2015

N2 - Labelled weighted transition systems (LWSs) are transition systems labelled with actions and real numbers. The numbers represent the costs of the corresponding actions in terms of resources. RecursiveWeighted Logic (RWL) is a multimodal logic that expresses qualitative and quantitative properties of LWSs. It is endowed with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We demonstrate that RWL is sufficiently expressive to characterize weighted-bisimilarity of LWSs. In addition, we prove that the logic is decidable, i.e., the satisfiability problem for RWL can be algorithmically solved.

AB - Labelled weighted transition systems (LWSs) are transition systems labelled with actions and real numbers. The numbers represent the costs of the corresponding actions in terms of resources. RecursiveWeighted Logic (RWL) is a multimodal logic that expresses qualitative and quantitative properties of LWSs. It is endowed with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We demonstrate that RWL is sufficiently expressive to characterize weighted-bisimilarity of LWSs. In addition, we prove that the logic is decidable, i.e., the satisfiability problem for RWL can be algorithmically solved.

KW - labelled weighted transition system

KW - maximal fixed point

KW - Hennessy- Milner property

KW - satisfiability

U2 - 10.1007/978-3-662-46823-4_18

DO - 10.1007/978-3-662-46823-4_18

M3 - Article in proceeding

SN - 978-3-662-46822-7

T3 - Lecture Notes in Computer Science

SP - 216

EP - 231

BT - Perspectives of Systems Informatics

A2 - Voronkov, Andrei

A2 - Virbitskaite, Irina

PB - Springer

T2 - International Ershov Informatics Conference

Y2 - 24 June 2014 through 27 June 2014

ER -

Xue B, Larsen KG, Mardare RI. Decidability and Expressiveness of Recursive Weighted Logic. In Voronkov A, Virbitskaite I, editors, Perspectives of Systems Informatics: 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Springer. 2015. p. 216-231. (Lecture Notes in Computer Science; No. 8974). doi: 10.1007/978-3-662-46823-4_18

Decidability and Expressiveness of Recursive Weighted Logic

Abstract

Conference

Keywords

Access to Document

AUB Link

Fingerprint

Projects

IDEA4CPS: Foundations for Cyber-Physical Sytems

Cite this