*banner
 

Symbolic Reachability Analysis of Lazy Linear Hybrid Automata
Susmit Jha, Bryan Brady, Sanjit A. Seshia

Citation
Susmit Jha, Bryan Brady, Sanjit A. 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

Citation formats  
  • HTML
    Susmit Jha, Bryan Brady, Sanjit A. 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 A. 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 A. 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.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

You are not logged in 
©2002-2014 Chess