Showing 1–15 of 15 results for author: Blumensath, A

Simple Classes of Automatic Structures

Authors: Achim Blumensath

Abstract: We study two subclasses of the class of automatic structures: automatic structures of polynomial growth and Presburger structures. We present algebraic characterisations of the groups and the equivalence structures in these two classes. We study two subclasses of the class of automatic structures: automatic structures of polynomial growth and Presburger structures. We present algebraic characterisations of the groups and the equivalence structures in these two classes. △ Less

Submitted 28 May, 2025; originally announced May 2025.

Automata for Enriched Trees and Applications

Authors: Achim Blumensath

Abstract: We study trees where each successor set is equipped with some additional structure. We introduce a family of automaton models for such trees and prove their equivalence to certain fixed-point logics. As a consequence we obtain characterisations of various variants of monadic second-order logic in terms of automata and fixed-point logics. Finally, we use our machinery to give a simplified proof of… ▽ More We study trees where each successor set is equipped with some additional structure. We introduce a family of automaton models for such trees and prove their equivalence to certain fixed-point logics. As a consequence we obtain characterisations of various variants of monadic second-order logic in terms of automata and fixed-point logics. Finally, we use our machinery to give a simplified proof of the Theorem of Muchnik and we derive several variants of this theorem for other logics. △ Less

Submitted 21 February, 2025; originally announced February 2025.

Some Remarks on First-Order Definable Tree Languages

Authors: Achim Blumensath

Abstract: We study the question of whether a given regular language of finite trees can be defined in first-order logic. We develop an algebraic approach to address this question and we use it to derive several necessary and sufficient conditions for definability (but unfortunately no condition that is both). The main difference of our results to those from the literature is that our conditions are decidabl… ▽ More We study the question of whether a given regular language of finite trees can be defined in first-order logic. We develop an algebraic approach to address this question and we use it to derive several necessary and sufficient conditions for definability (but unfortunately no condition that is both). The main difference of our results to those from the literature is that our conditions are decidable. △ Less

Submitted 1 July, 2024; originally announced July 2024.

The Expansion Problem for Infinite Trees

Authors: Achim Blumensath

Abstract: We study Ramsey like theorems for infinite trees and similar combinatorial tools. As an application we consider the expansion problem for tree algebras. We study Ramsey like theorems for infinite trees and similar combinatorial tools. As an application we consider the expansion problem for tree algebras. △ Less

Submitted 29 April, 2025; v1 submitted 2 August, 2023; originally announced August 2023.

The Power-Set Construction for Tree Algebras

Authors: Achim Blumensath

Abstract: We study power-set operations on classes of trees and tree algebras. Our main result consists of a distributive law between the tree monad and the upwards-closed power-set monad, in the case where all trees are assumed to be linear. For non-linear ones, we prove that such a distributive law does not exist. We study power-set operations on classes of trees and tree algebras. Our main result consists of a distributive law between the tree monad and the upwards-closed power-set monad, in the case where all trees are assumed to be linear. For non-linear ones, we prove that such a distributive law does not exist. △ Less

Submitted 2 November, 2023; v1 submitted 1 July, 2022; originally announced July 2022.

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 4 (November 3, 2023) lmcs:9781

$ω$-Forest Algebras and Temporal Logics

Authors: Achim Blumensath, Jakub Lédl

Abstract: We use the algebraic framework for languages of infinite trees introduced in [4] to derive effective characterisations of various temporal logics, in particular the logic EF (a fragment of CTL) and its counting variant cEF. We use the algebraic framework for languages of infinite trees introduced in [4] to derive effective characterisations of various temporal logics, in particular the logic EF (a fragment of CTL) and its counting variant cEF. △ Less

Submitted 25 March, 2022; originally announced March 2022.

Algebraic Language Theory for Eilenberg--Moore Algebras

Authors: Achim Blumensath

Abstract: We develop an algebraic language theory based on the notion of an Eilenberg--Moore algebra. In comparison to previous such frameworks the main contribution is the support for algebras with infinitely many sorts and the connection to logic in form of so-called `definable algebras'. We develop an algebraic language theory based on the notion of an Eilenberg--Moore algebra. In comparison to previous such frameworks the main contribution is the support for algebras with infinitely many sorts and the connection to logic in form of so-called `definable algebras'. △ Less

Submitted 13 April, 2021; v1 submitted 15 June, 2020; originally announced June 2020.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 2 (April 14, 2021) lmcs:6569

Bisimulation Invariant Monadic-Second Order Logic in the Finite

Authors: Achim Blumensath, Felix Wolf

Abstract: We consider bisimulation-invariant monadic second-order logic over various classes of finite transition systems. We present several combinatorial characterisations of when the expressive power of this fragment coincides with that of the modal mu-calculus. Using these characterisations we prove for some simple classes of transition systems that this is indeed the case. In particular, we show that,… ▽ More We consider bisimulation-invariant monadic second-order logic over various classes of finite transition systems. We present several combinatorial characterisations of when the expressive power of this fragment coincides with that of the modal mu-calculus. Using these characterisations we prove for some simple classes of transition systems that this is indeed the case. In particular, we show that, over the class of all finite transition systems with Cantor-Bendixson rank at most k, bisimulation-invariant MSO coincides with L_mu. △ Less

Submitted 16 May, 2019; originally announced May 2019.

Regular Tree Algebras

Authors: Achim Blumensath

Abstract: We introduce a class of algebras that can be used as recognisers for regular tree languages. We show that it is the only such class that forms a pseudo-variety and we prove the existence of syntactic algebras. Finally, we give a more algebraic characterisation of the algebras in our class. We introduce a class of algebras that can be used as recognisers for regular tree languages. We show that it is the only such class that forms a pseudo-variety and we prove the existence of syntactic algebras. Finally, we give a more algebraic characterisation of the algebras in our class. △ Less

Submitted 12 February, 2020; v1 submitted 10 August, 2018; originally announced August 2018.

Journal ref: Logical Methods in Computer Science, Volume 16, Issue 1 (February 13, 2020) lmcs:4747

Branch-Continuous Tree Algebras

Authors: Achim Blumensath

Abstract: We study a class of algebras that can be used as recognisers for regular languages of infinite trees. We study a class of algebras that can be used as recognisers for regular languages of infinite trees. △ Less

Submitted 12 July, 2018; originally announced July 2018.

A Compositional Coalgebraic Semantics of Strategic Games

Authors: Achim Blumensath, Viktor Winschel

Abstract: We provide a compositional coalgebraic semantics for strategic games. In our framework, like in the semantics of functional programming languages, coalgebras represent the observable behaviour of systems derived from the behaviour of the parts over an unobservable state space. We use coalgebras to describe and program stage games, finitely and potentially infinitely repeated hierarchical or parall… ▽ More We provide a compositional coalgebraic semantics for strategic games. In our framework, like in the semantics of functional programming languages, coalgebras represent the observable behaviour of systems derived from the behaviour of the parts over an unobservable state space. We use coalgebras to describe and program stage games, finitely and potentially infinitely repeated hierarchical or parallel games with imperfect and incomplete information based on deterministic, non-deterministic or probabilistic decisions of learning agents in possibly endogenous networks. Our framework is compositional in that arbitrarily complex network of games can be composed. The coalgebraic approach allows to represent self-referential or reflexive structures like institutional dynamics, strategic network formation from within the network, belief formation, learning agents or other self-referential phenomena that characterise complex social systems of cognitive agents. And finally our games represent directly runnable code in functional programming languages that can also be analysed by sophisticated verification and logical tools of software engineering. △ Less

Submitted 22 December, 2017; originally announced December 2017.

Decidability Results for the Boundedness Problem

Authors: Achim Blumensath, Martin Otto, Mark Weyer

Abstract: We prove decidability of the boundedness problem for monadic least fixed-point recursion based on positive monadic second-order (MSO) formulae over trees. Given an MSO-formula phi(X,x) that is positive in X, it is decidable whether the fixed-point recursion based on phi is spurious over the class of all trees in the sense that there is some uniform finite bound for the number of iterations phi ta… ▽ More We prove decidability of the boundedness problem for monadic least fixed-point recursion based on positive monadic second-order (MSO) formulae over trees. Given an MSO-formula phi(X,x) that is positive in X, it is decidable whether the fixed-point recursion based on phi is spurious over the class of all trees in the sense that there is some uniform finite bound for the number of iterations phi takes to reach its least fixed point, uniformly across all trees. We also identify the exact complexity of this problem. The proof uses automata-theoretic techniques. This key result extends, by means of model-theoretic interpretations, to show decidability of the boundedness problem for MSO and guarded second-order logic (GSO) over the classes of structures of fixed finite tree-width. Further model-theoretic transfer arguments allow us to derive major known decidability results for boundedness for fragments of first-order logic as well as new ones. △ Less

Submitted 13 August, 2014; v1 submitted 30 June, 2014; originally announced June 2014.

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 3 (August 15, 2014) lmcs:1225

Monadic second-order definable graph orderings

Authors: Achim Blumensath, Bruno Courcelle

Abstract: We study the question of whether, for a given class of finite graphs, one can define, for each graph of the class, a linear ordering in monadic second-order logic, possibly with the help of monadic parameters. We consider two variants of monadic second-order logic: one where we can only quantify over sets of vertices and one where we can also quantify over sets of edges. For several special cases… ▽ More We study the question of whether, for a given class of finite graphs, one can define, for each graph of the class, a linear ordering in monadic second-order logic, possibly with the help of monadic parameters. We consider two variants of monadic second-order logic: one where we can only quantify over sets of vertices and one where we can also quantify over sets of edges. For several special cases, we present combinatorial characterisations of when such a linear ordering is definable. In some cases, for instance for graph classes that omit a fixed graph as a minor, the presented conditions are necessary and sufficient; in other cases, they are only necessary. Other graph classes we consider include complete bipartite graphs, split graphs, chordal graphs, and cographs. We prove that orderability is decidable for the so called HR-equational classes of graphs, which are described by equation systems and generalize the context-free languages. △ Less

Submitted 20 January, 2014; v1 submitted 30 October, 2013; originally announced October 2013.

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 1 (January 21, 2014) lmcs:793

On the Monadic Second-Order Transduction Hierarchy

Authors: Achim Blumensath, Bruno Courcelle

Abstract: We compare classes of finite relational structures via monadic second-order transductions. More precisely, we study the preorder where we set C \subseteq K if, and only if, there exists a transduction τ such that C\subseteqτ(K). If we only consider classes of incidence structures we can completely describe the resulting hierarchy. It is linear of order type ω+3. Each level can be characterised in… ▽ More We compare classes of finite relational structures via monadic second-order transductions. More precisely, we study the preorder where we set C \subseteq K if, and only if, there exists a transduction τ such that C\subseteqτ(K). If we only consider classes of incidence structures we can completely describe the resulting hierarchy. It is linear of order type ω+3. Each level can be characterised in terms of a suitable variant of tree-width. Canonical representatives of the various levels are: the class of all trees of height n, for each n \in N, of all paths, of all trees, and of all grids. △ Less

Submitted 22 June, 2010; v1 submitted 27 April, 2010; originally announced April 2010.

ACM Class: G.2.2; F.4.1

Journal ref: Logical Methods in Computer Science, Volume 6, Issue 2 (June 22, 2010) lmcs:1208

Guarded Second-Order Logic, Spanning Trees, and Network Flows

Authors: Achim Blumensath

Abstract: According to a theorem of Courcelle monadic second-order logic and guarded second-order logic (where one can also quantify over sets of edges) have the same expressive power over the class of all countable $k$-sparse hypergraphs. In the first part of the present paper we extend this result to hypergraphs of arbitrary cardinality. In the second part, we present a generalisation dealing with metho… ▽ More According to a theorem of Courcelle monadic second-order logic and guarded second-order logic (where one can also quantify over sets of edges) have the same expressive power over the class of all countable $k$-sparse hypergraphs. In the first part of the present paper we extend this result to hypergraphs of arbitrary cardinality. In the second part, we present a generalisation dealing with methods to encode sets of vertices by single vertices. △ Less

Submitted 16 February, 2010; v1 submitted 16 October, 2009; originally announced October 2009.

ACM Class: G.2.2; F.4.1

Journal ref: Logical Methods in Computer Science, Volume 6, Issue 1 (February 16, 2010) lmcs:1207