Parametric Verification of Weighted Systems

Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, Julian Trier Ringsmose, Kim Guldstrand Larsen, Radu Iulian Mardare

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

54 Downloads (Pure)


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.
TidsskriftOpen Access Series in Informatics
Sider (fra-til)77-90
StatusUdgivet - 2015
Begivenhed2nd International Workshop on Synthesis of Complex Parameters - Mile End campus of Queen Mary University of London, London, Storbritannien
Varighed: 11 apr. 201511 apr. 2015


Workshop2nd International Workshop on Synthesis of Complex Parameters
LokationMile End campus of Queen Mary University of London

Fingeraftryk Dyk ned i forskningsemnerne om 'Parametric Verification of Weighted Systems'. Sammen danner de et unikt fingeraftryk.