Abhisekh Sankaran
Tata Consultancy Services (TCS) Research, Pune, India
Email: firstname.lastname [at] tcs.com
About me
I am a Consultant at Tata Research Development and Design Centre (TRDDC), the branch of TCS Research in Pune. Prior to joining TRDDC, I was a postdoctoral research associate at the Department of Computer Science and Technology at the University of Cambridge, working with Anuj Dawar in the project "Logical Fractals" funded by the Leverhulme Trust. Before Cambridge, I was a postdoctoral fellow in the Theoretical Computer Science Wing at the Institute of Mathematical Sciences, Chennai working with R. Ramanujam. I completed my Ph.D., and also my Bachelors and Masters, from the Department of Computer Science and Engineering at IIT Bombay. My dissertation, titled "A generalization of the ŁośTarski preservation theorem", was completed under the guidance of Bharat Adsul and Supratik Chakraborty. A summary of my dissertation can be found here.
Research Interests
My research is in the areas of mathematical logic, particularly classical and finite model theory, and parameterized algorithms. My work is largely about adapting notions and results from classical (infinitary) model theory to the context of finite structures. Two of these of particular interest to me have been the ŁośTarski preservation theorem and the LöwenheimSkolem property. In parameterized algorithms, my interest is primarily in algorithmic metatheorems that provide a uniform means of obtaining fixed parameter tractable algorithms for all problems that can be defined in a given logic. Finally, I am also interested in structural (hyper)graph theory, particularly the notion of cliquewidth in the graph and geometric settings, in itself, and also for the various connections it has to logic and algorithms.
Selected Publications

FefermanVaught decompositions for prefix classes of first order logic
[abstract]
[paper]
Journal of Logic, Language and Information (JLLI), 32(1): 147174, 2023
The FefermanVaught theorem provides a way of evaluating a first order sentence φ on a disjoint union of structures by producing a decomposition of φ into sentences which can be evaluated on the individual structures and the results of these evaluations combined using a propositional formula. This decomposition can in general be nonelementarily larger than φ. We show that for first order sentences in prenex normal form with a fixed number of quantifier alternations, such a decomposition, further with the same number of quantifier alternations, can be obtained in time elementary in the size of φ. We obtain this result as a consequence of a more general decomposition theorem that we prove for a family of infinitary logics we define. We extend these results by considering binary operations other than disjoint union, in particular sumlike operations such as ordered sum and NLCsum, that are definable using quantifierfree interpretations. 
Cliquewidth of point configurations
(with
Onur Çağırıcı,
Petr Hliněný, and
Filip Pokrývka)
[abstract]
[
paper]
Journal of Combinatorial Theory, Series B, Vol. 158 (Part 1): 4373, 2023
While structural width parameters (of the input) belong to the standard toolbox of graph algorithms, it is not the usual case in computational geometry. As a case study we propose a natural extension of the structural graph parameter of cliquewidth to geometric point configuration represented by their order type. We study basic properties of this cliquewidth notion, and show that it is aligned with the general concept of cliquewidth of relational structures by Blumensath and Courcelle (2006). We also relate the new notion to monadic secondorder logic of point configurations. As an application, we provide several linear FPT time algorithms for geometric point problems which are NPhard in general, in the special case that the input point set is of bounded cliquewidth and the cliquewidth expression is also given. 
MSO undecidability for some hereditary classes of unbounded cliquewidth
(with Anuj Dawar)
[abstract]
[paper]
[pdf]
[slides]
[arxiv]
Proc. of the 30^{th} Computer Science Logic (CSL), Göttingen, Germany, pp. 17:117:17, February 2022
Seese's conjecture for finite graphs states that monadic secondorder logic (MSO) is undecidable on all graph classes of unbounded cliquewidth. We show that to establish this it would suffice to show that grids of unbounded size can be interpreted in two families of graph classes: minimal hereditary classes of unbounded cliquewidth; and antichains of unbounded cliquewidth under the induced subgraph relation. We explore all the currently known classes of the former category and establish that grids of unbounded size can indeed be interpreted in them. 
Pseudofiniteness of arbitrary graphs of bounded shrubdepth
[abstract]
[arxiv]
ArXiv preprint, February 2022
We consider classes of arbitrary (finite or infinite) graphs of bounded shrubdepth, specifically the classes TM_{r}(d) of arbitrary graphs that have tree models of height d and r labels. We show that the graphs of TM_{r}(d) are MSOpseudofinite relative to the class TM^{f}_{r}(d) of finite graphs of TM_{r}(d); that is, that every MSO sentence true in a graph of TM_{r}(d) is also true in a graph of TM^{f}_{r}(d). We also show that TM_{r}(d) is closed under ultraproducts and ultraroots. These results have two consequences. The first is that the index of the MSO[m]equivalence relation on graphs of TM_{r}(d) is bounded by a (d+1)fold exponential in m. The second is that TM_{r}(d) is exactly the class of all graphs that are MSOpseudofinite relative to TM^{f}_{r}(d). 
FefermanVaught decompositions for prefix classes of first order logic
[abstract]
[paper]
[pdf]
[slides]
[arxiv]
Proc. of the 9^{th} Indian Conference on Logic and Applications (ICLA), Chennai, India, March 2021, pp. 111116
The FefermanVaught theorem provides a way of evaluating a first order sentence φ on a disjoint union of structures by producing a decomposition of φ into sentences which can be evaluated on the individual structures and the results of these evaluations combined using a propositional formula. This decomposition can in general be nonelementarily larger than φ. We show that for FO sentences in prenex normal form with a fixed number of quantifier alternations, such a decomposition can be obtained in time elementary in the size of φ. 
Extension preservation in the finite and prefix classes of first order logic
(with Anuj Dawar)
[abstract]
[paper]
[pdf]
[slides]
[video]
Proc. of the 29^{th} Computer Science Logic (CSL), Ljbuljana, Slovenia, January 2021, pp. 18:118:13, Schloss Dagstuhl  LZI
It is well known that the classic ŁośTarski preservation theorem fails in the finite: there are firstorder definable classes of finite structures closed under extensions which are not definable (in the finite) in the existential fragment of firstorder logic. We strengthen this by constructing for every n, firstorder definable classes of finite structures closed under extensions which are not definable with n quantifier alternations. The classes we construct are definable in the extension of Datalog with negation and indeed in the existential fragment of transitiveclosure logic. This answers negatively an open question posed by Rosen and Weinstein. 
Some classical model theoretic aspects of bounded shrubdepth classes
[abstract]
[]paper
[pdf]
Arxiv preprint, October 2020
We consider classes of arbitrary (finite or infinite) graphs of bounded shrubdepth, specifically the class TM_{r, p}(d) of plabeled arbitrary graphs whose underlying unlabeled graphs have tree models of height d and r labels. We show that this class satisfies an extension of the classical LöwenheimSkolem property into the finite and for MSO. This extension being a generalization of the small model property, we obtain that the graphs of TM_{r, p}(d) are pseudofinite. In addition, we obtain as consequences entirely new proofs of a number of known results concerning bounded shrubdepth classes (of finite graphs) and TM_{r, p}(d). These include the small model property for MSO with elementary bounds, the classical compactness theorem from model theory over TM_{r, p}(d), and the equivalence of MSO and FO over TM_{r, p}(d) and hence over bounded shrubdepth classes. The proof for the last of these is via an adaptation of the proof of the classical Lindström's theorem characterizing FO over arbitrary structures. 
Cliquewidth of point configurations
(with
Onur Çağırıcı,
Petr Hliněný, and
Filip Pokrývka)
[abstract]
[paper]
[pdf]
Proc. of the 46^{th} International Workshop on Graph Theoretic Concepts in Computer Science, Leeds, UK, June 2020, pp. 5466, Springer
While structural width parameters (of the input) belong to the standard toolbox of graph algorithms, it is not the usual case in computational geometry. As a case study we propose a natural extension of the structural graph parameter of cliquewidth to geometric point configuration represented by their order type. We study basic properties of this cliquewidth notion, and show that it is aligned with the general concept of cliquewidth of relational structures by Blumensath and Courcelle (2006). We also relate the new notion to monadic secondorder logic of point configurations. As an application, we provide several linear FPT time algorithms for geometric point problems which are NPhard in general, in the special case that the input point set is of bounded cliquewidth and the cliquewidth expression is also given. 
Exact crossing number parameterized by vertex cover
(with Petr Hliněný)
[abstract]
[paper]
[pdf]
[slides]
Proc. of the 27^{th} International Symposium on Graph Drawing and Network Visualization (GD), Prague, Czech Republic, September 2019, pp.307319, Springer
We prove that the exact crossing number of a graph can be efficiently computed for simple graphs having bounded vertex cover. In more precise words, Crossing Number is in FPT when parameterized by the vertex cover size. This is a notable advance since we know only very few nontrivial examples of graph classes with unbounded and yet efficiently computable crossing number. Our result can be viewed as a strengthening of a previous result of Lokshtanov [arXiv, 2015] that Optimal Linear Arrangement is in FPT when parameterized by the vertex cover size, and we use a similar approach of reducing the problem to a tractable instance of Integer Quadratic Programming as in Lokshtanov’s paper. 
Revisiting the generalized ŁośTarski theorem
[abstract]
[paper]
[pdf]
[slides]
Proc. of the 8^{th} Indian Conference on Logic and its Applications (ICLA), Delhi, India, March 2019, pp. 7688, Springer
We present a new proof of the generalized ŁośTarski theorem (GLT(k)) from [1], over arbitrary structures. Instead of using λsaturation as in [1], we construct just the "required saturation" directly using ascending chains of structures. We also strengthen the failure of GLT(k) in the finite shown in [2], by strengthening the failure of the ŁośTarski theorem in this context. In particular, we prove that not just universal sentences, but for each fixed k, even Σ^{0}_{2} sentences containing k existential quantifiers fail to capture hereditariness in the finite. We conclude with two problems as future directions, concerning the ŁośTarski theorem and GLT(k), both in the context of all finite structures.
[1] Sankaran, A., Adsul, B., Chakraborty, S.: A generalization of the ŁośTarski preservation theorem. Annals of Pure and Applied Logic, 167(3), 189210 (2016)
[2] Sankaran, A., Adsul, B., Madan, V., Kamath, P., Chakraborty, S.: Preservation under substructures modulo bounded cores. Proceedings of WoLLIC 2012, Buenos Aires, Argentina, 36 September, 2012, pp. 291–305 (2012) 
A finitary analogue of the downward LöwenheimSkolem property
[abstract]
[paper]
[pdf]
[slides]
[Talk venues]
Proc. of the 26^{th} Computer Science Logic (CSL), Stockholm, Sweden, August 2017, pp. 37:137:21, Schloss Dagstuhl  LZI
We present a modeltheoretic property of finite structures, that can be seen to be a finitary analogue of the wellstudied downward LöwenheimSkolem property from classical model theory. We call this property the Lequivalent bounded substructure property, denoted LEBSP, where L is either FO or MSO. Intuitively, LEBSP states that a large finite structure contains a small "logically similar" substructure, where logical similarity means indistinguishability with respect to sentences of L having a given quantifier nesting depth. It turns out that this simply stated property is enjoyed by a variety of classes of interest in computer science: examples include regular languages of words, trees (unordered, ordered or ranked) and nested words, and various classes of graphs, such as cographs, graph classes of bounded treedepth, those of bounded shrubdepth and npartite cographs.
Further, LEBSP remains preserved in the classes generated from the above by operations that are implementable using quantifierfree translation schemes. All of the aforementioned classes admit natural tree representations for their structures. We use this fact to show that the small and logically similar substructure of a large structure in any of these classes, can be computed in time linear in the size of the tree representation of the structure, giving linear time fixed parameter tractable (f.p.t.) algorithms for checking Ldefinable properties of the large structure. We conclude by presenting a strengthening of LEBSP, that asserts "logical selfsimilarity at all scales" for a suitable notion of scale. We call this the logical fractal property and show that most of the classes mentioned above are indeed, logical fractals. Oct '17: (Invited talk) The annual meet of the Calcutta Logic Circle, Kolkata, India
 Sep '17: Department of Informatics, RheinischWestfälische Technische Hochschule (RWTH), Aachen, Germany
 Aug '17: Institute of Informatics, University of Warsaw, Poland
 Aug '17: (*) The 26^{th} International Conference on Computer Science Logic (CSL) 2017, Stockholm, Sweden
 Dec '16: (Invited talk) International Conference of the Indian Mathematics Consortium (TIMC) in cooperation with the American Mathematical Society (AMS), Varanasi, India
 Nov '16: Department of Mathematics, University of California at Berkeley, USA
 Nov '16: The Graduate Center, City University of New York (CUNY), USA
 Oct '16: Department of Computer Science, IIT Patna, India

A generalization of the ŁośTarski preservation theorem
(with
Bharat Adsul and
Supratik Chakraborty)
[abstract]
[paper]
[pdf]
Annals of Pure and Applied Logic, Vol. 167(3), 189210, 2016
We present new parameterized preservation properties that provide for each natural number k, semantic characterizations of the ∃^{k}∀^{*} and ∀^{k}∃^{*} prefix classes of first order logic sentences, over the class of all structures and for arbitrary finite vocabularies. These properties, that we call preservation under substructures modulo kcruxes and preservation under kary covered extensions respectively, correspond exactly to the classical properties of preservation under substructures and preservation under extensions, when k equals 0. As a consequence, we get a parameterized generalization of the Łoś–Tarski preservation theorem for sentences, in both its substructural and extensional forms. We call our characterizations collectively the generalized Łoś–Tarski theorem for sentences. We generalize this theorem to theories, by showing that theories that are preserved under kary covered extensions are characterized by theories of ∀^{k}∃^{*} sentences, and theories that are preserved under substructures modulo kcruxes, are equivalent, under a wellmotivated modeltheoretic hypothesis, to theories of ∃^{k}∀^{*} sentences. In contrast to existing preservation properties in the literature that characterize the Σ^{0}_{2} and Π^{0}_{2} prefix classes of FO sentences, our preservation properties are combinatorial and finitary in nature, and stay nontrivial over finite structures as well. 
A generalization of the ŁośTarski preservation theorem over classes of finite structures
(with
Bharat Adsul and
Supratik Chakraborty)
[abstract]
[paper]
[pdf]
[slides]
[Talk venues]
Proc. of the 39^{th} Mathematical Foundations of Computer Science (MFCS), Budapest, Hungary, August 2014, pp. 474485, Springer
We present a logicbased combinatorial property of classes of finite structures that allows an effective generalization of the ŁośTarski preservation theorem to hold over classes satisfying the property. The wellstudied classes of words and trees, and structures of bounded treedepth are shown to satisfy the property. We also show that starting with classes satisfying this property, the classes generated by applying composition operations like disjoint union, cartesian and tensor products, inherit the property. We finally show that all classes of structures that are wellquasiordered under the embedding relation satisfy a natural generalization of our property. Sep '15: Department of Mathematics, RheinischWestfälische Technische Hochschule (RWTH), Aachen, Germany
 Aug '15: (Poster presentation) Heidelberg Laureate Forum 2015, Heidelberg, Germany
 Aug ’14: (*) The 39^{th} International Symposium on the Mathematical Foundations of Computer Science (MFCS), Budapest, Hungary

Preservation under substructures modulo bounded cores
(with
Bharat Adsul,
Vivek Madan,
Pritish Kamath and
Supratik Chakraborty)
[abstract]
[paper]
[pdf]
[slides]
[Talk venues]
Proc. of the 19^{th} Workshop on Logic, Language, Information and Computation (WoLLIC), Buenos Aires, Argentina, September 2012, Vol. 7456, pp. 291305, Springer
We investigate a modeltheoretic property that generalizes the classical notion of preservation under substructures. We call this property preservation under substructures modulo bounded cores, and present a syntactic characterization via Σ^{0}_{2} sentences for properties of arbitrary structures definable by FO sentences. Towards a sharper characterization, we conjecture that the count of existential quantifiers in the and Σ^{0}_{2} sentence equals the size of the smallest bounded core. We show that this conjecture holds for special fragments of FO and also over special classes of structures. We present a (not FOdefinable) class of finite structures for which the conjecture fails, but for which the classical ŁośTarski preservation theorem holds. As a fallout of our studies, we obtain combinatorial proofs of the ŁośTarski theorem for some of the aforementioned cases. Oct '12: Model Theory Seminar, Graduate Center, City University of New York (CUNY), USA
 Oct '12: Computational Logic Seminar, Graduate Center, City University of New York (CUNY), USA
 Sep ’12: (*) The 19^{th} Workshop for Logic, Language, Information and Computation (WoLLIC), Buenos Aires, Argentina
Thesis

A generalization of the ŁośTarski preservation theorem
[summary]
[synopsis]
[dissertation]
[arxiv]
[defence slides]
Doctoral dissertation submitted to the Department of Computer Science and Technology, IIT Bombay, India, August 2016.
Other refereed articles/abstracts

Cliquewidth of point configurations
(with Petr Hliněný)
[newsletter]
Invited article in the Parameterized Complexity News (Newsletter of the Parameterized Complexity community), Vol 17, No. 3, December 2021

A generalization of the ŁośTarski preservation theorem
(with
Bharat Adsul and
Supratik Chakraborty)
[paper]
[slides]
Abstract accepted at the 14^{th} Asian Logic Conference, IIT Bombay, India, January 2015

A generalization of the ŁośTarski preservation theorem via characterizations of Σ^{0}_{n} and Π^{0}_{n} theories
[abstract]
[paper]
[slides]
Abstract accepted at the 29^{th} Annual Conference of the Ramanujan Mathematical Society, IISER Pune, India, June 2014
We present a family of preservation theorems that provide semantic characterization of Σ^0_n and Π^0_n theories, for each n >= 1, and hence generalize the classical ŁośTarski preservation theorem. Vis`avis the characterizations of the aforesaid theories provided by H. J. Keisler in 1960 using sandwiches of finite orders, our semantic properties as well as our proofs are much simpler, and more naturally generalize the ŁośTarski theorem. We also explicitly relate the modeltheoretic operations involved in our results, with those of Keisler.
Professional Activities
Teaching
Supervisor of the Bachelors thesis titled "Algorithmic study of equivalence relations over finite graphs based on logics of bounded rank" submitted to the Department of Computer Science and Technology, University of Cambridge

Supervisor for Part IB Complexity Theory (second year Bachelors course) in '19, '20 and '21, and Part III Topics in Logic and Complexity (Masters course) in '20

Lecturer at the Theoretical Computer Science Summer Student Programme 2018 conducted by IMSc, Chennai for visiting Undergraduate and Masters students across India. This is a part of the larger Summer Research programme conducted by IMSc.

Teaching assistant for various Bachelors and Masters courses at the Department of Computer Science and Engineering, IIT Bombay.
Some talks and reports

Program verification using small models
[abstract]
[report]
[slides]
Accepted short talk at the Workshop on Research Highlights in Programming Languages (RHPL) 2023, December, 2023
We explore the use of methods from model theory in the verification of array programs. Given a program P and an assertion A to check of P, we formulate these respectively as sentences φ_{P} and φ_{A} of multisorted first order logic. The sentence φ_{P} is such that modulo a small set φ_{{ax}} of axioms, the models of φ_{P} are in 11 correspondence with (suitably abstract representations of) the executions of P on arbitrary input arrays. Likewise, the models of φ_{A} restricted to the class of models of φ_{P} \wedge φ_{ax}, correspond to (suitably abstracted) executions of P that satisfy the assertion A.
Our approach to verifying the program P against the assertion A consists of showing that the sentence α_{P, A} := φ_{ax} ∧ φ_{P} ∧ ¬φ_{A} has thesmall model property . That is, if α_{P, A} has a model of some finite size, then there is also such a model in which the domains interpreting the sorts have all sizes bounded by a small function of P and A. The desired verification reduces to searching for models of α_{P, A} of sizes within the mentioned bound. We examine specific classes of programs and assertions, and establish the small model property for α_{P, A} by showing that models of α_{P, A} that are large admit local reductions that are effected by "removal of iterations" in the executions of P that they correspond to. 
First order Skolem function synthesis over finite structures
[abstract]
Presented at the Formal Methods Update Meet (FMU) 2023, JuneJuly, 2023
The problem of Skolem function synthesis (SFS) asks if there is an algorithm that, given a prenex first order (FO) formula φ and a structure A, synthesizes the interpretations in A of the Skolem functions for the existential variables of φ, assuming that computable such interpretations exist. Here synthesis means constructing algorithms that compute the said interpretations. This problem has been studied extensively in the Boolean setting but a commensurate study for FO is lacking in the literature. A recent paper of Akshay and Chakraborty (MFCS '22) provides a (possibly the first) systemmatic study of SFS for FO showing amongst other results that SFS in general has a negative answer, and that if the structure is fixed, then SFS has a positive answer precisely when the elementary diagram of the structure is decidable.
The characterization above immediately implies that SFS is in the affirmative for all finite structures. In fact it can be shown that there is an algorithm that for any given finite structure A of size n, synthesises the interpretations in A of the Skolem functions for any given prenex FO formula φ, in time n^{O(φ)}. However with φ and A both seen as part of the input, this running time is exponential. This motivates asking: under what conditions can we get polynomial time algorithms for SFS? This talk explores the stated question and proposes that a finitary adaptation of a classical modeltheoretic notion called the Löwenheim–Skolem property might offer some answers. 
Extension preservation in the finite and prefix classes of first order logic
(with Anuj Dawar)
[abstract]
[slides]
[video]
Invited talk at the Young Researchers  Online Worldwide Logic Seminar (YROWLS), November, 2020
It is well known that the classic ŁośTarski preservation theorem fails in the finite: there are firstorder definable classes of finite structures closed under extensions which are not definable (in the finite) in the existential fragment of firstorder logic. We strengthen this by constructing for every n, firstorder definable classes of finite structures closed under extensions which are not definable with n quantifier alternations. The classes we construct are definable in the extension of Datalog with negation and indeed in the existential fragment of transitiveclosure logic. This answers negatively an open question posed by Rosen and Weinstein. 
Hereditariness in the finite and prefix classes of first order logic
(with Anuj Dawar)
[abstract]
[slides]
[Talk venues]
This talk presents an alternate (and chronologically first) proof of the central result of this paper. February 2019.
The LosTarski theorem is a result from classical model theory that states that over arbitrary (finite or infinite) structures, a first order (FO) sentence is hereditary if, and only if, it is equivalent to a universal sentence. This theorem however fails when restricted to finite structures. Tait (1959) and independently Gurevich and Shelah (1984) showed that in the finite (i.e. over the class of all finite structures), there is an FO sentence that is hereditary but that is not equivalent to any universal sentence.
In a recent paper [2], a strengthening of the above failure was shown: in the finite, for every k, there is a hereditary FO sentence that is not equivalent to any Σ^{0}_{2} sentence that contains k existential quantifiers. We generalize this result by showing in the finite, that for every n, there is a hereditary FO sentence φ_{n} that is not equivalent to any Σ^{0}_{n} sentence. In short, (FO)hereditariness over all finite structures is not capturable by any prefix class of FO. We show further that ¬φ_{n} is expressible in Datalog(≠, ¬), thus answering in the negative an open question posed by Rosen and Weinstein [1], that asks whether FO ∩ Datalog(≠, ¬) is contained (semantically) inside some prefix class of FO. The methods used to show our result extend the ideas from [2] in a significant way, and involve the construction of structures that exhibit selfsimilarity.
This is joint work with Anuj Dawar.
[1] Eric Rosen and Scott Weinstein. Preservation theorems in finite model theory. In International Workshop on Logic and Computational Complexity, pages 480–502. Springer, 1994.
[2] Abhisekh Sankaran. Revisiting the generalized LosTarski theorem. In Logic and Its Applications  8th Indian Conference, ICLA 2019, Delhi, India, March 15, 2019, Proceedings, pages 76–88, 2019.
 Nov '19: Department of Computer Science, University of Oxford, UK
 Apr '19: Department of Informatics, University of Bergen (UiB), Bergen, Norway
 Apr '19: Faculty of Informatics, Masaryk University, Brno, Czechia
 Mar '19: Department of Computer Science and Engineering, IIT Bpmbay, Mumbai, India
 Mar ’19: The Institute of Mathematical Sciences, Chennai, India

Algorithmic metatheorems  a survey
[abstract]
[slides][Talk venues]
A survey of the methods used in showing algorithmic meta theorems over various classes of structures.We present a (partial) survey of the area of algorithmic metatheorems. These theorems provide fixed parameter tractable (FPT) algorithms for the model checking problem, namely the problem of checking if an input structure from a given class of structures satisfies a property that is expressible in a given logic, like say first order logic (FO) or monadic second order logic (MSO). The parameters in these algorithms are the size of the logical description of the property, along with (the numerical description of) some structural aspect of the input structure. We look at various wellstudied classes of posets and graphs that admit such FPT algorithms and give the intuitive ideas behind the techniques involved. Apr '22: Theory Seminar, Department of Computer Science and Engineering, IIT Delhi, India
 Jul '18: Formal Methods Update (FMU) Meeting, BITS Goa, India

Kernels using composition
[abstract]
[slides]
Presented at the Parameterized Complexity Week, IMSc Chennai, India, October, 2017
We present a modeltheoretic approach for the problem of FO/MSO model checking over a given class of graphs. Specifically, we consider classes that are represented using trees in which the leaf nodes are labeled with simple structures (typically, point graphs) and the internal nodes are labeled with operations on structures. We show that if the operations satisfy the FefermanVaught composition property, then the model checking problem admits kernelization and linear time f.p.t. algorithms. This result provides a unified approach for handling a variety of sparse and dense graph classes: graphs of bounded treewidth, bounded treedepth, bounded shrubdepth,bounded cliquewidth/rankwidth and mpartite cographs, and graphs obtained from these using various wellstudied operations such as complementation, linegraph, disjoint union, seriesparallel connects and the Cartesian and tensor products. 
Using preservation theorems for inexpressibility results in first order logic
(with
Bharat Adsul,
S. Akshay,
Supratik Chakraborty,
Nutan Limaye)
[abstract]
[pdf]
A set of results that came about when the efforts at proving GLT(k) were still on. IIT Bombay, India, August 2012
We investigate the applications of preservation theorems in showing inexpressibility results in FO. 
Reminiscences from the ACM A. M. Turing Centenary Celebrations at San Francisco, USA, June 2012 [article] [ACM Press Release] [On Michael Rabin]

Interview for Bitstream, the newsletter of the Department of CSE, IIT Bombay [newsletter]
Abhisekh Sankaran, 2023