2026-10-06T16:56:51Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5611 2024-03-06T09:29:42Z ddc:004 open_access

Parametric Verification of Weighted Systems Christoffersen, Peter Hansen, Mikkel Mariegaard, Anders Ringsmose, Julian Trier Larsen, Kim Guldstrand Mardare, Radu parametric weighted transition systems parametric weighted CTL parametric model checking well-quasi ordering tool 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Peter Christoffersen and Mikkel Hansen and Anders Mariegaard and Julian Trier Ringsmose and Kim Guldstrand Larsen and Radu Mardare 2015 Is Part Of OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.SynCoP.2015.77 urn:nbn:de:0030-drops-56115 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.77 eng https://creativecommons.org/licenses/by/3.0/legalcode