Kamal Lodaya
with Ashok Subramanian
Research interests:
Logic, Petri nets, concurrency, automata.
Graduate teaching:
Theory of computation, logic, logics of programs, concurrency, automata,
infinite discrete structures, programming languages, computability, databases.
Short courses:
Logic on words, trees and graphs .
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
CLC '99 , 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 Chennai, 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 .
Univ of Chennai, 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 Chennai, 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:
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.
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;
CLC '03 , Kolkata, 13-16 Oct 03;
CLC '02 , Kolkata, 28-31 Oct 02.
Parsing as deduction.
CLC '01 , Kolkata, 18-22 June 01.
Update talks:
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.
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 logic of finite graphs .
6th Formal methods update,
Kanpur, 12-15 Apr 07; Mumbai, Mar 02.
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.
Reviews:
Reinhard Kahle and Michael Rathjen (eds).
Gentzen's centenary: the quest for consistency .
Computing Reviews , July 16.
Maria Manzano, Ildikó Sain and Enrique Alonso (eds).
The life and work of Leon Henkin: essays on his contributions .
Computing Reviews , Oct 15.
Thomas Müller (ed) -
Nuel Belnap on indeterminism and free action .
Computing Reviews , Nov 14.
Robert Trypuz (ed) -
Krister Segerberg on logic of actions .
Computing Reviews , Sep 14.
Sven Ove Hansson (ed) -
David Makinson on classical methods for non-classical problems .
Computing Reviews , Aug 14.
Tiziano Villa, Nina Yevtushenko, Robert Brayton, Alan Mishchenko,
Alexandre Petrenko and Alberto Sangiovanni-Vincentelli -
The unknown component problem: theory and applications .
Computing Reviews , Nov 12.
Dov Gabbay and Karl Schlechta -
Logical tools for handling change in agent-based systems .
Computing Reviews , Oct 11.
Ernst-Erich Doberkat -
Stochastic coalgebraic logic .
Computing Reviews , Aug 11.
Manfred Droste, Werner Kuich and Heiko Vogler (eds) -
Handbook of weighted automata .
Computing Reviews , Mar 11.
Orna Grumberg, Michael Kaminski, Shmuel Katz and Shuly Wintner (eds) -
Languages: from formal to natural .
Computing Reviews , Feb 11.
Raymond Turner -
Computable models . Computing Reviews , Sep 10.
Jeffrey Shallit -
A second course in formal languages and automata theory .
Computing Reviews , Feb 10.
Arnon Avron, Nachum Dershowitz and Alexander Rabinovich (eds) -
Pillars of computer science .
Computing Reviews , Nov 09.
Javier Esparza and Keijo Heljanko -
Unfoldings .
Computing Reviews , Sep 09.
Marco Aiello, Ian Pratt-Hartmann and Johan van Benthem (eds) -
Handbook of spatial logics .
Computing Reviews , Nov 08.
Eric Schechter -
Classical and nonclassical logics .
Computing Reviews , Sep 06.
Leonid Libkin -
Elements of finite model theory .
Computing Reviews , Mar 05.
Melvin Fitting -
Types, tableaus and Gödel's god .
Computing Reviews , Nov 03.
(with
Sitabhra Sinha )
Michael Arbib (ed) -
The handbook of brain theory and neural networks .
Computing Reviews , June 03.
Stephen Wolfram -
A new kind of science .
Reviewed in 03.
Patrick Blackburn, Maarten de Rijke and Yde Venema -
Modal logic .
Computing Reviews , May 02.
Susantha Goonatilake -
Toward a global science:
mining civilizational knowledge .
Review of Development and Change
V ,2, Dec 00.
Melvin Fitting and Richard L. Mendelsohn -
First-order modal logic .
Computing Reviews , Mar 00.
Recent work:
(with Paritosh Pandya ).
Deterministic temporal logics and interval constraints ,
9th Methods for Modalities , Kanpur, EPTCS, to appear (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.
(with
Ramchandra Phawade )
Kleene theorems for synchronous products with matching .
Trans. Petri nets and other models of concurrency X
(Jörg Desel and Serge Haddad, eds.),
LNCS 9410 (2015), pp 84-108.
(with
A.V. Sreejith )
Counting quantifiers on word models .
14th Asian logic conference, Mumbai, 5-8 Jan 15.
Some finished work:
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, BITS Goa, 4 Nov 15;
Nakshatra , NIT Tiruchi, 16 Feb 14;
Eyes on Ison
(tamil slides ), IMSc, 13 Oct 13.
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
Aainanagar , a Bangla-English little magazine