Weighted Systems in Branching-Time: Behavioural Relations, Behavioural Distances, and their Logical Characterisations

Jensen, Mathias Claus

4. term

Computer Science, Master

2018

2018-06-08

62 pages

This Thesis presents the mathematical foundations required for reasoning about weighted systems in branching-time. In particular, using Weighted Kripke Structures as our models, we produce a range of behavioural equivalence that are an analogue to the traditional notion of Branching Bisimulation. We produce a behavioural equivalence relation for weighted behaviour in branching-time, namely Weighted Branching Bisimulation. We show that for a class of branching-compact WKS (ones WKS in which branching-behaviour accumulate weights only within closed sets of real numbers) are characterised by a suitable temporal logic, namely Weighted Branching Logic. This logic is based upon Computation Tree Logic without the next-operator, but with quantifiers that take weights into account as well. We develop a notion of relaxing our bisimulation, thereby allowing us to compare almost similar weighted systems with one another. In parallel, we develop a similar notion of relaxing our logic. Again, we show that these relaxed bisimulation are characterised by the relaxation of our logic. From this notion of relaxing our bisimulation we induce a distance between our weighted systems, by taking the greatest lower bounds of constants of relaxation. We show that this distance forms a behavioural pseudometric and that weighted systems that near each other also satisfy similar formulae. We introduce what it means for weighted systems to be cheaper than each other in branching-time, thus producing two behavioural preorders. The first being Possibly Cheaper Than, in which the cheaper system is only required to have at least one way to be cheaper than the other system. The second being Always Cheaper Than, in which the cheaper system is required to always be cheaper than the other. We also introduce a logic for reasoning about the bounds of a weighted system in branching-time. We show that fragments of this logic characterise our Possibly Cheaper Than relation and Always Cheaper Than relation on branching-compact WKS. Similarly to the previous, we also develop a notion of relaxing our Possibly Cheaper than preorder, and induce a distance from this. We show that this distance forms a hemimetric and that weighted systems near each other again satisfy similar formulae.

This Thesis presents the mathematical foundations required for reasoning about weighted systems in branching-time. In particular, using Weighted Kripke Structures as our models, we produce a range of behavioural equivalence that are an analogue to the traditional notion of Branching Bisimulation. We produce a behavioural equivalence relation for weighted behaviour in branching-time, namely Weighted Branching Bisimulation. We show that for a class of branching-compact WKS (ones WKS in which branching-behaviour accumulate weights only within closed sets of real numbers) are characterised by a suitable temporal logic, namely Weighted Branching Logic. This logic is based upon Computation Tree Logic without the next-operator, but with quantifiers that take weights into account as well. We develop a notion of relaxing our bisimulation, thereby allowing us to compare almost similar weighted systems with one another. In parallel, we develop a similar notion of relaxing our logic. Again, we show that these relaxed bisimulation are characterised by the relaxation of our logic. From this notion of relaxing our bisimulation we induce a distance between our weighted systems, by taking the greatest lower bounds of constants of relaxation. We show that this distance forms a behavioural pseudometric and that weighted systems that near each other also satisfy similar formulae. We introduce what it means for weighted systems to be cheaper than each other in branching-time, thus producing two behavioural preorders. The first being Possibly Cheaper Than, in which the cheaper system is only required to have at least one way to be cheaper than the other system. The second being Always Cheaper Than, in which the cheaper system is required to always be cheaper than the other. We also introduce a logic for reasoning about the bounds of a weighted system in branching-time. We show that fragments of this logic characterise our Possibly Cheaper Than relation and Always Cheaper Than relation on branching-compact WKS. Similarly to the previous, we also develop a notion of relaxing our Possibly Cheaper than preorder, and induce a distance from this. We show that this distance forms a hemimetric and that weighted systems near each other again satisfy similar formulae.

Download
View record in AAU Student Projects