Verification of cooperating traffic agents

References

• Alur , R , Courcoubetis , C , Henzinger , TA and Pei-Hsin Ho . 1992 . “ Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems ” . In Hybrid Systems , Edited by: Grossman , RL , Nerode , A , Ravn , AP and Rischel , H . 209 – 229 . Berlin, Heidelberg : Springer-Verlag . Volume 736 of LNCS
   Google Scholar
• Bohn , J , Damm , W , Grumberg , O , Hungar , H and Laster , K . 1998 . “ First-order CTL model checking ” . In 18th Conf. on Foundations of Software Technology and Theoretical Comp. Sc. , Edited by: Arvind , V and Ramanujam , R . 283 – 294 . Berlin, Heidelberg : Springer-Verlag . Volume 1530 of LNCS
   Google Scholar
• Bohn , J , Damm , W , Klose , J , Moik , A and Wittke , H . 2002 . Modelling and validating train system applications using statemate and live sequence charts
   Google Scholar
• Damm , W , Hungar , H and Olderog , E-R . 2004 . “ On the verification of cooperating traffic agents ” . In FMCO 2003: Formal Methods for Components and Objects, Volume 3188 of LNCS , Edited by: de Boer , FS , Bonsangue , MM , Graf , S and de Roever , W-P . 77 – 110 . Berlin, Heidelberg : Springer-Verlag .
   Google Scholar
• Damm , W , Pinto , G and Ratschan , S . 2005 . “ Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems ” . In Proceedings of the Third Intern. Symposium on Automated Technology for Verification and Analysis, Volume 3707 of LNCS , 99 – 113 . Berlin, Heidelberg : Springer-Verlag .
   Google Scholar
• Ganzinger , H , Sofronie-Stokkermans , V and Waldmann , U . 2004 . “ Modular proof systems for partial functions with weak equality ” . In Automated reasoning: Second Intern. Joint Conference, IJCAR 2004, Volume 3097 of LNAI , Edited by: Basin , D and Rusinowitch , M . 168 – 182 . Berlin, Heidelberg : Springer-Verlag .
   Google Scholar
• Haxthausen , AE and Peleska , J . 2000 . Formal development and verification of a distributed railway control system . IEEE Transactions on Software Engineering , 26 : 687 – 701 .
   Google Scholar
• Hoenicke , J and Olderog , E-R . 2002 . “ CSP-OZ-DC: a combination of specification techniques for processes, data and time ” . In Nordic Journal of Computing Vol. 9 , 301 – 334 . (appeared March 2003)
   Google Scholar
• Hu , A , Eskafi , F , Sachs , S and Varaiya , P . 1991 . The design of platoon manoeuvre protocols for IVHS Technical Report UCB-ITS-PRR-91-6, Insitute of Transportation Studies, Univ. of California at Berkeley
   Google Scholar
• Hu , T and Lin , Z . 2000 . On enlarging the basin of attraction for linear systems under saturated linear feedback . Systems and Control Letters , 40 : 59 – 69 .
   Web of Science ®Google Scholar
• Johansson , M and Rantzer , A . 1998 . Computation of piecewise quadratic Lyapunov functions for hybrid systems . IEEE Transactions on Automatic Control , 43 : 555 – 559 .
   Web of Science ®Google Scholar
• Kalman , RE and Bertram , JE . 1960 . Control system analysis and system design via the second method of Lyapunov – Part I: continuous time systems . Transactions of the ASME, Journal of Basic Engineering , 82 : 371 – 393 .
   Google Scholar
• Kuehlmann , A , Ganai , MK and Paruthi , V . 2001 . “ Circuit-based boolean reasoning ” . In DAC '01: Proceedings of the 38th Conference on Design Automation , 232 – 237 . New York, NY, , USA : ACM Press .
   Google Scholar
• Kuehlmann , A , Paruthi , V , Krohm , F and Gana , MK . 2002 . Robust boolean reasoning for equivalence checking and functional property verification . IEEE Trans. CAD , 21 : 1377 – 1394 .
   Google Scholar
• Larsen , KG , Petterson , P and Wang Yi . 1997 . Uppaal in a nutshell . Intern. Journal on Software Tools for Technology Transfer , 1 : 134 – 152 .
   Google Scholar
• Leveson , NG . 1995 . Safeware: System Safety and Computers , Reading, Massachusets : Addison Wesley .
   Google Scholar
• Livadas , C , Lygeros , J and Lynch , NA . 2000 . High-level modelling and analysis of TCAS . Proceedings of IEEE Special Issue on Hybrid Systems: Theory & Applications , 88 : 926 – 947 .
   Google Scholar
• Lygeros , J , Godbole , DN and Sastry , SS . 1997 . A design framework for hierarchical, hybrid control Technical Report UCB-ITS-PRR-97-24, California Partners for Advanced Transit and Highways (PATH), University of California at Berkeley, Jan. http://repositories.cdlib.org/its/path/reports/UCBITS-PRR-97-24
   Google Scholar
• Lygeros , J , Godbole , DN and Sastry , SS . 1998 . Verified hybrid controllers for automated vehicles . IEEE Transactions on Automatic Control , 43 : 522 – 539 .
   Web of Science ®Google Scholar
• Lynch , NA , Segala , R and Vaandrager , F . 2003 . Hybrid I/O automata . Inform. and Comp. , 185 : 105 – 157 .
   Web of Science ®Google Scholar
• Oehlerking , J , Burchardt , H and Theel , O . 2005 . Towards automatic verification of affine hybrid system stability SIGBED Review, Special Issue on IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS, 2, Available on line: http://www.cs.virginia.edu/sigbed/archives/2005-04/wip7.pdf
   Google Scholar
• Pettersson , S . 1999 . “ Analysis and design of hybrid systems ” . In PhD thesis , Gothenburg : Chalmers Univ. of Technology .
   Google Scholar
• Ravn , AP . 1995 . Design of embedded real-time computing systems Technical Report ID-TR: 1995-170, Thesis for Doctor of Technics, Tech. Univ. Denmark
   Google Scholar
• Sofronie-Stokkermans , V . 2005 . “ Hierarchic reasoning in local theory extensions ” . In CADE-20 – The 20th Intern. Conference on Automated Deduction, volume 3632 of LNAI , Edited by: Nieuwenhuis , R . 219 – 234 . Berlin, Heidelberg : Springer-Verlag .
   Google Scholar
• Theel , O . June 2005 . Private communication
   Google Scholar
• Tiwari , A . 2003 . “ Approximate reachability for linear systems ” . In Hybrid Systems: Computation and Control, volume 2623 of LNCS , Edited by: Maler , O and Pnueli , A . 514 – 525 . Berlin, Heidelberg : Springer-Verlag .
   Google Scholar
• Tomlin , C , Pappas , G and Sastry , SS . April 1998 . Confiict resolution for air traffic management: a case study in multi-agent hybrid systems . IEEE Transactions on Automatic Control , 43 : 509 – 521 .
   Web of Science ®Google Scholar
• Tomlin , C , Lygeros , J and Sastry , SS . 2000 . A game theoretic approach to controller design for hybrid systems . Proceedings of the IEEE , 88 : 949 – 970 .
   Web of Science ®Google Scholar
• Zhou , C and Hansen , MR . 2004 . Duration Calculus: A Formal Approach to Real-Time Systems , Berlin, Heidelberg : Springer-Verlag .
   Google Scholar
• Zhou , C , Hoare , CAR and Ravn , AP . 1991 . A calculus of durations . IPL , 40 : 269 – 276 .
   Web of Science ®Google Scholar