CALL FOR PAPERS

Formal Methods in Aerospace: Techniques from Logic, Mathematics and AI

A special issue of the journal:

Annals of Mathematics and Artificial Intelligence

[ Deadline: 10th March 2010 ]

PDF version of this Call for Papers

Special Issue editors:

Manuela Bujorianu; Michael Fisher; Corina Pasareanu.

OVERVIEW

The coexistence of multiple disciplinary perspectives on aerospace systems and formalized investigation methods, leads naturally to the opportunity to define multidisciplinary approaches. Thus, work in this area underlines the importance of some research problems from aerospace to the Logic, Mathematics and Artificial Intelligence communities, and promotes new techniques combining the principles from Logic, Artificial Intelligence, Hybrid Systems, Control Engineering, etc. Key to this is the fact that logic-based formal methods provide a link between many of these different areas, for example using logic-based methods we can express properties of complex temporal structures, of hybrid and continuous systems, of probabilistic behaviours, of reliability, concurrency and autonomy.

The wide diversity of aerospace systems provides a strong source of new problems for logical/mathematical/AI methods. These systems might be satellites, unmanned aerial vehicles (UAVs), terrestrial or other kinds of flying robots, or even traditional aircraft. Such systems can be involved in complex activities such as space exploration, telecommunication support, fire detection, geo-mapping, weather prognoses, geo-rectification, search and rescue, naval traffic surveillance, tracking high value targets. From these applications, new research problems appear: autonomy, collective behaviour, information fusion, cognitive skills, coordination, flocking; etc. In addition, new concepts must be formalised: digital pheromones, swarms, system of systems of robots, sensing, physical actuation, and so on.

Aerospace systems are not only safety critical, but also mission critical and have very high performance requirements. For example, there is no safety issue regarding a planetary rover, but the system performance must justify the great cost of deploying it. Consequently, aerospace enriches traditional formal analysis methods topics with new (or, at least, rarely investigated) research issues.

Formal modelling and analysis approaches could greatly benefit from integration with approaches from other disciplines, and many such opportunities are now appearing. A good example is the problem of coordination for platoons of UAVs or satellites, which have been successfully tackled using various techniques from control engineering and numerical tools from dynamic programming. In addition, there exist an abundance of examples of Artificial Intelligence techniques in aerospace (target tracking, rover planning, multi-agent technologies and so on). The implementation of these methods could benefit from formal analysis and development. From the cross-fertilization of related multidisciplinary approaches, we expect more robust, safe and mechanizable modelling, development and verification methods for aerospace systems.

THE JOURNAL

The Annals of Mathematics and Artificial Intelligence journal is intended to represent a wide range of topics of concern to scholars applying quantitative, combinatorial, logical, algebraic and algorithmic methods to Artificial Intelligence areas as diverse as decision support, automated deduction, reasoning, knowledge-based systems, machine learning, computer vision, robotics and planning. The journal is aimed at: applied logicians, algorithms and complexity researchers, Artificial Intelligence theorists and applications specialists using mathematical methods. For more details, see http://www.kluweronline.com/issn/1012-2443

TOPICS OF INTEREST

The topics of interest of this special issue include (but are not limited to)

• new modeling paradigms
• formal verification of safety properties
• formal models for cyber-physical systems
• autonomous and autonomic systems
• performance modelling and verification
• heterogeneous and hybrid system models
• multi-agent systems and coordination technologies
• probabilistic logics for system specification
• stochastic modelling and verification methods
• control techniques that span over multiple disciplines
• communication and control co-design

specifically formal methods concerning the above within the area of aerospace.

This special issue is inspired by the FMA workshop held as part of FM-2009. However, submission to this special issue is open to everyone.

SUBMISSION OF MANUSCRIPTS

We invite submission of full (typically, 15-30 pages) high-quality research papers for this special issue. These should neither have been previously published in their full form, nor be under review elsewhere. Submissions consisting of the paper (in PDF form) and a separate abstract in which the role of formal methods in the particular approach used is clarified, should be emailed to one of the special issue editors (email addresses below) to arrive no later than 10th March 2010. Formatting instructions can be found at the journal's web site.

Queries concerning this special issue should be directed to any of the editors. Up-to-date information will also be available from http://www.csc.liv.ac.uk/~michael/AMAI10

IMPORTANT DATES

Submission deadline:	10th March 2010
Author notification:	10th May 2010
Revised papers due:	10th June 2010

SPECIAL ISSUE EDITORS

• MANUELA BUJORIANU
  School of Mathematics, University of Manchester, Manchester, U.K.
  email: Manuela.Bujorianu@manchester.ac.uk
  url: http://personalpages.manchester.ac.uk/staff/Manuela.Bujorianu

• MICHAEL FISHER
  Department of Computer Science, University of Liverpool, Liverpool, U.K.
  email: MFisher@liverpool.ac.uk         url: http://www.csc.liv.ac.uk/~michael

• CORINA PASAREANU
  CMU (Silicon Valley), USA and Robust Software Engineering group, NASA, USA
  email: Corina.S.Pasareanu@nasa.gov         url: http://ti.arc.nasa.gov/profile/pcorina

About this document ...

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.70)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -no_navigation -split 1 -address MFisher@liverpool.ac.uk amai10cfp.tex

The translation was initiated by Michael Fisher on 2009-12-18