License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.SynCoP.2015.77
URN: urn:nbn:de:0030-drops-56115
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5611/
Christoffersen, Peter ;
Hansen, Mikkel ;
Mariegaard, Anders ;
Ringsmose, Julian Trier ;
Larsen, Kim Guldstrand ;
Mardare, Radu
Parametric Verification of Weighted Systems
Abstract
This paper addresses the problem of parametric model checking for weighted transition systems. We consider transition systems labelled with linear equations over a set of parameters and we use them to provide semantics for a parametric version of weighted CTL where the until and next operators are themselves indexed with linear equations. The parameters change the model-checking problem into a problem of computing a linear system of inequalities that characterizes the parameters that guarantee the satisfiability. To address this problem, we use parametric dependency graphs (PDGs) and we propose a global update function that yields an assignment
to each node in a PDG. For an iterative application of the function, we prove that a fixed point assignment to PDG nodes exists and the set of assignments constitutes a well-quasi ordering, thus ensuring that the fixed point assignment can be found after finitely many iterations. To demonstrate the utility of our technique, we have implemented a prototype tool that computes the constraints on parameters for model checking problems.
BibTeX - Entry
@InProceedings{christoffersen_et_al:OASIcs:2015:5611,
author = {Peter Christoffersen and Mikkel Hansen and Anders Mariegaard and Julian Trier Ringsmose and Kim Guldstrand Larsen and Radu Mardare},
title = {{Parametric Verification of Weighted Systems}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {77--90},
series = {OpenAccess Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {{\'E}tienne Andr{\'e} and Goran Frehse},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5611},
URN = {urn:nbn:de:0030-drops-56115},
doi = {10.4230/OASIcs.SynCoP.2015.77},
annote = {Keywords: parametric weighted transition systems, parametric weighted CTL, parametric model checking, well-quasi ordering, tool}
}
Keywords: |
|
parametric weighted transition systems, parametric weighted CTL, parametric model checking, well-quasi ordering, tool |
Collection: |
|
2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) |
Issue Date: |
|
2015 |
Date of publication: |
|
03.12.2015 |