Arjun Kapur 

	        PhD, 1997
		Department of Computer Science
		Stanford University

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

Contents

  • Research
  • The STeP Project (The Stanford Temporal Prover): A system for computer-aided formal verification of concurrent and reactive systems based on temporal specifications.
  • Graduate Student Pointers: My personal guide to various resources for graduate students (entertainment, food, web sites, etc,).
  • Worldwide Indian Network (WIN): An international network of Asian Indians working on a variety of projects.
  • India related stuff: Internet resources pertaining to the Asian Indian community.
  • The Lost Generation: Kamlesh Kapur's latest novel exploring the causes of drug abuse, set in the context of a cross cultural love story.

    • Research

     I am currently investigating verification techniques for hybrid systems. Hybrid systems are real-time systems that allow continuous state changes as well as discrete state changes. Ubiquitous examples of hybrid systems appear in nature, since all analog physical phenomena, typically modeled by differential equations, that interact with digital devices, usually modeled by finite automata, can be regarded as hybrid systems.

    In a joint paper with Tom Henzinger, Zohar Manna, and Amir Pnueli, we investigate the verification of safety properties using HTL, a hybrid temporal logic.

    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.
    Abstract only
    Cornell University Technical Report TR94-1459

    In a joint paper with Luca de Alfaro and Zohar Manna, we investigate the verification of both safety and progress properties (as represented in standard temporal logic) using hybrid diagrams.

    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.
    Abstract only
    Postscript version of paper (US format)
    Postscript version of paper (A4 format)

    My thesis is now available online: Interval And Point-Based Approaches To Hybrid System Verification. The slides of my talk are also available.

    Abstract
    Hybrid systems are real-time systems consisting of both continuous and discrete components. This thesis presents deductive and diagrammatic methodologies for proving point-based and interval-based properties of hybrid systems, where the hybrid system is modeled in either a sampling semantics or a continuous semantics. Under a sampling semantics the behavior of the system consists of a discrete number of system snapshots, where each snapshot records the state of the system at a particular moment in time. Under a continuous semantics, the system behavior is given by a function mapping each point in time to a system state. Two continuous semantics are studied: a continuous interval semantics, where at any given point in time the system is in a unique state, and a super-dense semantics, where no such requirement is needed.

    We use Linear-time Temporal Logic expressing properties under either a sampling semantics or a super-dense semantics, and we introduce Hybrid Temporal Logic expressing properties under a continuous interval semantics. Linear-time Temporal Logic is useful for expressing point-based, whose validity is dependent on individual states, while Hybrid Temporal Logic is useful for expressing both interval-based properties, whose validity is dependent on intervals of time, and point-based properties.

    Finally, two different verification methodologies are presented: a diagrammatic approach for verifying properties specified in Linear-time Temporal Logic, and a deductive approach for verifying properties specified in Hybrid Temporal Logic.

    The Stanford home page.

    The Computer Science Department home page.

    The Theory Division home page.

    Arjun Kapur
    arjun@CS.Stanford.EDU