Courtesy of Don Goelman, Ph.D., and Tom Way, Ph.D.
Department of Computing Sciences

Computer Science Student Solves Open Problem in Computability Logic

In the course of working on his graduate thesis in Computer Science, Matt Bauer ’12 solved an open problem in Computability Logic: that the basic first-order fragment of Computability Logic is PSPACE-complete. The non-trivial proof  for this theorem was found by him independently, without any help from his advisor. The paper is presented in "A PSPACE-complete First-Order Fragment of Computability Logic," which is under review for publication.

The focus of his research was at the intersection of mathematical logic and theoretical computer science. Specifically, he worked within the framework of "Computability Logic," a research line introduced by Professor Giorgi Japaridze of the Department of Computing Sciences in 2003 that has been extensively studied worldwide during recent years. The aim of Computability Logic is to redevelop logic as a systematic formal tool for characterizing "computability," as opposed to the more traditional understanding of logic as a tool for characterizing "truth."

Matt demonstrated that deciding validity for the basic first-order fragment of Computability Logic is PSPACE-complete, which had been an open problem since 2006. The significance of this result is that it concretely establishes how difficult it is for a machine to determine if a formula in Computability Logic is valid or not. Matt intends to continue working in this area and tackle new problems during the summer, thanks to a research fellowship from Villanova.

Computer Science Professor and Graduate Student Participate in 2012 Spring Simulation Multi-Conference

Professor Vijay Gehlot of the Department of Computing Sciences together with graduate student Carmen Nigro, will present their research paper, “Modeling and Simulation of a Re-entrant Manufacturing System Using Colored Petri Nets,” at the 45th Annual Simulation Symposium (part of the 2012 Spring Simulation Multi-conference) in late March. The paper describes the use of Colored Petri Nets in the simulation and analysis of re-entrant manufacturing systems with inspections. Colored Petri Nets provide a powerful modeling framework for simulating manufacturing systems, because they allow for distributed and concurrent processes with both synchronous and asynchronous communication. Inspection stations in a manufacturing system are designed to enhance product quality and process performance. An example is the semiconductor manufacturing process, especially the wafer fabrication line, which is composed of many repeated sequential processes used to produce electrical circuits. A reentrant manufacturing system with inspections allows a specimen that has failed an inspection to reenter the system at a previous work stage. Reentrancy is also a crucial property of non-manufacturing systems, such as in the blood samples matching process.

The Colored Petri Nets modeling framework allows investigation of the system before it is constructed in order to reduce errors and maximize efficiency. Competitive pressures are influencing manufacturers to place greater focus on the customer in producing high quality products at reduced product lead times. The increased focus on quality and efficiency has increased the importance of inspection stations throughout the manufacturing process.

Computing Sciences Professor Selected to Attend 24th Winter Workshop on Computational Geometry at Bellairs Research Institute

During the third week of February 2012, Professor Mirela Damian, Ph.D., of the Department of Computing Sciences, joined a selected group of researchers at the 24th winter workshop on Computational Geometry at Bellairs Research Institute of McGill University in Holetown, West Indies. Twenty researchers from six countries spent a week working together on self-assembly: arranging geometric parts so that they come together by themselves. The theoretical models used in their work have been implemented in real biological systems using DNA tiles, which allow controlled manufacture of precise geometric objects at nanometer resolution (nanomanufacture). The research group also investigated the dynamics of protein folding, seeking to determine how proteins consistently fold into a stable state.  Such an understanding would greatly influence many areas in biology and medicine, such as drug design.