Behavioural Analysis of Systems with Weights and Conditions
Sebastian Küpper · 2018
State-based systems have been used as powerful tools to analyse and model computer systems for a long time. Among many other applications, state based systems are one of the formalisms UML offers, they are used in natural language processing and play a particularly important role when designing compilers. Notably, every imperative program can be interpreted as a state-based system in a straight-forward way. However, many state-based system models that were extensively studied in the past focussed on single-system behaviour, as opposed to a uniform description of classes of systems, and are only fit to model what actions a system may perform, without taking the resources used or the likelihood for a transition to be taken into account. Therefore, state-based systems that enrich the semantics with a notion of weights that are accumulated over a run of the system, as well as conditions, which allow to specify classes of systems, rather than single systems, have been studied extensively recently. The aim of this thesis is two-fold: First, to identify commonalities between classical behavioural analysis for non-deterministic automata and labelled transition systems on the one hand, and weighted automata and conditional transition systems on the other hand, in a coalgebraic setting. Coalgebra offers a unifying theory that allows to develop prototype algorithms and to model various state-based systems in order to uniformly analyse very different system models using instances of the same general procedure. In this thesis, a coalgebraic algorithm, based on the well-known final chain, is presented, that can be instantiated to a large array of automata models. In addition, it is shown how automata with weights or conditions can be modelled coalgebraically in such a way that this algorithm yields the desired notion of behavioural equivalence.