Jard-Jeron-CAV89

C. Jard, T. Jéron. On-line model-checking for finite linear temporal logic specifications. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, LNCS, Volume 407, Pages 275-285, June 1989.

Download [help]

Download paper: Gziped Postscript

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

Model-checking is the basis of several verification tools. It allows to check if a finite state program satisfies a set of temporal logic formulas. The main limitation is the size of the memory needed to record the state graph. Avoiding state space explosion is necessary to improve the applicability of such verification tools. For that aim, we explore an approach called ``on-line model-checking" where satisfiability is checked during the state generation process. We deal with the simple context of checking finite computations against linear temporal logic properties. The logic specification is first translated into a finite automaton. This one values the system states during enumeration. Validity can be decided in finite time provided a memory larger than the state graph diameter. Precise algorithms and some results of experiments are given

Contact

Thierry Jéron http://www.irisa.fr/prive/jeron

BibTex Reference

@InProceedings{Jard-Jeron-CAV89,
   Author = {Jard, C. and Jéron, T.},
   Title = {On-line model-checking for finite linear temporal logic specifications},
   BookTitle = {Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France},
   Volume = {407},
   Pages = {275--285},
   Series = {LNCS},
   Publisher = {Springer-Verlag},
   Month = {June},
   Year = {1989}
}

EndNote Reference [help]

Get EndNote Reference (.ref)