Citation
Susmit Jha, Bryan Brady, Sanjit Seshia. "Symbolic Reachability Analysis of Lazy Linear Hybrid Automata". Talk or presentation, 4, September, 2007.

Abstract
Lazy linear hybrid automata (LLHA) model the discrete time behavior of control systems containing finite-precision sensors and actuators interacting with their environment under bounded inertial delays. We present a symbolic technique for reachability analysis of lazy linear hybrid automata. The model permits invariants and guards to be nonlinear predicates but requires flow values to be a finite set of constants. Assuming finite precision, flows represented by uniform linear predicates can be reduced to those containing values from a finite set of constants. We present an abstraction hierarchy for LLHA. Our verification technique is based on bounded model checking and k-induction for reachability analysis at different levels of the abstraction hierarchy within an abstraction-refinement framework. The counterexamples obtained during BMC are used to construct refinements in each iteration. This technique has been tested on some examples that include Highway Control System and we found that it scales well compared to other tools like Phaver.

Electronic downloads

• jha_CHESS.pdf · · 429 kbytes

• HTML

  Susmit Jha, Bryan Brady, Sanjit Seshia. <a
  href="http://chess.eecs.berkeley.edu/pubs/351.html"
  ><i>Symbolic Reachability Analysis of Lazy Linear
  Hybrid Automata</i></a>, Talk or presentation, 
  4, September, 2007.

• Plain text

  Susmit Jha, Bryan Brady, Sanjit Seshia. "Symbolic
  Reachability Analysis of Lazy Linear Hybrid Automata".
  Talk or presentation,  4, September, 2007.

• BibTeX

  @presentation{JhaBradySeshia07_SymbolicReachabilityAnalysisOfLazyLinearHybridAutomata,
      author = {Susmit Jha and Bryan Brady and Sanjit Seshia},
      title = {Symbolic Reachability Analysis of Lazy Linear
                Hybrid Automata},
      day = {4},
      month = {September},
      year = {2007},
      abstract = {Lazy linear hybrid automata (LLHA) model the
                discrete time behavior of control systems
                containing finite-precision sensors and actuators
                interacting with their environment under bounded
                inertial delays. We present a symbolic technique
                for reachability analysis of lazy linear hybrid
                automata. The model permits invariants and guards
                to be nonlinear predicates but requires flow
                values to be a finite set of constants. Assuming
                finite precision, flows represented by uniform
                linear predicates can be reduced to those
                containing values from a finite set of constants.
                We present an abstraction hierarchy for LLHA. Our
                verification technique is based on bounded model
                checking and k-induction for reachability analysis
                at different levels of the abstraction hierarchy
                within an abstraction-refinement framework. The
                counterexamples obtained during BMC are used to
                construct refinements in each iteration. This
                technique has been tested on some examples that
                include Highway Control System and we found that
                it scales well compared to other tools like Phaver.},
      URL = {http://chess.eecs.berkeley.edu/pubs/351.html}
  }
  

Posted by Douglas Densmore on 10 Oct 2007.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.