Current Preprints

The following are preprints of papers I worked on so far in my time at the KSL. More on verification for physical systems is in the works...


Safety Verification Proofs for Physical Systems Tony Loeser, Yumi Iwasaki, and Richard Fikes. Accepted for QR-98.
(KSL technical report KSL-98-14)

Abstract: While much progress has been made in verification of discrete systems such as computer programs, work on formal verification of continuous, physical systems has been limited. We present a technique for verification of safety properties of such systems. Our algorithm treats safety as a reachability problem, and attempts to prove that a system cannot evolve from an abstract initial state into a state in which the safety condition does not hold. This approach is inspired by qualitative simulation techniques and makes use of trajectories comprised of a sequence of qualitative states and state transitions. The applicability of the technique, however, is not limited to qualitative problems, as we can use any amount of quantitative math in the system description. This paper describes the technique, presents example problems, and discusses its limitations as well as potential for use in device engineering.


Thoughts on a Practical Theory of Reformulation for Reasoning About Physical Systems Yumi Iwasaki, Berthe Choueiry, Sheila McIlraith, Tony Loeser, Todd Neller, Robert Engelmore, and Richard Fikes. Accepted for SARA-98.

Abstract: In this paper, we propose a practical framework for characterizing, evaluating and selecting reformulation techniques for reasoning about physical systems, with the long-term goal of automating the selection and application of these techniques. We view reformulation as a mapping from one encoding of a problem to another. A problem solving task is in turn accomplished by the application of a sequence of reformulations to an inital problem encoding to produce a final encoding that addresses the task. Our framework provides the terminology to specify the conditions under which a particular reformulation technique is applicable, the cost associated with performing the reformulation, and the effects of the reformulation with respect to the problem encoding. As such it provides the vocabulary to characterize the selection of a sequence of reformulation techniques as a planning problem. Our framework is sufficiently flexible to accommodate previously proposed properties and metrics for reformulation. We have used the framework to characterize a variety of reformulation techniques, three of which are presented in this paper.

Back to publications

Back to home