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:

Logic and automata, behaviour and structure. 7th ISLA (Part 2) school, IIEST Shibpur, 17-22 Dec 18; 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; Proc Automata, Graphs and Logic, Chennai, Narosa (2019), to appear.
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.
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. 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:

The origin of computer science. BITS Goa, 15 Mar 18; Ahmedabad Univ, 12 Mar 18; Univ of Madras, 21-22 Nov 12; Tezpur Univ, 2 Nov 12.

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:

Roberto Gorrieri - Process algebras for Petri nets, Comp. Rev., online Feb 19.

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). Two-variable logics with some betweenness relations (2019), 40 pp.
Via. In Proc. 14th and 15th Asian logic, Mumbai and Daejeon, World Scientific (2019), pp 205-212.
(with A.V. Sreejith) Two-variable logic with counting quantifiers: complexity results. 21st DLT, Liège, LNCS 10396 (2017), pp 260-271.

Some finished work:

(with Paritosh Pandya). Deterministic temporal logics and interval constraints, 9th Methods for Modalities, Kanpur, EPTCS 243 (2017), pp 23-40.
(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