NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner

Computer Science Review Publishes Kristin Y. Rozier’s Linear Temporal Logic Symbolic Model Checking Paper

A survey paper titled “Linear Temporal Logic Symbolic Model Checking,” written by Kristin Y. Rozier, will appear in the May, 2011 issue of the Computer Science Review Journal. This paper is a response to the increasing use of formal verification techniques in safety-critical software and hardware in practice. Formal verification has been successfully used to verify systems including air traffic control, airplane separation assurance, autopilot, CPU designs, life-support systems, medical equipment (such as devices that administer radiation), and many other systems that ensure human safety. This survey provides a perspective on the formal verification technique of Linear Temporal Logic (LTL) symbolic model checking, from its history and evolution leading up to the state-of-the-art. It unifies research from 1977 to 2009, providing a complete end-to-end analysis, and embraces a users’ perspective by applying each step to a real-life aerospace example.

The paper includes an in-depth examination of the algorithms underlying the symbolic model-checking procedure, shows proofs of important theorems, and points to directions of ongoing research. The primary focus is on model checking using LTL specifications, though other approaches are briefly discussed and compared with using LTL.

The editor’s reviews state that the paper was set apart by applying all of the verification techniques presented on the real automated airspace concept architecture. One review stated: “This is a state of the art survey written in a good style with the aim on applications and illustrative examples taken from air-traffic control. However engineering aspects and comments are spread throughout the whole text. This is one of the strong points of this survey.” The paper provides thorough coverage of the most impactful research in LTL symbolic model checking, including 169 references.

The survey paper is available here: http://ti.arc.nasa.gov/m/profile/kyrozier/papers/COSREV_62.pdf.. The DOI site is at: http://dx.doi.org/10.1016/j.cosrev.2010.06.002.

BACKGROUND: Computer Science Review intends to fulfill a need in the computer science community by publishing research surveys and expository overviews in computer science and related fields. The reviews are aimed at a general computer science audience seeking a full and expert overview of the latest in computer science research.

Articles should be of sufficient scientific interest and help to advance the fundamental understanding of ongoing research, applied or theoretical, for a general computer science audience. The treatment of each topic should be more than a catalogue of known results. Emphasis should be on clarity and originality of presentation and each survey should add insight to the topic under review.

A survey typically contains the following elements:

  • Introduction (including motivation and historical remarks)
  • Outline of the survey
  • Basic concepts, examples, and results (with sketches of proofs)
  • Comments on the relevance of results, and relations to other results and applications
  • Open problems
  • Critical review of the relevant literature
  • Comprehensive bibliography

NASA PROGRAM FUNDING: Next Generation Air Transport System (NGATS) project

Contact: Kristin Y. Rozier

+NASA Home

+Ames Home

Computer Science Review Publishes Kristin Y. Rozier’s Linear Temporal Logic Symbolic Model Checking Paper
+ Home + Organization + News + Research Areas + Publications + Software + Internal Systems Help
First Gov logo
NASA Logo - nasa.gov