Projection for Büchi Tree Automata with Constraints between Siblings

2020 ◽  
Vol 31 (06) ◽  
pp. 749-775
Author(s):  
Patrick Landwehr ◽  
Christof Löding
Keyword(s):  
Decision Procedure ◽  
Order Logic ◽  
Tree Automata ◽  
Boolean Operations ◽  
Regular Tree ◽  
Infinite Trees ◽  
Acceptance Condition ◽  
Emptiness Problem ◽  
Second Order Logic ◽  
Monadic Second Order Logic

We consider an extension of tree automata on infinite trees that can use equality and disequality constraints between direct subtrees of a node. Recently, it has been shown that the emptiness problem for these kind of automata with a parity acceptance condition is decidable and that the corresponding class of languages is closed under Boolean operations. In this paper, we show that the class of languages recognizable by such tree automata with a Büchi acceptance condition is closed under projection. This construction yields a new algorithm for the emptiness problem, implies that a regular tree is accepted if the language is non-empty (for the Büchi condition), and can be used to obtain a decision procedure for an extension of monadic second-order logic with predicates for subtree comparisons.

scholarly journals Monoidal-closed categories of tree automata

2020 ◽  
Vol 30 (1) ◽  
pp. 62-117
Author(s):  
Colin Riba
Keyword(s):  
Linear Logic ◽  
Tree Automata ◽  
Sequential Games ◽  
Infinite Trees ◽  
Alternating Tree Automata ◽  
Deduction Rules ◽  
New Perspective ◽  
Alternating Automata ◽  
Second Order Logic ◽  
Monadic Second Order Logic

AbstractThis paper surveys a new perspective on tree automata and Monadic second-order logic (MSO) on infinite trees. We show that the operations on tree automata used in the translations of MSO-formulae to automata underlying Rabin’s Tree Theorem (the decidability of MSO) correspond to the connectives of Intuitionistic Multiplicative Exponential Linear Logic (IMELL). Namely, we equip a variant of usual alternating tree automata (that we call uniform tree automata) with a fibered monoidal-closed structure which in particular handles a linear complementation of alternating automata. Moreover, this monoidal structure is actually Cartesian on non-deterministic automata, and an adaptation of a usual construction for the simulation of alternating automata by non-deterministic ones satisfies the deduction rules of the !(–) exponential modality of IMELL. (But this operation is unfortunately not a functor because it does not preserve composition.) Our model of IMLL consists in categories of games which are based on usual categories of two-player linear sequential games called simple games, and which generalize usual acceptance games of tree automata. This model provides a realizability semantics, along the lines of Curry–Howard proofs-as-programs correspondence, of a linear constructive deduction system for tree automata. This realizability semantics, which can be summarized with the slogan “automata as objects, strategies as morphisms,” satisfies an expected property of witness extraction from proofs of existential statements. Moreover, it makes it possible to combine realizers produced as interpretations of proofs with strategies witnessing (non-)emptiness of tree automata.

Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski

2000 ◽  
Vol 65 (1) ◽  
pp. 310-332 ◽  
Author(s):  
Giovanna D'agostino ◽  
Marco Hollenberg
Keyword(s):  
Decision Procedure ◽  
Sequent Calculus ◽  
Theoretical Perspective ◽  
Order Logic ◽  
Rite Of Passage ◽  
Finite Model ◽  
Finite Model Property ◽  
Exponential Time ◽  
Second Order Logic ◽  
Monadic Second Order Logic

The (modal) μ-calculus ([14]) is a very powerful extension of modal logic with least and greatest fixed point operators. It is of great interest to computer science for expressing properties of processes such as termination (every run is finite) and fairness (on every infinite run, no action is repeated infinitely often to the exclusion of all others).The power of the μ-calculus is also evident from a more theoretical perspective. The μ-calculus is a fragment of monadic second-order logic (MSO) containing only formulae that are invariant for bisimulation, in the sense that they cannot distinguish between bisimilar states. Janin and Walukiewicz prove the converse: any property which is invariant for bisimulation and MSO-expressible is already expressible in the μ-calculus ([13]). Yet the μ-calculus enjoys many desirable properties which MSO lacks, like a complete sequent-calculus ([29]), an exponential-time decision procedure, and the finite model property ([25]). Switching from MSO to its bisimulation-invariant fragment gives us these desirable properties.In this paper we take a classical logician's view of the μ-calculus. As far as we are concerned a new logic should not be allowed into the community of logics without at least considering the standard questions that any logic is bothered with. In this paper we perform this rite of passage for the μ-calculus. The questions we will be concerned with are the following.

scholarly journals Choice functions and well-orderings over the infinite binary tree

2010 ◽  
Vol 8 (4) ◽  
Author(s):  
Arnaud Carayol ◽  
Christof Löding ◽  
Damian Niwinski ◽  
Igor Walukiewicz
Keyword(s):  
Binary Tree ◽  
Choice Function ◽  
Second Order ◽  
Order Logic ◽  
Automata Theory ◽  
Choice Functions ◽  
Infinite Trees ◽  
Second Order Logic ◽  
Inherent Ambiguity ◽  
Monadic Second Order Logic

AbstractWe give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We show how the result can be used to prove the inherent ambiguity of languages of infinite trees. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded order on the infinite binary tree by showing that every infinite binary tree with a well-founded order has an undecidable MSO-theory.

The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic

2021 ◽  
Vol 178 (1-2) ◽  
pp. 1-30
Author(s):  
Florian Bruse ◽  
Martin Lange ◽  
Etienne Lozes
Keyword(s):  
Model Checking ◽  
Lower Bounds ◽  
Expressive Power ◽  
Higher Order ◽  
Order Logic ◽  
High Complexity ◽  
Transition Systems ◽  
Recursive Formulas ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ-calculus into the modal μ-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most k < 0. In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in (k − 1)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.

Sign in / Sign up

Export Citation Format

Share Document