Parametric verification of weighted systems

Christoffersen, Peter and Hansen, Mikkel and Mariegaard, Anders and Ringsmose, Julian Trier and Guldstrand Larsen, Kim and Mardare, Radu; André, Étienne and Frehse, Goran, eds. (2015) Parametric verification of weighted systems. In: 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Wadern, Germany, pp. 77-90. ISBN 9783939897828 (https://doi.org/10.4230/OASIcs.SynCoP.2015.77)

[thumbnail of Christoffersen-etal-SynCoP-2015-Parametric-verification-of-weighted-systems]
Preview
 Text. Filename: Christoffersen-etal-SynCoP-2015-Parametric-verification-of-weighted-systems.pdf
Final Published Version
License: Creative Commons Attribution 3.0 logo
Download (650kB)| Preview

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 modelchecking 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.

CORE (COnnecting REpositories)