I worked with the BIP team (now called POP-ART)  at INRIA Rhone-Alpes, Grenoble, FRANCE, under Eric Rutten  for my summer internship during May - July 2001. My work consisted of specifying in the synchronous programming language Signal, an excavator system with a number of predefined control tasks, determining synthesis objectives relevant to the application (in the form of properties to be made True), synthesizing the controller using the functionality offered by the model checking tool Sigali, and finally constructing a graphical simulation environment for observing the behavior of the controlled system. Discrete controller synthesis is a wonderful approach to solving reactive control problems using a compiler(synthesizer) which automatically generates a control program from a description of control objectives and of course a description of the system to be controlled. Starting from a representation of the possible behaviors of the system(e.g. in the form of a finite state automaton) and the properties to be satisfied by the controlled system, the synthesis directly produces the constained automaton, i.e., the one that presents only those behaviors that satisfy the required properties.

I worked for my final year B.Tech. dissertation under Prof. Rajeev Kumar  at IIT Kharagpur. We developed a novel approach to topological design of communication networks using multiobjective genetic optimization and obtained highly interesting results. Designing communication networks is a multi-criterion and multi-constraint optimization problem involving possibly conflicting objectives. Such a design is a complex real-world problem and is NP-hard. Since the solution is not known a priori, many implementations of multiobjective genetic optimization techniques are not very effective. In this work, we used a Pareto Converging Genetic Algorithm (PCGA) and made a number of interesting observations about convergence, diversity and scalability. We optimized two primary objectives namely network delay and installation cost subject to satisfaction of reliability and flow constraints. This method can be applied successfully where traditional approaches such as branch exchange heuristics are rendered infeasible due to large node sizes.

After completing by B.Tech., I joined the Formal Verification Research Group  at IIT Kharagpur for a year (June 2002 - July 2003) under  Prof. P. P. Chakrabarti and Prof. Pallab Dasgupta . I worked in a research project  related to developing  Coverage Metrics for Model Checking. The focus here is coverage analysis for formal property verification. Given two sets of specifications, one at a more abstract architectural level (A-Spec),  and another at the lower RTL level, the issue is to decide whether the latter "covers" or "implies"  the former. In case 100% coverage is not reported, the job is to express the part of the A-Spec that is left  uncovered (in most cases, it is a weakened version of an existing A-Spec) and how to augment the RTL specs  to achieve 100% coverage. This problem is shown to be computationally hard and non-trivial. We developed the concept of property weakening and made use of satisfiability results to work in this area. We also implemented a satisfiability checker for the LTL computational logic. The point to be noted here is that the entire process of computing coverage, weakening, and reporting uncovered portions is meant to automated.

1. Rajeev Kumar, Prajna P. Parida and Mohit Gupta, "Topological Design of Communication Networks using Multiobjective Genetic Optimization",  in Proceedings of the 2002 IEEE Congress on Evolutionary Computation CEC2002, pp 425-430, Hawaii, 12-17 May 2002.

2. Prajna Prakash Parida and Mohit Gupta,  "Topological Design of Communication Networks using Multiobjective Genetic Optimization",  dissertation for Bachelor of Technology (Honors) in Computer Science and Engineering, IIT Kharagpur, May 2002.

3. Prajna Prakash Parida,  "A Case Study in Discrete Controller Synthesis: from Specification to Graphical Simulation", Training Report, INRIA Rhone-Alpes, France, July 2001.

4. Herve Marchand, Prajna Prakash Parida and Eric Rutten,  "Discrete Controller Synthesis Made Easy: A User's Manual for  Sigali",  INRIA Technical Report (Rapport de Recherche), INRIA Rhone-Alpes, France, 2002.