DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2015.441

A Unified Approach to Boundedness Properties in MSO

Authors: Lukasz Kaiser, Martin Lang, Simon Leßenich, and Christof Löding

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract

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.

Cite as

Lukasz Kaiser, Martin Lang, Simon Leßenich, and Christof Löding. A Unified Approach to Boundedness Properties in MSO. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 441-456, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kaiser_et_al:LIPIcs.CSL.2015.441,
  author =	{Kaiser, Lukasz and Lang, Martin and Le{\ss}enich, Simon and L\"{o}ding, Christof},
  title =	{{A Unified Approach to Boundedness Properties in MSO}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{441--456},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.441},
  URN =		{urn:nbn:de:0030-drops-54309},
  doi =		{10.4230/LIPIcs.CSL.2015.441},
  annote =	{Keywords: quantitative logics, monadic second order logic, boundedness, automatic structures, tree automata}
}

Document

DOI: 10.4230/LIPIcs.CSL.2012.305

Banach-Mazur Games with Simple Winning Strategies

Authors: Erich Grädel and Simon Leßenich

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract

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.

Cite as

Erich Grädel and Simon Leßenich. Banach-Mazur Games with Simple Winning Strategies. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 305-319, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2012.305,
  author =	{Gr\"{a}del, Erich and Le{\ss}enich, Simon},
  title =	{{Banach-Mazur Games with Simple Winning Strategies}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{305--319},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.305},
  URN =		{urn:nbn:de:0030-drops-36806},
  doi =		{10.4230/LIPIcs.CSL.2012.305},
  annote =	{Keywords: Banach-Mazur games, winning strategies, positional determinacy, Muller winning conditions}
}

Document

DOI: 10.4230/LIPIcs.CSL.2012.366

A Counting Logic for Structure Transition Systems

Authors: Lukasz Kaiser and Simon Leßenich

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract

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.

Cite as

Lukasz Kaiser and Simon Leßenich. A Counting Logic for Structure Transition Systems. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 366-380, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kaiser_et_al:LIPIcs.CSL.2012.366,
  author =	{Kaiser, Lukasz and Le{\ss}enich, Simon},
  title =	{{A Counting Logic for Structure Transition Systems}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{366--380},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.366},
  URN =		{urn:nbn:de:0030-drops-36848},
  doi =		{10.4230/LIPIcs.CSL.2012.366},
  annote =	{Keywords: Logic in Computer Science, Quantitative Logics, Model Checking}
}

3 Search Results for "Leßenich, Simon"

A Unified Approach to Boundedness Properties in MSO

Abstract

Cite as

Banach-Mazur Games with Simple Winning Strategies

Abstract

Cite as

A Counting Logic for Structure Transition Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message