Model-Based Reasoning
Symbolic Model Checking
Formal verification means having a mathematical model of a system, a language for specifying desired properties of the system in a concise, comprehensible and unambiguous way, and a method of proof to verify that the specified properties are satisfied. When the method of proof is carried out substantially by machine, we speak of automatic verification. Symbolic Model Checking deals with methods of automatic verification as applied to computer hardware. The practical motivation for study in this area is the high and increasing cost of correcting design errors in VLSI technologies. There is a growing demand for design methodologies that can yield correct designs on the first fabrication run.
National Aeronautics and Space Administration Workshop on Monitoring and Diagnosis
The First National Aeronautics and Space Administration (NASA) Workshop on Monitoring and Diagnosis was held in Pasadena, California, from 15 to 17 January 1992. The workshop brought together individuals from NASA centers, academia, and aerospace who have a common interest in AI-based approaches to monitoring and diagnosis technology. The workshop was intended to promote familiarity, discussion, and collaboration among the research, development, and user communities.
Integrating Case-Based and Model-Based Reasoning: A Computational Model of Design Problem Solving
My Ph.D. dissertation (Goel 1989) presents a computational model of experience-based design. It first reviews the core issues in experience-based design, for example, (1) the content of a design experience (or case), (2) the internal organization of design cases, (3) the language for indexing the cases, (4) the mechanism for retrieving a case relevant to a given design task, (5) the mechanism for adapting a retrieved design to satisfy the constraints of the design task, (6) the mechanism for evaluating a design against the specification of the design task, (7) the mechanism for redesigning a failed design, (8) the mechanism for acquiring new design knowledge, (9) the mechanism for chunking information about a design into a new case, and (10) the mechanism for storing a new case in memory for potential reuse in the future. It then proposes that decisions about these issues might lie in the designer's comprehension of the designs of artifacts he/she has encountered in the past, that is, in his/her mental models of how the designs achieve the functions and satisfy the constraints of the artifacts.
Integrating Case-Based and Model-Based Reasoning: A Computational Model of Design Problem Solving
My Ph.D. dissertation (Goel 1989) presents a computational model of experience-based design. It first reviews the core issues in experience-based design, for example, (1) the content of a design experience (or case), (2) the internal organization of design cases, (3) the language for indexing the cases, (4) the mechanism for retrieving a case relevant to a given design task, (5) the mechanism for adapting a retrieved design to satisfy the constraints of the design task, (6) the mechanism for evaluating a design against the specification of the design task, (7) the mechanism for redesigning a failed design, (8) the mechanism for acquiring new design knowledge, (9) the mechanism for chunking information about a design into a new case, and (10) the mechanism for storing a new case in memory for potential reuse in the future. It then proposes that decisions about these issues might lie in the designer's comprehension of the designs of artifacts he/she has encountered in the past, that is, in his/her mental models of how the designs achieve the functions and satisfy the constraints of the artifacts.
Readings in Model-based Diagnosis
Observations play a major role in diagnosis. The nature of an observation varies according to the class of the considered system. In static systems, an observation is the value of a variable at a single time point. In dynamic continuous systems, such a value is observed over a time interval. In discrete-event systems, an observation consists of a sequence of temporally ordered events. In any case, what is observed is assumed not to be ambiguous.
A qualitative physics based on confluences
A qualitative physics predicts and explains the behavior of mechanisms in qualitative terms. The goals for the qualitative physics are (1) to be far simpler than the classical physics and yet retain all the important distinctions (e.g., state, oscillation, gain, momentum) without invoking the mathematics of continuously varying quantities and differential equations, (2) to produce causal accounts of physical mechanisms that are easy to understand, and (3) to provide the foundations for commonsense models for the next generation of expert systems. This paper presents a fairly encompassing account of qualitative physics. First, we discuss the general subject of naive physics and some of its methodological considerations. Second, we present a framework for modeling the generic behavior of individual components of a device based on the notions of qualitative differential equations (confluences) and qualitative state.