TY - GEN
T1 - Verifying tolerant systems using polynomial approximations
AU - Prabhakar, Pavithra
AU - Vladimerou, Vladimeros
AU - Viswanathan, Mahesh
AU - Dullerud, Geir E.
PY - 2009
Y1 - 2009
N2 - In this paper, we approximate a hybrid system with arbitrary flow functions by systems with polynomial flows; the verification of certain properties in systems with polynomial flows can be reduced to the first order theory of reals, and is therefore decidable. The polynomial approximations that we construct ε-simulate (as opposed to "simulate") the original system, and at the same time are tight. We show that for systems that we call tolerant, safety verification of a system can be reduced to the safety verification of the polynomial approximation. Our main technical tool in proving this result is a logical characterization of ε-simulations. We demonstrate the construction of the polynomial approximation, as well as the verification process, by applying it to an example protocol in air traffic coordination.
AB - In this paper, we approximate a hybrid system with arbitrary flow functions by systems with polynomial flows; the verification of certain properties in systems with polynomial flows can be reduced to the first order theory of reals, and is therefore decidable. The polynomial approximations that we construct ε-simulate (as opposed to "simulate") the original system, and at the same time are tight. We show that for systems that we call tolerant, safety verification of a system can be reduced to the safety verification of the polynomial approximation. Our main technical tool in proving this result is a logical characterization of ε-simulations. We demonstrate the construction of the polynomial approximation, as well as the verification process, by applying it to an example protocol in air traffic coordination.
KW - Approximation
KW - Hybrid automata
KW - Hybrid systems
KW - Logical characterization
KW - ε-simulation
UR - http://www.scopus.com/inward/record.url?scp=77649326306&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77649326306&partnerID=8YFLogxK
U2 - 10.1109/RTSS.2009.28
DO - 10.1109/RTSS.2009.28
M3 - Conference contribution
AN - SCOPUS:77649326306
SN - 9780769538754
T3 - Proceedings - Real-Time Systems Symposium
SP - 181
EP - 190
BT - Proceedings - Real-Time Systems Symposium, RTSS 2009
T2 - Real-Time Systems Symposium, RTSS 2009
Y2 - 1 December 2009 through 4 December 2009
ER -