Author name cluster

Martin Lang

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.

3 papers

1 author row

Highlights Conference 2015 Conference Abstract

A unified approach to boundedness properties in MSO

Martin Lang

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. 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 decidability proofs 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. This is joint work with Simon Leßenich, Christof Löding and Lukasz Kaiser. It is currently submitted for publication.

Details

Highlights Conference 2014 Conference Abstract

First-order Cost Logics and Automatic Structures

Martin Lang

We provide new characterizations of the class of regular cost functions (Colcombet 2009) in terms of different quantitative first-order logics. This result extends a classical result connecting the regular languages with the languages definable by a first-order formula over the infinite (binary) tree of finite words with equal length predicate. Furthermore, we use these results to identify a structure that is complete for the class of resource automatic structures and investigate approaches how resource (tree) automatic structures can be used to obtain decidability results for costWMSO and WMSO+U as well. Parts of this are joint work with Simon Leßenich, Christof Löding and Amaldev Manuel and will appear in MFCS 2014 as Definability and Transformations for Cost Logics and Automatic Structures

PDF Details

Highlights Conference 2013 Conference Abstract

Resource reachability games on pushdown graphs

Martin Lang
Christof Löding

We consider two-player games on the configuration graph of pushdown systems with an additional finite set of non-negative integer counters. These counters can be incremented, reset to zero or left unchanged by the transition rules of the pushdown system. We associate the cost of a play with the highest counter value that occurs and look at a combined reachability and cost-limit winning condition. Is there a uniform cost-bound k such that one can win from a set of configurations A with this bound? We provide a solution to this question by an extension of the well-known saturation principle.

PDF Details