Reachability Analysis Using Extremal Rates

详细信息    查看全文

• 作者：Andrew N. Fisher (16)
  Chris J. Myers (16)
  Peng Li (17)
  
  16. University of Utah ; Salt Lake City ; UT ; 84112 ; USA
  17. Texas A&M University ; College Station ; TX ; 77843 ; USA
  
• 关键词：Range of rates ; LPNs ; Zones ; Difference bound matrices
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9058
• 期：1
• 页码：158-172
• 全文大小：282 KB
• 参考文献：1. Alur, R, Courcoubetis, C, Halbwachs, N, Henzinger, TA, Ho, PH, Nicollin, X, Olivero, A, Sifakis, J, Yovine, S (1995) The algorithmic analysis of hybrid systems. Theoretical Computer Science 138: pp. 3-34 CrossRef
  2. Alur, R, Courcoubeti, C, Henzinger, TA, Ho, PH Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, RL, Nerode, A, Ravn, AP, Rischel, H eds. (1993) Hybrid Systems. Springer, Heidelberg, pp. 209-229 CrossRef
  3. Asarin, E, Dang, T, Maler, O The $$\mathbf{d/dt}$$ tool for verification of hybrid systems. In: Brinksma, E, Larsen, KG eds. (2002) Computer Aided Verification. Springer, Heidelberg, pp. 365-370 CrossRef
  4. Bengtsson, JE, Yi, W Timed Automata: Semantics, Algorithms and Tools. In: Desel, J, Reisig, W, Rozenberg, G eds. (2004) Lectures on Concurrency and Petri Nets. Springer, Heidelberg, pp. 87-124 CrossRef
  5. Cassez, F, Larsen, KG The impressive power of stopwatches. In: Palamidessi, C eds. (2000) CONCUR 2000 - Concurrency Theory. Springer, Heidelbergpp. 138 CrossRef
  6. Dill, DL Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J eds. (1990) Automatic Verification Methods for Finite State Systems. Springer, Heidelberg, pp. 197-212 CrossRef
  7. Fisher, A.N., Myers, C.J., Li, P.: Ranges of rates (2013) [Online; accessed 31-December-2014]. http://www.async.ece.utah.edu/~andrewf/ranges_of_rates.pdf
  8. Frehse, G, Guernic, C, Donz茅, A, Cotton, S, Ray, R, Lebeltel, O, Ripado, R, Girard, A, Dang, T, Maler, O SpaceEx: Scalable verification of hybrid systems. In: Gopalakrishnan, G, Qadeer, S eds. (2011) Computer Aided Verification. Springer, Heidelberg, pp. 379-395 CrossRef
  9. Frehse, G., Krogh, B., Rutenbar, R.: Verifying analog oscillator circuits using forward/backward abstraction refinement. In: DATE 2006 Proceedings of the Design, Automation and Test in Europe, vol. 1, p. 6, March 2006
  10. Frehse, G.: Spaceex (2012) [Online; accessed 31-December-2012]. http://spaceex.imag.fr/documentation/publications
  11. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What鈥檚 decidable about hybrid automata? In: Symposium on Theory of Computing, pp. 373鈥?82. Association for Computing Machinery (1995). http://dl.acm.org/citation.cfm?id=225162
  12. Little, S, Seegmiller, N, Walter, D, Myers, C, Yoneda, T (2011) Verification of analog/mixed-signal circuits using labeled hybrid petri nets. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 30: pp. 617-630 CrossRef
  13. Little, S, Walter, D, Jones, K, Myers, C, Sen, A (2010) Analog/mixed-signal circuit verification using models generated from simulation traces. The Inernational Journal of Foundations of Computer Science 21: pp. 191-210 CrossRef
  14. Little, S.R.: Efficient modeling and verification of analog/mixed-signal circuits using labeled hybrid petri nets. Ph.D. thesis, University of Utah (2008)
  15. Myers, C.: Asynchronous Circuit Design. John Wiley & Sons, July 2001
  16. Puri, A, Borkar, V, Varaiya, P $$\epsilon $$ -approximation of differential inclusions. In: Alur, R, Sontag, ED, Henzinger, TA eds. (1996) Hybrid Systems III. Springer, Heidelberg CrossRef
  17. Silva, BI, Krogh, BH (2000) Formal verification of hybrid systems using checkmate: A case study. American Control Conference 3: pp. 1679-1683
  18. Yan, C., Greenstreet, M.: Faster projection based methods for circuit level verification. In: ASPDAC 2008 Design Automation Conference, Asia and South Pacific, pp. 410鈥?15 (2008)
  
• 作者单位：NASA Formal Methods
• 丛书名：978-3-319-17523-2
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

General hybrid systems can be difficult to verify due to their generality. To reduce the complexity, one often specializes to hybrid systems where the complexity is more manageable. If one reduces the modeling formalism to ones where the continuous variables have a single rate, then it may be possible to use the methods of zones to find the reachable state space. Zones are a restricted class of polyhedra formed by considering the intersections of half-planes defined by two variable constraints. Due to their simplicity, zones have simpler, more efficient methods of manipulation than more general polyhedral classes, though they are less accurate. This paper extends the method of zones to labeled Petri net (LPN) models with continuous variables that evolve over a range of rates.