About Me
After my BTech in Computer Science
from
College of engineering,
Thiruvananthapuram (CET), I joined
for a masters program (Mtech) in Computer science from
IIT, Madras. I further pursued my interest in logic and automata theory during my PhD in
Institute of
Mathematical Sciences, Chennai under
Prof. Kamal Lodaya. After
I finished my PhD in 2013, I immediately joined for a postdoc in
Tata Institute of Fundamental Research
(TIFR), Mumbai, followed by postdocs in
Laboratoire d'Informatique Algorithmique: Fondements et Applications
(LIAFA), Paris with
Prof.
Thomas Colcombet and
Chennai Mathematical Institute (CMI). Currently I am working with
Mikołaj Bojańczyk in
University of Warsaw.
Awards: ACM
India Honourable Mention for dissertation titled "Regular
Quantifiers
in Logic"
PhD Thesis: Regular
quantifiers in Logic
Publications
Two-variable logic over
countable linear orderings, with Amaldev
Manuel,
MFCS 2016.
(
pdf,
full,
abstract)
Abstract :
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.
Limited Set quantifiers
over
Countable Linear Orderings, with
Thomas
Colcombet,
ICALP 2015.
(
pdf,
full,
abstract)
Abstract :
In
this paper, we study several sublogics of monadic second-order logic
over countable linear orderings, such as first-order logic, first-order
logic on cuts, weak monadic second-order logic, weak monadic
second-order logic with cuts, as well as fragments of monadic
second-order logic in which sets have to be well ordered or scattered.
We give decidable algebraic characterizations of all these logics and
compare their respective expressive power.
Counting quantifiers
and
linear arithmetic on word models, with
Kamal Lodaya,
Asian
Logic Conference (ALC), 2014.
(
pdf)
On lower bounds for
multiplicative circuits and linear circuits in
noncommutative domains, with
V
Arvind and
S Raja,
Computer
Science Symposium in Russia (CSR), 2014.
(
pdf,
abstract)
Abstract :
In
this paper we show some lower bounds for the size of multiplicative
circuits computing multi-output functions in some noncommutative
domains like monoids and finite groups. We also introduce and study a
generalization of linear circuits in which the goal is to compute MY
where Y is a vector of indeterminates and M is a matrix
whose
entries come from noncommutative rings. We show some lower
bounds in this setting as well.
Non-definability of
Languages by Generalized First-order Formulas
over (N, +), with
Andreas
Krebs,
LICS 2012.
(
pdf,
full,
abstract)
Abstract :
We
consider first-order logic with monoidal quantifiers. We show that all
languages with a neutral letter, definable using the addition numerical
predicate are also definable with the order predicate as the only
numerical predicate. Since we prove this result for arbitrary subsets
of the monoidal quantifiers, the following holds in the presence of a
neutral letter: For aperiodic monoids, we get the result of Libkin that
FO[<, +] collapses to FO[<]; For solvable monoids, we get the
result of Roy and Straubing that FO+MOD[<, +] collapses to
FO+MOD[<]; For cyclic groups, we answer an open question of Roy and
Straubing, proving that MOD[<, +] collapses to MOD[<].
All these results can be viewed as collapse results for the uniformity
of constant depth circuits, and in this sense as a separation result
for very uniform circuit classes. For example we separate
FO[<,+]-uniform CC^0 from FO[<,+]-uniform ACC^0.
Expressive Completeness
for
LTL With Modulo Counting and Group
Quantifiers,
Electronic
Notes in Theoretical Computer Science
(ENTCS),
2011.
(
pdf,
abstract)
Abstract :
Kamp
showed that linear temporal logic is expressively complete for
first order logic over words. We give a Gabbay style proof to show
that linear temporal logic extended with modulo counting and group
quantifiers (introduced by Baziramwabo,McKenzie,Th\'erien) is
expressively complete for first order logic with modulo counting
(introduced by Straubing, Th\'erien, Thomas) and
group quantifiers (introduced by Barrington, Immerman,
Straubing).
LTL can be more succinct,
with
Kamal Lodaya,
Automated
Technology for Verification
and Analysis (ATVA), 2010.
(
pdf,
abstract)
Abstract :
It
is well known that modelchecking and satisfiability of Linear Temporal
Logic (LTL) are Pspace-complete. Wolper showed that
with grammar operators, this result can be extended to increase the
expressiveness of the logic to all regular languages. Other ways of
extending the expressiveness of LTL using modular and group modalities
have been explored by Baziramwabo, McKenzie and Th\'erien, which are
expressively complete for regular languages recognized by solvable
monoids and for all regular languages, respectively. In all the papers
mentioned, the numeric constants used in the modalities are in unary
notation. We show that in some cases (such as the modular and symmetric
group modalities) we can use numeric constants in binary notation,
and still maintain the Pspace upper bound. Adding modulo counting to
LTL[F] (with just the unary future modality) already makes the logic
Pspace-hard. We also consider a restricted logic which allows only
the modulo counting of length from the beginning of the word. Its
satisfiability is Sigmathree-complete.
Teaching
One week course on
Descriptive Complexity theory: An
introduction, Indian School on Logic and its
Applications
(ISLA), PSG college of Technology, Coimbatore in March 2016
An one semester course titled
Verification
for graduate and undergraduate students in Wilhelm-Schickard-Institut
für Informatik, University of Tübingen, Germany, from March 2012 to
August 2012
Abstract :
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.
Interesting Links
Computer science
bibliography collections
Computer science conference timelines
Erdos Number
![[photograph]](images/sav.jpg)