Local Model Checking of Weighted CTL with Upper-Bound Constraints

Jonas Finnemann Jensen; Kim Guldstrand Larsen; Jiri Srba; Lars Østergaard

doi:10.1007/978-3-642-39176-7_12

Local Model Checking of Weighted CTL with Upper-Bound Constraints

Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiri Srba, Lars Østergaard

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

7 Citations (Scopus)

Abstract

We present a symbolic extension of dependency graphs by Liu and Smolka in order to model-check weighted Kripke structures against the logic CTL with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers in order to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages of our approach compared to the direct encoding of the model checking problem into dependency graphs. We implement all algorithms in a publicly available tool prototype and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of “witnesses”.

Original language	English
Title of host publication	Model Checking Software : 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings
Editors	Ezio Bartocci, C. R. Ramakrishnan
Number of pages	18
Place of Publication	Holland
Publisher	Springer Publishing Company
Publication date	2013
Pages	178-195
ISBN (Print)	978-3-642-39175-0
DOIs	https://doi.org/10.1007/978-3-642-39176-7_12
Publication status	Published - 2013
Event	International SPIN Symposium on Model Checking of Software - Stony Brook, Stony Brook, NY, United States Duration: 8 Jul 2013 → 9 Jul 2013 Conference number: 20

Conference

Conference	International SPIN Symposium on Model Checking of Software
Number	20
Location	Stony Brook
Country/Territory	United States
City	Stony Brook, NY
Period	08/07/2013 → 09/07/2013

Series	Lecture Notes in Computer Science
Volume	7976
ISSN	0302-9743

Keywords

CTL, weighted Kripke structure, model checking, on-the-fly algorithm

Access to Document

10.1007/978-3-642-39176-7_12

http://link.springer.com/chapter/10.1007%2F978-3-642-39176-7_12

AUB Link

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

Cite this

Jensen, J. F., Larsen, K. G., Srba, J., & Østergaard, L. (2013). Local Model Checking of Weighted CTL with Upper-Bound Constraints. In E. Bartocci, & C. R. Ramakrishnan (Eds.), Model Checking Software : 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings (pp. 178-195 ). Springer Publishing Company. https://doi.org/10.1007/978-3-642-39176-7_12

Jensen, Jonas Finnemann ; Larsen, Kim Guldstrand ; Srba, Jiri et al. / Local Model Checking of Weighted CTL with Upper-Bound Constraints. Model Checking Software : 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings. editor / Ezio Bartocci ; C. R. Ramakrishnan. Holland : Springer Publishing Company, 2013. pp. 178-195 (Lecture Notes in Computer Science, Vol. 7976).

@inproceedings{77bea1ea5fee498b985e43f96b5fef83,

title = "Local Model Checking of Weighted CTL with Upper-Bound Constraints",

abstract = "We present a symbolic extension of dependency graphs by Liu and Smolka in order to model-check weighted Kripke structures against the logic CTL with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers in order to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages of our approach compared to the direct encoding of the model checking problem into dependency graphs. We implement all algorithms in a publicly available tool prototype and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of “witnesses”.",

keywords = "CTL, weighted Kripke structure, model checking, on-the-fly algorithm",

author = "Jensen, {Jonas Finnemann} and Larsen, {Kim Guldstrand} and Jiri Srba and Lars {\O}stergaard",

year = "2013",

doi = "10.1007/978-3-642-39176-7_12",

language = "English",

isbn = "978-3-642-39175-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer Publishing Company",

pages = "178--195 ",

editor = "Ezio Bartocci and Ramakrishnan, {C. R. }",

booktitle = "Model Checking Software",

address = "United States",

note = "International SPIN Symposium on Model Checking of Software, SPIN ; Conference date: 08-07-2013 Through 09-07-2013",

}

Jensen, JF, Larsen, KG , Srba, J & Østergaard, L 2013, Local Model Checking of Weighted CTL with Upper-Bound Constraints. in E Bartocci & CR Ramakrishnan (eds), Model Checking Software : 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings. Springer Publishing Company, Holland, Lecture Notes in Computer Science, vol. 7976, pp. 178-195 , International SPIN Symposium on Model Checking of Software, Stony Brook, NY, United States, 08/07/2013. https://doi.org/10.1007/978-3-642-39176-7_12

Local Model Checking of Weighted CTL with Upper-Bound Constraints. / Jensen, Jonas Finnemann; Larsen, Kim Guldstrand ; Srba, Jiri et al.
Model Checking Software : 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings. ed. / Ezio Bartocci; C. R. Ramakrishnan. Holland: Springer Publishing Company, 2013. p. 178-195 (Lecture Notes in Computer Science, Vol. 7976).

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

TY - GEN

T1 - Local Model Checking of Weighted CTL with Upper-Bound Constraints

AU - Jensen, Jonas Finnemann

AU - Larsen, Kim Guldstrand

AU - Srba, Jiri

AU - Østergaard, Lars

N1 - Conference code: 20

PY - 2013

Y1 - 2013

N2 - We present a symbolic extension of dependency graphs by Liu and Smolka in order to model-check weighted Kripke structures against the logic CTL with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers in order to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages of our approach compared to the direct encoding of the model checking problem into dependency graphs. We implement all algorithms in a publicly available tool prototype and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of “witnesses”.

AB - We present a symbolic extension of dependency graphs by Liu and Smolka in order to model-check weighted Kripke structures against the logic CTL with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers in order to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages of our approach compared to the direct encoding of the model checking problem into dependency graphs. We implement all algorithms in a publicly available tool prototype and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of “witnesses”.

KW - CTL, weighted Kripke structure, model checking, on-the-fly algorithm

U2 - 10.1007/978-3-642-39176-7_12

DO - 10.1007/978-3-642-39176-7_12

M3 - Article in proceeding

SN - 978-3-642-39175-0

T3 - Lecture Notes in Computer Science

SP - 178

EP - 195

BT - Model Checking Software

A2 - Bartocci, Ezio

A2 - Ramakrishnan, C. R.

PB - Springer Publishing Company

CY - Holland

T2 - International SPIN Symposium on Model Checking of Software

Y2 - 8 July 2013 through 9 July 2013

ER -

Jensen JF, Larsen KG , Srba J, Østergaard L. Local Model Checking of Weighted CTL with Upper-Bound Constraints. In Bartocci E, Ramakrishnan CR, editors, Model Checking Software : 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings. Holland: Springer Publishing Company. 2013. p. 178-195 . (Lecture Notes in Computer Science, Vol. 7976). doi: 10.1007/978-3-642-39176-7_12

Local Model Checking of Weighted CTL with Upper-Bound Constraints

Abstract

Conference

Keywords

Access to Document

AUB Link

Fingerprint

Cite this