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

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

2 Citationer (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.

Originalsprog	Engelsk
Titel	Perspectives of Systems Informatics : 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014
Redaktører	Andrei Voronkov, Irina Virbitskaite
Forlag	Springer
Publikationsdato	2015
Sider	216-231
ISBN (Trykt)	978-3-662-46822-7
ISBN (Elektronisk)	978-3-662-46823-4
DOI	https://doi.org/10.1007/978-3-662-46823-4_18
Status	Udgivet - 2015
Begivenhed	International Ershov Informatics Conference: PSI 2014 - St. Petersburg, Rusland Varighed: 24 jun. 2014 → 27 jun. 2014 Konferencens nummer: 9th

Konference

Konference	International Ershov Informatics Conference
Nummer	9th
Land/Område	Rusland
By	St. Petersburg
Periode	24/06/2014 → 27/06/2014

Navn	Lecture Notes in Computer Science
Nummer	8974
ISSN	0302-9743

Adgang til dokumentet

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

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

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
Projekter: Projekt › Forskning

Citationsformater

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. red. / Andrei Voronkov ; Irina Virbitskaite. Springer, 2015. s. 216-231 (Lecture Notes in Computer Science; Nr. 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. i A Voronkov & I Virbitskaite (red), Perspectives of Systems Informatics: 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Springer, Lecture Notes in Computer Science, nr. 8974, s. 216-231, International Ershov Informatics Conference, St. Petersburg, Rusland, 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. red. / Andrei Voronkov; Irina Virbitskaite. Springer, 2015. s. 216-231 (Lecture Notes in Computer Science; Nr. 8974).

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › 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. I Voronkov A, Virbitskaite I, red., Perspectives of Systems Informatics: 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Springer. 2015. s. 216-231. (Lecture Notes in Computer Science; Nr. 8974). doi: 10.1007/978-3-662-46823-4_18

Decidability and Expressiveness of Recursive Weighted Logic

Abstract

Konference

Adgang til dokumentet

AUB Link

Fingeraftryk

Projekter

IDEA4CPS: Foundations for Cyber-Physical Sytems

Citationsformater