https://www.scipedia.com/wd/index.php?action=history&feed=atom&title=Platzer_Clarke_2018a 2026-04-22T01:24:05Z Revision history for this page on the wiki MediaWiki 1.27.0-wmf.10 https://www.scipedia.com/wd/index.php?title=Platzer_Clarke_2018a&diff=176095&oldid=prev 2020-10-14T14:28:20Z

<p>Scipediacontent moved page <a href="/public/Draft_Content_944654520" class="mw-redirect" title="Draft Content 944654520">Draft Content 944654520</a> to <a href="/public/Platzer_Clarke_2018a" title="Platzer Clarke 2018a">Platzer Clarke 2018a</a></p> <table class="diff diff-contentalign-left" data-mw="interface"> <tr style='vertical-align: top;' lang='en'> <td colspan='1' style="background-color: white; color:black; text-align: center;">← Older revision</td> <td colspan='1' style="background-color: white; color:black; text-align: center;">Revision as of 14:28, 14 October 2020</td> </tr><tr><td colspan='2' style='text-align: center;' lang='en'><div class="mw-diff-empty">(No difference)</div> </td></tr></table>

Scipediacontent https://www.scipedia.com/wd/index.php?title=Platzer_Clarke_2018a&diff=176094&oldid=prev 2020-10-14T14:28:18Z

<p>Created page with &quot; == Abstract == Aircraft collision avoidance maneuvers are important and complex applications. Curved flight exhibits nontrivial continuous behavior. In combination with the...&quot;</p> <p><b>New page</b></p><div><br /> == Abstract ==<br /> <br /> Aircraft collision avoidance maneuvers are important and complex applications. Curved flight exhibits nontrivial continuous behavior. In combination with the control choices during air traffic maneuvers, this yields hybrid systems with challenging interactions of discrete and continuous dynamics. As a case study illustrating the use of a new proof assistant for a logic for nonlinear hybrid systems, we analyze collision freedom of roundabout maneuvers in air traffic control, where appropriate curved flight, good timing, and compatible maneuvering are crucial for guaranteeing safe spatial separation of aircraft throughout their flight. We show that formal verification of hybrid systems can scale to curved flight maneuvers required in aircraft control applications. We introduce a fully flyable variant of the roundabout collision avoidance maneuver and verify safety properties by compositional verification.<br /> <br /> Document type: Part of book or chapter of book<br /> <br /> == Full document ==<br /> &lt;pdf&gt;Media:Draft_Content_944654520-beopen1018-1729-document.pdf&lt;/pdf&gt;<br /> <br /> <br /> == Original document ==<br /> <br /> The different versions of the original document can be found in:<br /> <br /> * [http://dx.doi.org/10.1007/978-3-642-05089-3_35 http://dx.doi.org/10.1007/978-3-642-05089-3_35]<br /> <br /> * [http://dx.doi.org/10.1184/r1/6605798 http://dx.doi.org/10.1184/r1/6605798]<br /> <br /> * [http://dx.doi.org/10.1184/r1/6605798.v1 http://dx.doi.org/10.1184/r1/6605798.v1]<br /> <br /> * [http://reports-archive.adm.cs.cmu.edu/anon/2009/CMU-CS-09-147.pdf http://reports-archive.adm.cs.cmu.edu/anon/2009/CMU-CS-09-147.pdf]<br /> <br /> <br /> <br /> DOIS: 10.1007/978-3-642-05089-3_35 10.1184/r1/6605798.v1 10.1184/r1/6605798</div>

Scipediacontent