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/
Go to the corresponding OASIcs Volume Portal

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

Parametric Verification of Weighted Systems

pdf-format:
9.pdf (0.6 MB)

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI