Showing 1–11 of 11 results for author: Kartzow, A

Model Checking Constraint LTL over Trees

Authors: Alexander Kartzow, Thomas Weidner

Abstract: Constraint automata are an adaptation of Büchi-automata that process data words where the data comes from some relational structure S. Every transition of such an automaton comes with constraints in terms of the relations of S. A transition can only be fired if the current and the next data values satisfy all constraints of this transition. These automata have been used in the setting where S is a… ▽ More Constraint automata are an adaptation of Büchi-automata that process data words where the data comes from some relational structure S. Every transition of such an automaton comes with constraints in terms of the relations of S. A transition can only be fired if the current and the next data values satisfy all constraints of this transition. These automata have been used in the setting where S is a linear order for deciding constraint LTL with constraints over S. In this paper, S is the infinitely branching infinite order tree T. We provide a PSPACE algorithm for emptiness of T-constraint automata. This result implies PSPACE-completeness of the satisfiability and the model checking problem for constraint LTL with constraints over T. △ Less

Submitted 23 April, 2015; originally announced April 2015.

Satisfiability of ECTL* with tree constraints

Authors: Claudia Carapelle, Shiguang Feng, Alexander Kartzow, Markus Lohrey

Abstract: Recently, we have shown that satisfiability for $\mathsf{ECTL}^*$ with constraints over $\mathbb{Z}$ is decidable using a new technique. This approach reduces the satisfiability problem of $\mathsf{ECTL}^*$ with constraints over some structure A (or class of structures) to the problem whether A has a certain model theoretic property that we called EHD (for "existence of homomorphisms is decidable"… ▽ More Recently, we have shown that satisfiability for $\mathsf{ECTL}^*$ with constraints over $\mathbb{Z}$ is decidable using a new technique. This approach reduces the satisfiability problem of $\mathsf{ECTL}^*$ with constraints over some structure A (or class of structures) to the problem whether A has a certain model theoretic property that we called EHD (for "existence of homomorphisms is decidable"). Here we apply this approach to concrete domains that are tree-like and obtain several results. We show that satisfiability of $\mathsf{ECTL}^*$ with constraints is decidable over (i) semi-linear orders (i.e., tree-like structures where branches form arbitrary linear orders), (ii) ordinal trees (semi-linear orders where the branches form ordinals), and (iii) infinitely branching trees of height h for each fixed $h\in \mathbb{N}$. We prove that all these classes of structures have the property EHD. In contrast, we introduce Ehrenfeucht-Fraisse-games for $\mathsf{WMSO}+\mathsf{B}$ (weak $\mathsf{MSO}$ with the bounding quantifier) and use them to show that the infinite (order) tree does not have property EHD. As a consequence, a different approach has to be taken in order to settle the question whether satisfiability of $\mathsf{ECTL}^*$ (or even $\mathsf{LTL}$) with constraints over the infinite (order) tree is decidable. △ Less

Submitted 24 February, 2015; v1 submitted 9 December, 2014; originally announced December 2014.

The field of the Reals and the Random Graph are not Finite-Word Ordinal-Automatic

Authors: Alexander Kartzow

Abstract: Recently, Schlicht and Stephan lifted the notion of automatic-structures to the notion of (finite-word) ordinal-automatic structures. These are structures whose domain and relations can be represented by automata reading finite words whose shape is some fixed ordinal $α$. We lift Delhommé's relative-growth-technique from the automatic and tree-automatic setting to the ordinal-automatic setting. Th… ▽ More Recently, Schlicht and Stephan lifted the notion of automatic-structures to the notion of (finite-word) ordinal-automatic structures. These are structures whose domain and relations can be represented by automata reading finite words whose shape is some fixed ordinal $α$. We lift Delhommé's relative-growth-technique from the automatic and tree-automatic setting to the ordinal-automatic setting. This result implies that the random graph is not ordinal-automatic and infinite integral domains are not ordinal-automatic with respect to ordinals below $ω_1+ω^ω$ where $ω_1$ is the first uncountable ordinal. △ Less

Submitted 20 October, 2014; originally announced October 2014.

Reachability in Higher-Order-Counters

Authors: Alexander Heußner, Alexander Kartzow

Abstract: Higher-order counter automata (\HOCS) can be either seen as a restriction of higher-order pushdown automata (\HOPS) to a unary stack alphabet, or as an extension of counter automata to higher levels. We distinguish two principal kinds of \HOCS: those that can test whether the topmost counter value is zero and those which cannot. We show that control-state reachability for level $k$ \HOCS with… ▽ More Higher-order counter automata (\HOCS) can be either seen as a restriction of higher-order pushdown automata (\HOPS) to a unary stack alphabet, or as an extension of counter automata to higher levels. We distinguish two principal kinds of \HOCS: those that can test whether the topmost counter value is zero and those which cannot. We show that control-state reachability for level $k$ \HOCS with $0$-test is complete for \mbox{$(k-2)$}-fold exponential space; leaving out the $0$-test leads to completeness for \mbox{$(k-2)$}-fold exponential time. Restricting \HOCS (without $0$-test) to level $2$, we prove that global (forward or backward) reachability analysis is $\PTIME$-complete. This enhances the known result for pushdown systems which are subsumed by level $2$ \HOCS without $0$-test. We transfer our results to the formal language setting. Assuming that $\PTIME \subsetneq \PSPACE \subsetneq \mathbf{EXPTIME}$, we apply proof ideas of Engelfriet and conclude that the hierarchies of languages of \HOPS and of \HOCS form strictly interleaving hierarchies. Interestingly, Engelfriet's constructions also allow to conclude immediately that the hierarchy of collapsible pushdown languages is strict level-by-level due to the existing complexity results for reachability on collapsible pushdown graphs. This answers an open question independently asked by Parys and by Kobayashi. △ Less

Submitted 5 June, 2013; originally announced June 2013.

Comments: Version with Full Proofs of a paper that appears at MFCS 2013

Satisfiability of CTL* with constraints

Authors: Claudia Carapelle, Alexander Kartzow, Markus Lohrey

Abstract: We show that satisfiability for CTL* with equality-, order-, and modulo-constraints over Z is decidable. Previously, decidability was only known for certain fragments of CTL*, e.g., the existential and positive fragments and EF. We show that satisfiability for CTL* with equality-, order-, and modulo-constraints over Z is decidable. Previously, decidability was only known for certain fragments of CTL*, e.g., the existential and positive fragments and EF. △ Less

Submitted 4 June, 2013; originally announced June 2013.

Comments: To appear at Concur 2013

Structures Without Scattered-Automatic Presentation

Authors: Alexander Kartzow, Philipp Schlicht

Abstract: Bruyere and Carton lifted the notion of finite automata reading infinite words to finite automata reading words with shape an arbitrary linear order L. Automata on finite words can be used to represent infinite structures, the so-called word-automatic structures. Analogously, for a linear order L there is the class of L-automatic structures. In this paper we prove the following limitations on the… ▽ More Bruyere and Carton lifted the notion of finite automata reading infinite words to finite automata reading words with shape an arbitrary linear order L. Automata on finite words can be used to represent infinite structures, the so-called word-automatic structures. Analogously, for a linear order L there is the class of L-automatic structures. In this paper we prove the following limitations on the class of L-automatic structures for a fixed L of finite condensation rank 1+α. Firstly, no scattered linear order with finite condensation rank above ω^(α+1) is L-α-automatic. In particular, every L-automatic ordinal is below ω^ω^(α+1). Secondly, we provide bounds on the (ordinal) height of well-founded order trees that are L-automatic. If αis finite or L is an ordinal, the height of such a tree is bounded by ω^{α+1}. Finally, we separate the class of tree-automatic structures from that of L-automatic structures for any ordinal L: the countable atomless boolean algebra is known to be tree-automatic, but we show that it is not L-automatic. △ Less

Submitted 3 April, 2013; originally announced April 2013.

Comments: 10 pages + 20 pages Appendix; accepted for CiE 2013

Collapsible Pushdown Graphs of Level 2 are Tree-Automatic

Authors: Alexander Kartzow

Abstract: We show that graphs generated by collapsible pushdown systems of level 2 are tree-automatic. Even if we allow epsilon-contractions and reachability predicates (with regular constraints) for pairs of configurations, the structures remain tree-automatic whence their first-order logic theories are decidable. As a corollary we obtain the tree-automaticity of the second level of the Caucal-hierarchy. We show that graphs generated by collapsible pushdown systems of level 2 are tree-automatic. Even if we allow epsilon-contractions and reachability predicates (with regular constraints) for pairs of configurations, the structures remain tree-automatic whence their first-order logic theories are decidable. As a corollary we obtain the tree-automaticity of the second level of the Caucal-hierarchy. △ Less

Submitted 18 March, 2013; v1 submitted 11 March, 2013; originally announced March 2013.

Comments: Journal version of arXiv:0912.4110, accepted for publication in LMCS

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 1 (March 20, 2013) lmcs:1220

First-Order Logic on Higher-Order Nested Pushdown Trees

Authors: Alexander Kartzow

Abstract: We introduce a new hierarchy of higher-order nested pushdown trees generalising Alur et al.'s concept of nested pushdown trees. Nested pushdown trees are useful representations of control flows in the verification of programs with recursive calls of first-order functions. Higher-order nested pushdown trees are expansions of unfoldings of graphs generated by higher-order pushdown systems. Moreover,… ▽ More We introduce a new hierarchy of higher-order nested pushdown trees generalising Alur et al.'s concept of nested pushdown trees. Nested pushdown trees are useful representations of control flows in the verification of programs with recursive calls of first-order functions. Higher-order nested pushdown trees are expansions of unfoldings of graphs generated by higher-order pushdown systems. Moreover, the class of nested pushdown trees of level n is uniformly first-order interpretable in the class of collapsible pushdown graphs of level n+1. The relationship between the class of higher-order pushdown graphs and the class of collapsible higher-order pushdown graphs is not very well understood. We hope that the further study of the nested pushdown tree hierarchy leads to a better understanding of these two hierarchies. In this paper, we are concerned with the first-order model checking problem on higher-order nested pushdown trees. We show that the first-order model checking on the first two levels of this hierarchy is decidable. Moreover, we obtain an 2-EXPSPACE algorithm for the class of nested pushdown trees of level 1. The proof technique involves a pseudo-local analysis of strategies in the Ehrenfeucht-Fraisse games on two identical copies of a nested pushdown tree. Ordinary locality arguments in the spirit of Gaifman's lemma do not apply here because nested pushdown trees tend to have small diameters. We introduce the notion of relevant ancestors which provide a sufficient description of the FO_k -type of each element in a higher-order nested pushdown tree. The local analysis of these ancestors allows us to prove the existence of restricted winning strategies in the Ehrenfeucht-Fraisse game. These strategies are then used to create a first-order model checking algorithm. △ Less

Submitted 9 February, 2012; originally announced February 2012.

Comments: 41 pages

First-Order Model Checking on Generalisations of Pushdown Graphs

Authors: Alexander Kartzow

Abstract: We study the first-order model checking problem on two generalisations of pushdown graphs. The first class is the class of nested pushdown trees. The other is the class of collapsible pushdown graphs. Our main results are the following. First-order logic with reachability is uniformly decidable on nested pushdown trees. Considering first-order logic without reachability, we prove decidability in d… ▽ More We study the first-order model checking problem on two generalisations of pushdown graphs. The first class is the class of nested pushdown trees. The other is the class of collapsible pushdown graphs. Our main results are the following. First-order logic with reachability is uniformly decidable on nested pushdown trees. Considering first-order logic without reachability, we prove decidability in doubly exponential alternating time with linearly many alternations. First-order logic with regular reachability predicates is uniformly decidable on level 2 collapsible pushdown graphs. Moreover, nested pushdown trees are first-order interpretable in collapsible pushdown graphs of level 2. This interpretation can be extended to an interpretation of the class of higher-order nested pushdown trees in the collapsible pushdown graph hierarchy. We prove that the second level of this new hierarchy of nested trees has decidable first-order model checking. Our decidability result for collapsible pushdown graph relies on the fact that level 2 collapsible pushdown graphs are uniform tree-automatic. Our last result concerns tree-automatic structures in general. We prove that first-order logic extended by Ramsey quantifiers is decidable on all tree-automatic structures. △ Less

Submitted 1 February, 2012; originally announced February 2012.

Comments: phd thesis, 255 pages

Tree-Automatic Well-Founded Trees

Authors: Martin Huschenbett, Alexander Kartzow, Jiamou Liu, Markus Lohrey

Abstract: We investigate tree-automatic well-founded trees. Using Delhomme's decomposition technique for tree-automatic structures, we show that the (ordinal) rank of a tree-automatic well-founded tree is strictly below omega^omega. Moreover, we make a step towards proving that the ranks of tree-automatic well-founded partial orders are bounded by omega^omega^omega: we prove this bound for what we call upw… ▽ More We investigate tree-automatic well-founded trees. Using Delhomme's decomposition technique for tree-automatic structures, we show that the (ordinal) rank of a tree-automatic well-founded tree is strictly below omega^omega. Moreover, we make a step towards proving that the ranks of tree-automatic well-founded partial orders are bounded by omega^omega^omega: we prove this bound for what we call upwards linear partial orders. As an application of our result, we show that the isomorphism problem for tree-automatic well-founded trees is complete for level Delta^0_{omega^omega} of the hyperarithmetical hierarchy with respect to Turing-reductions. △ Less

Submitted 24 June, 2013; v1 submitted 26 January, 2012; originally announced January 2012.

Comments: Will appear in Logical Methods of Computer Science

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 2 (June 25, 2013) lmcs:721

Strictness of the Collapsible Pushdown Hierarchy

Authors: Alexander Kartzow, Paweł Parys

Abstract: We present a pum** lemma for each level of the collapsible pushdown graph hierarchy in analogy to the second author's pum** lemma for higher-order pushdown graphs (without collapse). Using this lemma, we give the first known examples that separate the levels of the collapsible pushdown graph hierarchy and of the collapsible pushdown tree hierarchy, i.e., the hierarchy of trees generated by hig… ▽ More We present a pum** lemma for each level of the collapsible pushdown graph hierarchy in analogy to the second author's pum** lemma for higher-order pushdown graphs (without collapse). Using this lemma, we give the first known examples that separate the levels of the collapsible pushdown graph hierarchy and of the collapsible pushdown tree hierarchy, i.e., the hierarchy of trees generated by higher-order recursion schemes. This confirms the open conjecture that higher orders allow one to generate more graphs and more trees. △ Less

Submitted 14 June, 2012; v1 submitted 16 January, 2012; originally announced January 2012.

Comments: 68 pages, short version in MFCS 2012