Computer Science faculty

Kamal Lodaya

Research interests: Logic, automata, Petri nets, concurrency.

Graduate teaching: Theory of computation, logic, logics of programs, concurrency, automata, infinite discrete structures, programming languages, computability, databases.

Short courses:

Programs, concurrency, communication, phones. Univ of Madras, 14 Nov 18; IMSc, 11-15 June 18 and 15 Feb 14; CMI, 20 July 15; IIT Guwahati, 14 Mar 14.

Logic on words, trees and graphs. Peking Univ, 16 Oct 18; IIT Madras, 11 Apr 16; Automata, graphs and logic, Madras Christian College, 7-8 Aug 15; 4th ISLA school, Manipal, 9-20 Jan 12; 1st Automata, concurrency and logic school, IMSc, 26-28 Jan 01; and 2nd CLC, Kolkata, 24-30 June 99.
Model checking. BITS Goa, 4-5 Nov 15; Tezpur Univ, 16-19 Mar 15; IMSc, 14-17 May 12; 2nd Automata, concurrency and logic school, IMSc, 24-26 Jan 03; Bangalore, 10 Sep-3 Oct 01.
Using formal logic in program correctness. BITS Goa, 4 Nov 15; Univ of Madras, 7 Dec 12; An invitation to theoretical computer science, IIT Madras/nptel, Dec 09-Apr 10; AVIT Paiyanoor, Feb 09; Practical program verification, Hyderabad, 14-18 Feb 08.
Programming concurrency and communication (slides). VIT Chennai, 19 Sep 13; IMSc, 23 June 12, June 11 and June-July 10; SNS College of Engg, Coimbatore, 25-26 Nov 10; PBS College, Vijayawada, 4-5 Aug 07; NIT Surathkal, 23-27 July 07; St Joseph's College, Tiruchirapalli, 26-28 Aug 04; and Sacred Heart College, Tirupattur, 26-30 Apr 04.
Turing machines and computability. BITS Goa, 15 Mar 18; Ahmedabad Univ, 12 Mar 18; Univ of Madras, 21-22 Nov 12; Tezpur Univ, 2 Nov 12; A celebration of Turing, IMSc thematic lectures, 25 Aug 12; Automata and computability workshop, Colombo, 29 July-5 Aug 02; and 2nd Theoretical aspects of computer science course, IMSc, 15 Oct-9 Nov 01.
Algorithms as machines. Resonance 14,4 (2009), pp 367-379. PSG Tech, Coimbatore, 2 Mar 12; Univ of Madras, 29-30 June 10 and 22-23 July 04; Easwari Engg College, Chennai, 30 Apr 10; IMSc, May-June 09; IIT Roorkee, 19 Jan 08; Kongu Engg College, Perundurai, 28-29 Dec 07; AK College of Engg, Krishnankoil, 28-29 Oct 06; and KSR College of Technology, Tiruchengode, 22-23 Sep 06.

Surveys and tutorials:

So many possible worlds go so many ways. IMSc, 6 Mar 18; 19th CLC, Kolkata, 13-15 Oct 17.
Branching automata. Univ de La Réunion, 26 Oct 17.
Description logics. Representation in AI school, IIT Mandi, 19-28 July 17.
Learning formal languages. IMSc, 30 May-3 June 16 and 22-26 June 15.
Automata, nets and models for concurrency. Univ de La Réunion, 7-9 Jan 16; TIFR Mumbai, May 09 and 21-23 Feb 06; and Univ of Birmingham, June 03.
Automata, concurrency and communication. BITS Goa, 6 Nov 15; Anna Univ, Chennai, 16 Nov 12; VIT Vellore, 14 July 11; Mumbai, 28 May 10; IMSc, Mar 10; and Formal theories of communication workshop, Lorentz Center, Leiden, 22-26 Feb 10.
Belief propagation. IMSc, 9-12 June 14 and 20-24 May 13.
Programs, proofs, languages and questions of provability. Concurrency workshop, TIFR Mumbai, 12 Nov 10.
Regularity. TIFR Mumbai, May 09, 4 July 08 and 6-9 Feb 07.
Timed and hybrid automata. Models of embedded computation workshop, Banasthali, 15-19 Mar 07.
Reasoning about time. 1st ISLA school, IIT Bombay, 3-18 Jan 06; 6th CLC, Kolkata, 13-16 Oct 03; 5th CLC, Kolkata, 28-31 Oct 02.
Parsing as deduction. 4th CLC, Kolkata, 18-22 June 01.

Update talks:

Unary temporal logics, points and intervals. 4th Asian philosophical logic workshop, Beijing, 20-21 Oct 18; 1st Automata, concurrency and timed systems workshop, Chennai, 29-31 Jan 09; 2nd Algebra, combinatorics and complexity workshop, Ekaterinburg, 1-3 Oct 08.
Between two- and three-variable logic on word models. 16th Formal methods update, Mandi, 17-18 July 17; 15th Asian logic conference, Daejeon, 10-14 July 17.
Axiomatizing regular expressions. IMSc, 28 Aug 15; 14th Formal methods update, Bangalore, 16-17 July 15; Mumbai, 18 June 15.
Automata from left and right. 13th Formal methods update, Kharagpur, 28-30 July 14.
50 years of the Krohn-Rhodes theorem. Chennai theory day, 3 Aug 13; 12th Formal methods update, Delhi, 27-28 July 13; Mumbai, 12 June 13.
Probabilistic systems and their verification. Guwahati, 1 Nov 12; IMSc, 30 Aug 12; 11th Formal methods update, Chennai, 19-21 July 12; Mumbai, June 12.
From temporal logic to circuits. 9th Formal methods update, Gandhinagar, 15-17 July 10.
(with M. Praveen) The Petri net reachability problem. 8th Formal methods update, Roorkee, 13-15 July 09; Mumbai, 18 Nov 08; and 2nd RP workshop, Liverpool, 15-17 Sep 08.
Doing automata theory over dense linear orders. 7th Formal methods update, Pune, 17-19 July 08.
(with Srikanth Srinivasan) Monadic logics of finite graphs. 6th Formal methods update, Kanpur, 12-15 Apr 07; Mumbai, Mar 02.
(with Antoine Meyer) Logical characterization of pushdown and automatic graphs. 5th Formal methods update, Guwahati, 3-6 July 06.
Separation logic. 4th Formal methods update, Mumbai, 18-22 July 05.
Infinite state automata. 3rd update, IMSc, 29 Feb-2 Mar 04.
Monadic second order logics and timed sequences. 2nd update, IMSc, 16-20 June 97.
1st update, IMSc, 7-11 Sep 92.

Book reviews:

Dov Gabbay and Karl Schlechta - A new perspective on nonmonotonic logics. Comp. Rev., May 18.
Stéphane Demri, Valentin Goranko and Martin Lange. Temporal logics in computer science: finite-state systems. Bull. Symb. Logic 23,2, June 17.
Katalin Bimbó (ed) - J. Michael Dunn on information based logics. Comp. Rev., July 17.
Reinhard Kahle and Michael Rathjen (eds). Gentzen's centenary: the quest for consistency. Comp. Rev., July 16.
Roberto Gorrieri and Cristian Versari - Introduction to concurrency theory. Math. Rev., Apr 16.
Maria Manzano, Ildikó Sain and Enrique Alonso (eds). The life and work of Leon Henkin: essays on his contributions. Comp. Rev., Oct 15.
Thomas Müller (ed) - Nuel Belnap on indeterminism and free action. Comp. Rev., Nov 14.
Robert Trypuz (ed) - Krister Segerberg on logic of actions. Comp. Rev., Sep 14.
Sven Ove Hansson (ed) - David Makinson on classical methods for non-classical problems. Comp. Rev., Aug 14.
Tiziano Villa, Nina Yevtushenko, Robert Brayton, Alan Mishchenko, Alexandre Petrenko and Alberto Sangiovanni-Vincentelli - The unknown component problem: theory and applications. Comp. Rev., Nov 12.
Dov Gabbay and Karl Schlechta - Logical tools for handling change in agent-based systems. Comp. Rev., Oct 11.
Ernst-Erich Doberkat - Stochastic coalgebraic logic. Comp. Rev., Aug 11.
Manfred Droste, Werner Kuich and Heiko Vogler (eds) - Handbook of weighted automata. Comp. Rev., Mar 11.
Orna Grumberg, Michael Kaminski, Shmuel Katz and Shuly Wintner (eds) - Languages: from formal to natural. Comp. Rev., Feb 11.
Raymond Turner - Computable models. Comp. Rev., Sep 10.
Jeffrey Shallit - A second course in formal languages and automata theory. Comp. Rev., Feb 10.
Arnon Avron, Nachum Dershowitz and Alexander Rabinovich (eds) - Pillars of computer science. Comp. Rev., Nov 09.
Javier Esparza and Keijo Heljanko - Unfoldings. Comp. Rev., Sep 09.
Marco Aiello, Ian Pratt-Hartmann and Johan van Benthem (eds) - Handbook of spatial logics. Comp. Rev., Nov 08.
Eric Schechter - Classical and nonclassical logics. Comp. Rev., Sep 06.
Leonid Libkin - Elements of finite model theory. Comp. Rev., Mar 05.
Melvin Fitting - Types, tableaus and Gödel's god. Comp. Rev., Nov 03.
(with Sitabhra Sinha) Michael Arbib (ed) - The handbook of brain theory and neural networks. Comp. Rev., June 03.
Stephen Wolfram - A new kind of science. Reviewed in 03.
Patrick Blackburn, Maarten de Rijke and Yde Venema - Modal logic. Comp. Rev., May 02.
Melvin Fitting and Richard L. Mendelsohn - First-order modal logic. Comp. Rev., Mar 00.
Stephen Bloom and Zoltan Ésik - Iteration theories. Comp. Rev., May 95.
D. Rydeheard and R. Burstall - Computational category theory. Comp. Rev., Oct 89.
Mike Shields - An introduction to automata theory. Comp. Rev., Jan 89.

Recent work:

(with Andreas Krebs, Paritosh Pandya and Howard Straubing). An algebraic decision procedure for two-variable logic with a between relation, 27th CSL, Birmingham, LIPIcs 119 (2018), pp 28:1-17.
(with A.V. Sreejith) Two-variable logic with counting quantifiers: complexity results. 21st DLT, Liège, LNCS 10396 (2017), pp 260-271.
Logic as regular behaviour. Proc Automata, Graphs and Logic, Chennai, Narosa (2018), to appear.
(with Paritosh Pandya). Deterministic temporal logics and interval constraints, 9th Methods for Modalities, Kanpur, EPTCS 243 (2017), pp 23-40.
(with Andreas Krebs, Paritosh Pandya and Howard Straubing). Two-variable logic with a between relation, 31st LICS, New York (2016), pp 106-115.

Some finished work:

(with Ramchandra Phawade) Kleene theorems for synchronous products with matching. Trans. Petri nets and other models of concurrency X, LNCS 9410 (2015), pp 84-108.
A language-theoretic view of verification. In Modern applications of automata theory (Deepak D'Souza and Priti Shankar, eds), IISc research monographs, World Scientific (2012), pp 149-169.
(with R. Ramanujam) Axioms for locality as product. In Reminiscing ideas and interactions: essays in honour of Mihir Kr. Chakraborty, Calcutta Logic Circle (2011), pp 162-180.
(with Kalpesh Kapoor and Uday Reddy) Fine-grained concurrency with separation logic. J. Philos. Logic 40,5 (Oct 2011), pp 583-632.
(with M. Praveen) Parameterized complexity results for 1-safe nets. 22nd Concur, Aachen, LNCS 6901 (2011), pp 358-372.
(with Madhavan Mukund and Ramchandra Phawade) Kleene theorems for product systems. 13th DCFS, Limburg, LNCS 6808 (2011), pp 235-247.
(with A.V. Sreejith) LTL can be more succinct. 8th ATVA, Singapore, LNCS 6252 (2010), pp 245-258.
(with Paritosh Pandya and Simoni Shah) Around dot depth two. 14th DLT, London (Canada), LNCS 6224 (2010), pp 303-314.
(with M. Praveen) Modelchecking counting properties of 1-safe nets with buffers in paraPspace. 29th FSTTCS, Kanpur, LIPIcs 4 (2009), pp 347-358.
(with Paritosh Pandya and Simoni Shah) Marking the chops: an unambiguous temporal logic. 5th TCS, Milano, IFIP 273 (2008), pp 461-476.
(with M. Praveen) Analyzing reachability for some Petri nets with fast growing markings. 2nd RP, Liverpool, ENTCS 223 (2008), pp 215-237.
Marking time. In Logic, navya-nyāya and applications ( Mihir K.Chakraborty, Benedikt Löwe, Madhabendra Nath Mitra and Sundar Sarukkai, eds.), College Publications (2008), pp 185-203.
(with Paritosh Pandya) A dose of timed logic, in guarded measure. 4th Formats, Paris, LNCS 4202 (2006), pp 260-273.
Product automata and process algebra. 4th SEFM, Pune, IEEE (2006), pp 128-136.
A regular viewpoint on processes and algebra. Acta Cybernetica 17,4 (2006), pp 751-763.
Petri nets, event structures and algebra. In Formal models, languages and applications (K.G. Subramanian, K. Rangarajan and Madhavan Mukund, eds.), World Scientific (2006), pp 246-259.
(with D. Ranganayakulu and K. Rangarajan) Hierarchical structure of 1-safe Petri nets. 8th Asian, Mumbai, LNCS 2896 (2003), pp 173-187.
(with D. Ranganayakulu) Infinite series-parallel posets of 1-safe nets. Proc Algorithms and Artificial Systems, Chennai, Allied (2003), pp 107-124.
(with R. Ramanujam) An automaton model of user-controlled navigation on the web. 5th CIAA, London (Canada) '00, LNCS 2088 (2001), pp 208-216.
Sharpening the undecidability of interval temporal logic. 6th Asian, Penang, LNCS 1961 (2000), pp 290-298.
(with Pascal Weil) Rationality in algebras with a series operation. Information and Computation 171,2 (2001), pp 269-293.
(with Pascal Weil) Series-parallel languages and the bounded-width property. TCS 237,1-2 (2000), pp 347-380.
(with Rohit Parikh, R. Ramanujam and P.S. Thiagarajan) A logical study of distributed transition systems. Information and Computation 119,1 (1995), pp 91-115.
(with R. Ramanujam and P.S. Thiagarajan) Decidability of a partial order based temporal logic. 20th ICALP, Lund, LNCS 700 (1993), pp 582-592.
(with R. Ramanujam and P.S. Thiagarajan) Temporal logics for communicating sequential agents: I. IJFOCS 3,2 (1992), pp 117-159.
(with Madhavan Mukund, R. Ramanujam and P.S. Thiagarajan) Models and logics for true concurrency. Sādhanā 17, Part 1 (1992), pp 131-165.
(with R.K. Shyamasundar) Proof theory for exception handling in a tasking environment. Acta Informatica 28 (1991), pp 7-41.
Proof theory for exception handling in distributed programs, PhD thesis, TIFR, Bombay Univ (1988).

Edited collections:

Proc. 5th ICLA, Chennai, LNCS 7750, Springer (2013).
(with Meena Mahajan) Proc. 30th FSTTCS, Chennai, LIPIcs 8 (2010).
(with Madhavan Mukund and R. Ramanujam) Perspectives in concurrency theory, Universities Press, CRC Press (2009).
The paper "Folding systems of communicating agents" in this volume, by myself and S.Paul, has a serious bug. Philippe Darondeau gave us an example event structure from his paper "Context-free event domains are recognizable" with Eric Badouel and J.-C. Raoult (1999) on which our proof does not work.
(with Meena Mahajan) Proc. 24th FSTTCS, Chennai, LNCS 3328, Springer (2004).

Other stuff:

(with Baskar Anguraj) Death and life at comets (tamil slides), IMSc, 8 May 18; Puducherry Science Centre, 25 Feb 17; BITS Goa, 4 Nov 15; Nakshatra, NIT Tiruchi, 16 Feb 14; Eyes on Ison, IMSc, 13 Oct 13.
(with pictures by R. Shankar) Eclipse at Tawang (22 July 09). Nehru High School, Chennai, 21 Aug 17; Aainanagar, July 14; National College, Tiruchi, 31 Aug 09.
R. Shankar. The annular solar eclipse, Kanyakumari (15 Jan 10).
Review of Susantha Goonatilake - Toward a global science: mining civilizational knowledge. Rev. Dev. Change V,2, Dec 00.
Whither traditional science and technology? Seminar 413, Jan 94.
Jantar mantar, a science magazine for children in English
Thulir, a science magazine for children in Tamil
(An article about) Tamil nadu science forum, a voluntary organization which publishes both these magazines
Pondicherry science forum, a voluntary organization which supports both these magazines