Temporal precedence checking for switched models and its application to a parallel landing protocol

Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan, César Muñoz

Research output: Chapter in Book/Report/Conference proceedingConference contribution


This paper presents an algorithm for checking temporal precedence properties of nonlinear switched systems. This class of properties subsume bounded safety and capture requirements about visiting a sequence of predicates within given time intervals. The algorithm handles nonlinear predicates that arise from dynamics-based predictions used in alerting protocols for state-of-the-art transportation systems. It is sound and complete for nonlinear switch systems that robustly satisfy the given property. The algorithm is implemented in the Compare Execute Check Engine (C2E2) using validated simulations. As a case study, a simplified model of an alerting system for closely spaced parallel runways is considered. The proposed approach is applied to this model to check safety properties of the alerting logic for different operating conditions such as initial velocities, bank angles, aircraft longitudinal separation, and runway separation.

Original languageEnglish (US)
Title of host publicationFM 2014
Subtitle of host publicationFormal Methods - 19th International Symposium, Proceedings
PublisherSpringer-Verlag Berlin Heidelberg
Number of pages15
ISBN (Print)9783319064093
StatePublished - 2014
Event19th International Symposium on Formal Methods, FM 2014 - Singapore, Singapore
Duration: May 12 2014May 16 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8442 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other19th International Symposium on Formal Methods, FM 2014

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Temporal precedence checking for switched models and its application to a parallel landing protocol'. Together they form a unique fingerprint.

Cite this