RECURSIVE AND BACKWARD REASONING IN THE VERIFICATION ON HYBRID SYSTEMS

Stefan Ratschan, Zhikun She

2008

Abstract

In this paper we introduce two improvements to the method of verification of hybrid systems by constraint propagation based abstraction refinement that we introduced earlier. The first improvement improves the recursive propagation of reachability information over the regions constituting the abstraction, and the second improvement reasons backward from the set of unsafe states, instead of reasoning forward from the set of initial states. Detailed computational experiments document the usefulness of these improvements.

Download


Paper Citation


in Harvard Style

Ratschan S. and She Z. (2008). RECURSIVE AND BACKWARD REASONING IN THE VERIFICATION ON HYBRID SYSTEMS . In Proceedings of the Fifth International Conference on Informatics in Control, Automation and Robotics - Volume 3: ICINCO, ISBN 978-989-8111-32-6, pages 65-71. DOI: 10.5220/0001475500650071

in Bibtex Style

@conference{icinco08,
author={Stefan Ratschan and Zhikun She},
title={RECURSIVE AND BACKWARD REASONING IN THE VERIFICATION ON HYBRID SYSTEMS},
booktitle={Proceedings of the Fifth International Conference on Informatics in Control, Automation and Robotics - Volume 3: ICINCO,},
year={2008},
pages={65-71},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0001475500650071},
isbn={978-989-8111-32-6},
}


in EndNote Style

TY - CONF
JO - Proceedings of the Fifth International Conference on Informatics in Control, Automation and Robotics - Volume 3: ICINCO,
TI - RECURSIVE AND BACKWARD REASONING IN THE VERIFICATION ON HYBRID SYSTEMS
SN - 978-989-8111-32-6
AU - Ratschan S.
AU - She Z.
PY - 2008
SP - 65
EP - 71
DO - 10.5220/0001475500650071