Activities per year
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.
Original language | English |
---|---|
Title of host publication | 2nd International Workshop on Synthesis of Complex Parameters, SynCoP 2015 |
Editors | Etienne Andre, Goran Frehse |
Number of pages | 14 |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
Publication date | 1 Nov 2015 |
Pages | 77-90 |
ISBN (Electronic) | 9783939897828 |
DOIs | |
Publication status | Published - 1 Nov 2015 |
Event | 2nd International Workshop on Synthesis of Complex Parameters, SynCoP 2015 - London, United Kingdom Duration: 11 Apr 2015 → … |
Conference
Conference | 2nd International Workshop on Synthesis of Complex Parameters, SynCoP 2015 |
---|---|
Country/Territory | United Kingdom |
City | London |
Period | 11/04/2015 → … |
Series | Open Access Series in Informatics |
---|---|
Volume | 44 |
ISSN | 2190-6807 |
Bibliographical note
Publisher Copyright:© Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, Julian Trier Ringsmose,Kim Guldstrand Larsen, and Radu Mardare; licensed under Creative Commons License CC-BY
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
Keywords
- Parametric model checking
- Parametric weighted CTL
- Parametric weighted transition systems
- Tool
- Well-quasi ordering
Fingerprint
Dive into the research topics of 'Parametric Verification of Weighted Systems'. Together they form a unique fingerprint.Activities
- 1 Conference presentations
-
2nd International Workshop on Synthesis of Complex Parameters
Mikkel Hansen (Speaker)
11 Apr 2015Activity: Talks and presentations › Conference presentations