I am a software developer actively working in Model Checking & Applied-Machine Learning research areas. I have about 3 years of experience in developing data warehousing(DWH) application. As an ETL developer, I integrated data from client's acquisitions and partners to their DWH. This requires mapping business and technical requirements with the ETL process.
To pursue my research interest in software development and applied Machine Learning, I started Master's degree in Computer Science at Iowa State University. It becomes quite interesting when I solve optimisation problems in my formal methods and verification lab by tweaking appropriate data structure and algorithms and on the other hand, gains knowledge in applied machine learning by exploring vast applications of it. The balance between two broad areas widens my perspective of approaching a problem.
In last one year, I have successfully coded two projects using machine learning algorithms. The first project was on parallelising the parametric K-Nearest Neighbours(k-NNs) Algorithm to study its performance against serial version of the algorithm. This project helped me to learn about the application of theoretical machine Learning in high-performance computing. The second project was on creating a GENERATIVE CHATBOT: "GARRULA" application implementing DEEP LEARNING techniques.
Along with studies, I love to RUN a lot. It keeps me motivated and energetic throughout the day. Recently, I have finished IMT Des Moines Half Marathon 2016 in 1:48:14 and a 4K run organised by Computer Science department at Iowa State University in 15:56.
Currently, I am working in the field of Model Checking & Verification and interested in developing the application for MEDDLY(Multi-terminal and Edge-valued Decision Diagram LibrarY) designed by Dr. Andrew Miner.
Model checking is the process of determining whether a system, described as a Non-deterministic model, satisfies some properties. We can write these properties formally using temporal logics , LTL / CTL. If the model is described by a finite state machine, then the model checking problem is decidable. In practice, the implementation of such models as finite state machines can be extremely large. This problem is known as “State space explosion” . This problem can be solved through Symbolic Techniques , which are using a data structure called Decision Diagrams(DD). These techniques focus on generating compact model representations of a high-level description of a system. In Practice, These systems are typically modeled using structured, high-level specification formalism such as Petri-nets and process algebras. MEDDLY is a C++ library that natively supports various types of DDs, including BDDs, MDDs, MTMDDs, EV+MDDs, and EV*MDDs.
To get a more intuitive sense of our work, I will explain with an example of Rubik’s Cube. To generate the whole state space using decision diagrams for a model of Rubic’s cube takes up 1019 states with a good variable ordering(May go worse if selects a bad ordering/permutation). The decision diagrams are susceptible to variable orderings. At an abstract level, we can think of variable ordering to be a set of variables that represents states in DDs. A permutation of this set can cause a DD to be huge or small. So, one has to come up with a heuristic that can yield a best variable order for a model (NP-hard problem ). The state space generation is done through an algorithm called “SATURATION” which is many orders of magnitude more efficient in terms of memory and time with respect to traditional method in generating full state space of a model. To generate a state space, saturation algorithm uses MEDDLY as a Decision Diagram library.
The current statistics for full state space generation of Rubik's Cube model takes ~4 Hours and a peak memory (RAM) ~19GB.
Our Lab’s Goal: Is to reduce the peak memory (RAM) consumption to ~4Gb (so that we can run it on a desktop machine). This will help us to solve many real-world problems.
I am currently working on optimizing MEDDLY’s code to make it more space efficient by tweaking appropriate Data Structures and algorithms implemented in it.
Kamal Kumar Poptani Manager Vodafone India Services Pvt. LTD.,Pune Area, India Voice:(India)+91-8888845948 | (UK) +447448574241 E-mail: Kamal.email@example.com
Andrew S.Miner Associate Professor Department of Computer Science Iowa State University Ames, Iowa 50011-1041, USA Voice: +1-515-294-2392 E-mail:firstname.lastname@example.org
Gianfranco Ciardo Professor and Chair Department of Computer Science Iowa State University Ames, Iowa 50011-1041, USA Voice: +1-515-294-3264 E-mail email@example.com
Samik Basu Professor Department of Computer Science Iowa State University Ames, Iowa 50011-1041, USA Voice: +1-515-294-6045 E-mail: firstname.lastname@example.org