On Locally Checkable Properties
The large computational price of formal verification of general
\omega-regular properties has led to the study of restricted classes
of properties, and to the development of verification methodologies
for them. Examples that have been widely accepted by the industry
include the verification of safety properties, and bounded model
checking. We introduce and study another restricted class of
properties -- the class of {\em locally checkable\/} properties. For
an integer k \geq 1, a language L\subseteq \Sigma^\omega is {\em
k-checkable} if there is a language R\subseteq \Sigma^k (of
``allowed subwords'') such that a word w belongs to L iff all the
subwords of w of length k belong to R. A property is locally
checkable if its language is k-checkable for some k. Locally
checkable properties, which are a special case of safety properties,
are common in the specification of systems. In particular, one can
often bound an eventuality constraint in a property by a fixed time
frame.
The practical importance of locally checkable properties lies in the
low memory demand for their run-time verification. A monitor for a
k-checkable property needs only a record of the last k computation
cycles. Furthermore, even if a large number of k-checkable
properties are monitored, the monitors can share their memory,
resulting in memory demand that do not depend on the number of
properties monitored. This advantage of locally checkable properties
makes them particularly suitable for run-time verification. In the
paper, we define locally checkable languages, study their relation to
other restricted classes of properties, study the question of deciding
whether a property is locally checkable, and study the relation
between the size of the property (specified by an LTL formula or an
automaton) and the smallest k for which the property is
k-checkable.