Exact symbolic models for verification

Paulo Tabuada ()
Additional contact information
Paulo Tabuada: University of California, Los Angeles, Department of Electrical Engineering

Chapter 7 in Verification and Control of Hybrid Systems, 2009, pp 73-111 from Springer

Abstract: Abstract The evolution of physical quantities such as position, temperature, humidity, etc, is usually described by differential equations with solutions evolving on $${\mathbb R}^n$$ or appropriate subsets. The infinite cardinality of $${\mathbb R}^n$$ prevents a direct application of the verification methods described in Chapter 5. However, verification algorithms are still applicable whenever suitable finite-state abstractions of these infinite-state systems can be constructed. In recent years, several methods have been proposed for the construction of these abstractions based on a very interesting blend of different mathematical techniques. We present several of these methods starting with timed automata to illustrate the general principles of the abstraction process. Most of the abstraction techniques described in this chapter require linear differential equations. For this reason, we discuss as a special topic how to transform a class of nonlinear differential equations into linear di_erential equations in larger state spaces.

Keywords: Equivalence Class; Equivalence Relation; Erential Equation; Discrete Transition; Unsafe State (search for similar items in EconPapers)
Date: 2009
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-1-4419-0224-5_7

Ordering information: This item can be ordered from
http://www.springer.com/9781441902245

DOI: 10.1007/978-1-4419-0224-5_7

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().