Author name cluster

Simon Leßenich

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

CSL Conference 2015 Conference Paper

A Unified Approach to Boundedness Properties in MSO

Lukasz Kaiser
Martin Lang 0001
Simon Leßenich
Christof Löding

In the past years, extensions of monadic second-order logic (MSO) that can specify boundedness properties by the use of operators referring to the sizes of sets have been considered. In particular, the logics costMSO introduced by T. Colcombet and MSO+U by M. Bojanczyk were analyzed and connections to automaton models have been established to obtain decision procedures for these logics. In this work, we propose the logic quantitative counting MSO (qcMSO for short), which combines aspects from both costMSO and MSO+U. We show that both logics can be embedded into qcMSO in a natural way. Moreover, we provide a decidability proof for the theory of its weak variant (quantification only over finite sets) for the natural numbers with order and the infinite binary tree. These decidability results are obtained using a regular cost function extension of automatic structures called resource-automatic structures.

Details

Highlights Conference 2014 Conference Abstract

A Quantitative Counting Monadic Second-Order Logic

Simon Leßenich

We propose a new quantitative extension of monadic second-order logic, which we call qcMSO, that adds a mechanism to count the size of sets to MSO. We prove that this logic subsumes both MSO+U and costMSO, as for every formula of these logics there is a formula of qcMSO with the same evaluation. Furthermore, central costMSO questions such as boundedness or dominance can be expressed in qcMSO. Using techniques from the field of counter automata, we prove that the weak variant of our logic is decidable on both the infinite linear order and the infinite binary tree, which provides a uniform approach to algorithmic solutions for MSO+U and costMSO problems. Joint work with Łukasz Kaiser (LIAFA, CNRS & Université Paris Diderot - Paris 7) and Martin Lang (Informatik 7, RWTH Aachen University).

PDF Details

CSL Conference 2012 Conference Paper

A Counting Logic for Structure Transition Systems

Lukasz Kaiser
Simon Leßenich

Quantitative questions such as "what is the maximum number of tokens in a place of a Petri net? " or "what is the maximal reachable height of the stack of a pushdown automaton? " play a significant role in understanding models of computation. To study such problems in a systematic way, we introduce structure transition systems on which one can define logics that mix temporal expressions (e. g. reachability) with properties of a state (e. g. the height of the stack). We propose a counting logic Qmu[#MSO] which allows to express questions like the ones above, and also many boundedness problems studied so far. We show that Qmu[#MSO] has good algorithmic properties, in particular we generalize two standard methods in model checking, decomposition on trees and model checking through parity games, to this quantitative logic. These properties are used to prove decidability of Qmu[#MSO] on tree-producing pushdown systems, a generalization of both pushdown systems and regular tree grammars.

Details

CSL Conference 2012 Conference Paper

Banach-Mazur Games with Simple Winning Strategies

Erich Grädel
Simon Leßenich

We discuss several notions of "simple" winning strategies for Banach-Mazur games on graphs, such as positional strategies, move-counting or length-counting strategies, and strategies with a memory based on finite appearance records (FAR). We investigate classes of Banach-Mazur games that are determined via these kinds of winning strategies. Banach-Mazur games admit stronger determinacy results than classical graph games. For instance, all Banach-Mazur games with omega-regular winning conditions are positionally determined. Beyond the omega-regular winning conditions, we focus here on Muller conditions with infinitely many colours. We investigate the infinitary Muller conditions that guarantee positional determinacy for Banach-Mazur games. Further, we determine classes of such conditions that require infinite memory but guarantee determinacy via move-counting strategies, length-counting strategies, and FAR-strategies. We also discuss the relationships between these different notions of determinacy.

Details

MFCS Conference 2012 Conference Paper

Solving Counter Parity Games

Dietmar Berwanger
Lukasz Kaiser
Simon Leßenich

Abstract We study a class of parity games equipped with counters that evolve according to arbitrary non-negative affine functions. These games capture several cost models for dynamic systems from the literature. We present an elementary algorithm for computing the exact value of a counter parity game, which both generalizes previous results and improves their complexity. To this end, we introduce a class of ω -regular games with imperfect information and imperfect recall, solve them using automata-based techniques, and prove a correspondence between finite-memory strategies in such games and strategies in counter parity games.

Details