Cost Fixed Point Logic
Anouk Michelle Oudshoorn

Abstract:
Cost automata, introduced under the name ‘distance parity automata’, are in fact automata with something extra: counters. In the most simple case, the automaton has one counter which, during a transition, we can increase, check, reset or perform a combination of these actions. This machinery is very powerful. It can for instance count the number of a’s appearing in a word.
Cost automata stand out from other automata because they recognise cost functions instead of languages. The counters are used to evaluate the ‘cost’ of different runs, which gives rise to a function from words or trees to the natural numbers. Noteworthy is that these counters are initialised for the purpose of bookkeeping certain patterns in the run and as such their actual values are not so important to us.
Next to cost automata, cost games are quite well understood and elaborated on too, but the logical counterpart has remained underdeveloped. In this thesis we propose a notion of cost formulas that connects well to the automata and game counterpart. This is obtained by enriching the modal μ-calculus with an appropriate form of ‘counters’ that can represent cost functions. We further establish a sequent calculus for a fragment of out logical framework which is sound and complete with respect to our ‘cost semantics’, though we leave open the question of utilising the system for deciding boundedness.