Author name cluster

Amaldev Manuel

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.

6 papers

2 author rows

Highlights Conference 2021 Conference Abstract

An Algebraic Characterisation of First-Order Logic with Neighbour

Amaldev Manuel

We give an algebraic characterisation of first-order logic with the neighbour relation, on finite words. For this, we consider languages of finite words over alphabets with an involution on them. The natural algebras for such languages are involution semigroups. To characterise the logic, we define a special kind of semidirect product of involution semigroups, called the locally hermitian product. The characterisation theorem for FO with neighbour states that a language is definable in the logic if and only if it is recognised by a locally hermitian product of an aperiodic commutative involution semigroup, and a locally trivial involution semigroup. We then define the notion of involution varieties of languages, namely classes of languages closed under Boolean operations, quotients, involution, and inverse images of involutory morphisms. An Eilenberg-type correspondence is established between involution varieties of languages and pseudovarieties of involution semigroups. The results are to be presented in LICS ’21.

Details

MFCS Conference 2016 Conference Paper

Two-Variable Logic over Countable Linear Orderings

Amaldev Manuel
A. V. Sreejith

We study the class of languages of finitely-labelled countable linear orderings definable in two-variable first-order logic. We give a number of characterisations, in particular an algebraic one in terms of circle monoids, using equations. This generalises the corresponding characterisation, namely variety DA, over finite words to the countable case. A corollary is that the membership in this class is decidable: for instance given an MSO formula it is possible to check if there is an equivalent two-variable logic formula over countable linear orderings. In addition, we prove that the satisfiability problems for two-variable logic over arbitrary, countable, and scattered linear orderings are NEXPTIME-complete.

Details

Highlights Conference 2014 Conference Abstract

Expressiveness of Min-Max Automata

Amaldev Manuel

A min-max automaton is a finite state automaton with a finite number of registers storing non-negative integer values that are updated by expressions consisting of register names and operations min, max and +1. We discuss the expressiveness results concerning these automata. This is a joint work with Thomas Colcombet and Stefan Göller.

PDF Details

CSL Conference 2013 Conference Paper

Two-Variable Logic on 2-Dimensional Structures

Amaldev Manuel
Thomas Zeume

This paper continues the study of the two-variable fragment of first-order logic (FO^2) over two- dimensional structures, more precisely structures with two orders, their induced successor relations and arbitrarily many unary relations. Our main focus is on ordered data words which are finite sequences from the set \Sigma x D where \Sigma is a finite alphabet and D is an ordered domain. These are naturally represented as labelled finite sets with a linear order <=_l and a total preorder <=_p. We introduce ordered data automata, an automaton model for ordered data words. An ordered data automaton is a composition of a finite state transducer and a finite state automaton over the product Boolean algebra of finite and cofinite subsets of N. We show that ordered data automata are equivalent to the closure of FO^2(+1_l, <=_p, +1_p) under existential quantification of unary relations. Using this automaton model we prove that the finite satisfiability problem for this logic is decidable on structures where the <=_p-equivalence classes are of bounded size. As a corollary, we obtain that finite satisfiability of FO^2 is decidable (and it is equivalent to the reachability problem of vector addition systems) on structures with two linear order successors and a linear order corresponding to one of the successors. Further we prove undecidability of FO^2 on several other two-dimensional structures.

Details

Highlights Conference 2013 Conference Abstract

μ-calculus on data words

Thomas Colcombet
Amaldev Manuel

We introduce and explore various fragments of μ-calculus on data words. We show that full μ-calculus is undecidable, but its ν-fragment is decidable by reduction to data automata. We disclose two subclasses of the ν-fragment that enjoy the further property of being closed under negation, namely the class of Bounded Reversal (BR) and the class of Bounded Mode Alternation (BMA). The latter is contained in the former class and is already sufficiently expressive for capturing several logics studied in the literature like $\fotwo$ and Data-LTL. We then characterize these two fragments as cascades of suitably defined transducer models. We finally prove the separation of BMA from BR using a novel paradigm of circuits and prove hierarchy theorems for BMA, Data-LTL and $\fotwo$.

PDF Details

MFCS Conference 2010 Conference Paper

Two Variables and Two Successors

Amaldev Manuel

Abstract We look at the finite satisfiability problem of the two variable fragment of first order logic with the successors of two linear orders. While the logic with both the successors and their transitive closures remains undecidable, we prove that the logic with only the successors is decidable.

Details