文章基本信息

标题：Parametric Verification of Weighted Systems
本地全文：下载
作者：Peter Christoffersen ; Mikkel Hansen ; Anders Mariegaard 等
期刊名称：OASIcs : OpenAccess Series in Informatics
电子版ISSN：2190-6807
出版年度：2015
卷号：44
页码：77-90
DOI：10.4230/OASIcs.SynCoP.2015.77
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：parametric weighted transition systems; parametric weighted CTL; parametric model checking; well-quasi ordering; tool