Lazy linear hybrid automaton

The CorenSearchBot has detected that the contents of this page may have been copied from the following web page:

http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-32.html (Copyvios report)

This may be a potential infringement of the copyright of a third-party. It will soon be reviewed to determine if there are any copyright issues. The content should not be mirrored or otherwise reused until the issue has been resolved.

If this marking was made in error, simply note so on the this article's discussion page.
You can write a new article without infringing material. Note that simply modifying copyrighted text is not sufficient to avoid copyright infringement— it is best to write the article from scratch, using web pages or other publications as sources of facts, but not as sources of sentences or phrases. You may want to begin the article as a "stub".
Or, if you hold the copyright to this text and permit its use under the terms consistent with Wikipedia's policies, please see Wikipedia:Donating copyrighted materials for instructions on how to verify the licensing.
If this text is in the public domain, or is already under a license suitable for Wikipedia, explain this on this article's discussion page, with reference to evidence.

Note: Articles on Wikipedia must be written from a neutral point of view and must be verifiable in published third-party sources; your text may not be appropriate for inclusion in Wikipedia, legal issues aside.

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. In this paper, we present a symbolic technique for reachability analysis of lazy linear hybrid automata. The model permits only linear flow constraints but the invariants and guards can be any computable function.

This model was proposed by Manindar Agrawal (Prime is in P fame) and P. S. Thiagarajan. This model is more realistic and also computationally amenable than the currently popular modeling paradigm of linear hybrid automata.

[1] [2]