eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
77
90
10.4230/OASIcs.SynCoP.2015.77
article
Parametric Verification of Weighted Systems
Christoffersen, Peter
Hansen, Mikkel
Mariegaard, Anders
Ringsmose, Julian Trier
Larsen, Kim Guldstrand
Mardare, Radu
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.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.77/OASIcs.SynCoP.2015.77.pdf
parametric weighted transition systems
parametric weighted CTL
parametric model checking
well-quasi ordering
tool