# Arjun Kapur

PhD, 1997
Department of Computer Science
Stanford University

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

## Contents

## 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.

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