Abschnittsübersicht

  • May 26
    • George Rahonis, Aristotle University of Thessaloniki:
    Quantitative logics

    We present a quantitative MSO-logic for finite and infinite words over semirings. Weighted MSO-formulas are represented as formal power series. For this, we require our semirings to satisfy concrete completeness axioms. The semantics of sentences from a fragment of this logic coincide with the behaviors of weighted automata. If the underlying semiring is the max-plus semiring, then we consider for our logic discounting parameters, so that infinite sums exist. Next, we deal with quantitative LTL with discounting. Again weighted LTL-formulas are represented as formal power series over infinite words. Every weighted LTL-formula with a restricted syntax is expressively equivalent to a weighted automaton. We conclude by addressing a list of open problems connected to potential practical applications.