{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:09:33Z","timestamp":1761487773343},"reference-count":21,"publisher":"World Scientific Pub Co Pte Lt","issue":"01","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2007,2]]},"abstract":"<jats:p>We present a novel approach to the automatic verification and falsification of LTL requirements of non-linear discrete-time hybrid systems. The verification tool uses an interval-based constraint solver for non-linear robust constraints to compute incrementally refined abstractions. Although the problem is in general undecidable, we prove termination of abstraction refinement based verification and falsification of such properties for the class of non-linear robust discrete-time hybrid systems. We argue, that\u2014in industrial practice\u2014safety critical control applications give rise to hybrid systems that are robust. We give first results on the application of this approach to a variant of an aircraft collision avoidance protocol.<\/jats:p>","DOI":"10.1142\/s0129054107004577","type":"journal-article","created":{"date-parts":[[2007,2,7]],"date-time":"2007-02-07T12:42:34Z","timestamp":1170852154000},"page":"63-86","source":"Crossref","is-referenced-by-count":20,"title":["GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS"],"prefix":"10.1142","volume":"18","author":[{"given":"WERNER","family":"DAMM","sequence":"first","affiliation":[{"name":"Department f\u00fcr Informatik, Carl v. Ossietzky Universit\u00e4t Oldenburg, 26111 Oldenburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"GUILHERME","family":"PINTO","sequence":"additional","affiliation":[{"name":"Department f\u00fcr Informatik, Carl v. Ossietzky Universit\u00e4t Oldenburg, 26111 Oldenburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"STEFAN","family":"RATSCHAN","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, Czech Academy of Sciences, Pod Vodarenskou v\u011b\u017e\u00ed 2, 182 07 Praha 8, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_4"},{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_4"},{"key":"rf4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48092-7_14"},{"key":"rf7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-49382-2_27"},{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410300190X"},{"key":"rf12","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"rf13","volume-title":"Model Checking","author":"Clarke Edmund M.","year":"1999"},{"key":"rf14","doi-asserted-by":"publisher","DOI":"10.1080\/00207170600587531"},{"key":"rf17","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_22"},{"key":"rf18","doi-asserted-by":"publisher","DOI":"10.1109\/9.664156"},{"key":"rf20","doi-asserted-by":"publisher","DOI":"10.1007\/11730637"},{"key":"rf21","volume-title":"Applied Interval Analysis, with Examples in Parameter and State Estimation, Robust Control and Robotics","author":"Jaulin Luc","year":"2001"},{"key":"rf22","volume-title":"The Control Handbook","author":"Levine W. S.","year":"1995"},{"key":"rf23","doi-asserted-by":"publisher","DOI":"10.1007\/b106766"},{"key":"rf24","volume-title":"Interval Methods for Systems of Equations","author":"Neumaier Arnold","year":"1990"},{"key":"rf26","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0519"},{"key":"rf29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_37"},{"key":"rf31","doi-asserted-by":"publisher","DOI":"10.1076\/1387-3954(200003)6:1;1-Q;FT051"},{"key":"rf32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36580-X_36"},{"key":"rf33","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"Tarski A.","year":"1951"},{"key":"rf34","volume":"43","author":"Tomlin Claire","journal-title":"IEEE Transactions on Automatic Control"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054107004577","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,8]],"date-time":"2021-08-08T13:10:50Z","timestamp":1628428250000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054107004577"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2]]},"references-count":21,"journal-issue":{"issue":"01","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2007,2]]}},"alternative-id":["10.1142\/S0129054107004577"],"URL":"https:\/\/doi.org\/10.1142\/s0129054107004577","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2]]}}}