Parameter Synthesis for Simulation Distances Between Weighted Transition Systems
Authors
Mariegaard, Anders ; Ringsmose, Julian Trier
Term
4. term
Education
Publication year
2015
Submitted on
2015-06-01
Pages
40
Abstract
Denne afhandling undersøger parameter-syntese til at kontrollere simulationsafstand i parametriske vægtede transitionssystemer. Et vægtet transitionssystem beskriver adfærd som tilstande og overgange med vægte (fx tid, omkostning eller energi), der kan afhænge af parametre. Vi udvider den gængse forståelse af simulation, så overgangenes vægte må afvige pr. skridt, hvilket definerer en rettet afstand fra én tilstand til en anden. Derefter analyserer vi, hvad disse afstande betyder for systemegenskaber udtrykt i logik ved hjælp af en parametrisk udvidelse af Weighted CTL. Hovedbidraget er at bruge parametriske symbolske afhængighedsgrafer til at formulere, om afstanden mellem to tilstande er under en given tærskel, som et parameter-synteseproblem. Til dette formål præsenterer vi en global fastpunkt-algoritme og har implementeret den med en webbaseret front-end.
This thesis studies parameter synthesis for checking simulation distance in parametric weighted transition systems. A weighted transition system models behavior as states and transitions with weights (for example time, cost, or energy) that may depend on parameters. We extend the usual notion of simulation to tolerate per-step differences in transition weights, which induces a directed distance from one state to another. We then examine what these distances imply for system properties expressed in logic, using a parametric extension of Weighted CTL. The main contribution is to use parametric symbolic dependency graphs to encode whether the distance between two states stays below a chosen threshold as a parameter-synthesis problem. To solve it, we present a global fixed-point algorithm and provide an implementation with a web-based front end.
[This abstract was generated with the help of AI]
Keywords
Documents