Arjun Kapur

Affiliations:	Graduate Student
		Department of Computer Science
		Stanford University

Research Interests: Formal Methods, Verification, Hybrid Systems, Reliability, Software Engineering, Temporal Logics


Abstracts

  • Proving Safety Properties of Hybrid Systems
  • Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification

  • Proving Safety Properties of Hybrid Systems

    A. Kapur, T.A. Henzinger, Z. Manna, A. Pnueli

    We propose a methodology for the specification, verification, and design of hybrid systems. The methodology consists of the computational model of Concrete Phase Transition Systems (CPTSs), the specification language of Hybrid Temporal Logic (HTL), the graphical system description language of Hybrid Automata, and a proof system for verifying that hybrid automata satisfy their HTL specifications. The novelty of the approach lies in the continuous-time logic, which allows specification of both point-based and interval-based properties (ie. properties which describe changes over an interval) and provides direct references to derivatives of variables, and in the proof system that supports verification of point-based and interval-based properties. The proof rules demonstrate that sound and convenient induction rules can be established for continuous-time logics. The proof rules are illustrated on several examples.

    Proving Safety Properties of Hybrid Systems
    in Proceedings of the Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, Springer-Verlag, 1994, pp. 431-454.

    Cornell University Technical Report TR94-1459

    Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification

    L. de Alfaro, A. Kapur, Z. Manna

    We present a methodology for the verification of temporal properties of hybrid systems. The methodology is based on the deductive transformation of hybrid diagrams, which represent the system and its properties, and which can be algorithmically checked against the specification. This check either gives a positive answer to the verification problem, or provides guidance for the further transformation of the diagrams. The resulting methodology is complete for quantifier-free linear-time temporal logic.

    Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification
    in 14th Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, Springer-Verlag, 1997.

    Postscript version of paper (US format)
    Postscript version of paper (A4 format)

    The Stanford home page.

    The Computer Science Department home page.

    The Theory Division home page.

    Arjun Kapur's home page.


    Arjun Kapur
    arjun@CS.Stanford.EDU