Weighted Systems in Branching-Time: Behavioural Relations, Behavioural Distances, and their Logical Characterisations
Author
Jensen, Mathias Claus
Term
4. term
Education
Publication year
2018
Submitted on
2018-06-08
Pages
62
Abstract
Mange systemer kan beskrives som tilstandsgrafer, hvor overgange har vægte (fx omkostninger, sandsynligheder eller ressourcer). Denne afhandling giver de matematiske grundlag for at ræsonnere om sådanne vægtede systemer i forgrenende tid, hvor flere mulige fremtider eksisterer samtidig. Vi bruger Vægtede Kripke-strukturer som model og opstiller en række adfærdslige ækvivalensbegreber, herunder Vægtet Forgrenings-bisimulation, som udvider klassisk forgrenings-bisimulation til også at matche vægte. Vi introducerer desuden Weighted Branching Logic, en temporallogik baseret på CTL uden næste-operatoren, men med kvantorer der tager vægte i betragtning. Vi viser, at for en klasse af forgrenings-kompakte Vægtede Kripke-strukturer (hvor vægtakkumulationer kun ligger i lukkede mængder af reelle tal), karakteriserer denne logik vores ækvivalens: to systemer er ækvivalente præcis når de opfylder de samme formler i logikken. For at sammenligne næsten ens systemer tillader vi en afslapning af bisimulationen, så små afvigelser i vægte accepteres. Parallelt afslapper vi logikken. Vi viser, at de afslappede bisimulationer stadig karakteriseres af den tilsvarende afslappede logik. Ud fra afslapningen definerer vi en afstand mellem vægtede systemer som den mindste tolerance, der skal til for at matche deres adfærd. Denne afstand er en adfærdspseudometrik, og systemer der ligger tæt på hinanden, opfylder også lignende formler. Vi indfører også, hvad det vil sige, at et vægtet system er billigere end et andet i forgrenende tid, og får derved to adfærdslige præordner: Måske billigere end (hvor der findes mindst én gren, der er billigere) og Altid billigere end (hvor alle grene er billigere). Vi giver en logik til at ræsonnere om grænser for et systems vægtede adfærd og viser, at dele af denne logik karakteriserer de to præordner på forgrenings-kompakte strukturer. Endelig afslapper vi også Måske billigere end-præordnen og definerer en dertil hørende afstand. Denne afstand er en hemimetrik (muligt asymmetrisk), og igen gælder, at nærliggende systemer opfylder lignende formler.
Many systems can be seen as state graphs where transitions carry weights (such as costs, probabilities, or resources). This thesis develops the mathematical foundations for reasoning about such weighted systems in branching time, where multiple possible futures coexist. We use Weighted Kripke Structures as our model and introduce a family of behavioral equivalences, including Weighted Branching Bisimulation, which extends classical branching bisimulation to also match weights. We further introduce Weighted Branching Logic, a temporal logic based on CTL without the next operator, augmented with quantifiers that account for weights. We show that for a class of branching-compact Weighted Kripke Structures (where accumulated weights fall within closed sets of real numbers), this logic characterizes our equivalence: two systems are equivalent precisely when they satisfy the same formulas in the logic. To compare systems that are almost alike, we relax our bisimulation to allow small deviations in weights and, in parallel, define a corresponding relaxation of the logic. We prove that the relaxed bisimulations are characterized by the relaxed logic. From this relaxation we define a distance between weighted systems as the smallest tolerance needed to match their behaviors. This yields a behavioral pseudometric, and systems that are close under this distance satisfy similar formulas. We also formalize what it means for one weighted system to be cheaper than another in branching time, yielding two behavioral preorders: Possibly Cheaper Than (there exists at least one cheaper branch) and Always Cheaper Than (every branch is cheaper). We provide a logic for reasoning about bounds of a weighted system and show that fragments of this logic characterize these two preorders on branching-compact structures. Finally, we relax the Possibly Cheaper Than preorder and define an induced distance. This distance is a hemimetric (potentially asymmetric), and, again, nearby systems satisfy similar formulas.
[This abstract was generated with the help of AI]
Documents