%0 Conference Proceedings
%F Jard-Jeron-CAV89
%A Jard, C.
%A Jéron, T.
%T On-line model-checking for finite linear temporal logic specifications
%B Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France
%V 407
%P 275-285
%S LNCS
%I Springer-Verlag
%X 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
%U http://www.irisa.fr/vertecs/Publis/Ps/89-CAV.ps.gz
%8 June
%D 1989