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

25 Downloads (Pure)

Resumé

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.
OriginalsprogEngelsk
TidsskriftOpen Access Series in Informatics
Vol/bind44
Sider (fra-til)77-90
ISSN2190-6807
DOI
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

Workshop

Workshop2nd International Workshop on Synthesis of Complex Parameters
LokationMile End campus of Queen Mary University of London
LandStorbritannien
ByLondon
Periode11/04/201511/04/2015

Fingerprint

Model checking
Linear equations
Linear systems
Mathematical operators
Semantics

Citer dette

@inproceedings{5c261b633de5443da9832d3adcbb3f03,
title = "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.",
keywords = "parametric weighted transition systems, parametric weighted CTL, parametric model checking, well-quasi ordering, Tool",
author = "Peter Christoffersen and Mikkel Hansen and Anders Mariegaard and Ringsmose, {Julian Trier} and Larsen, {Kim Guldstrand} and Mardare, {Radu Iulian}",
year = "2015",
doi = "10.4230/OASIcs.SynCoP.2015.77",
language = "English",
volume = "44",
pages = "77--90",
journal = "Open Access Series in Informatics",
issn = "2190-6807",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH",

}

Parametric Verification of Weighted Systems. / Christoffersen, Peter; Hansen, Mikkel; Mariegaard, Anders; Ringsmose, Julian Trier; Larsen, Kim Guldstrand; Mardare, Radu Iulian.

I: Open Access Series in Informatics, Bind 44, 2015, s. 77-90.

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

TY - GEN

T1 - Parametric Verification of Weighted Systems

AU - Christoffersen, Peter

AU - Hansen, Mikkel

AU - Mariegaard, Anders

AU - Ringsmose, Julian Trier

AU - Larsen, Kim Guldstrand

AU - Mardare, Radu Iulian

PY - 2015

Y1 - 2015

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

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

KW - parametric weighted transition systems

KW - parametric weighted CTL

KW - parametric model checking

KW - well-quasi ordering

KW - Tool

U2 - 10.4230/OASIcs.SynCoP.2015.77

DO - 10.4230/OASIcs.SynCoP.2015.77

M3 - Conference article in Journal

VL - 44

SP - 77

EP - 90

JO - Open Access Series in Informatics

JF - Open Access Series in Informatics

SN - 2190-6807

ER -