We are happy to announce that the following article has been accepted to
the 42nd International Conference on Formal Techniques for Distributed
Objects, Components, and Systems (FORTE'22), one of the three conference
of the 17th International Federated Conference on Distributed Computing
Techniques (DisCoTec'22) to be held on June 13-17 in Lucca, Italy.
(Philipp will go there to present the paper.)
======================================================================
LTL under reductions with weaker conditions than stutter invariance
Emmanuel Paviot-Adet (1)(2), Denis Poitrenaud (1)(2),
Etienne Renault (3), Yann Thierry-Mieg (1)
(1) SorbonneUniversité,CNRS,LIP6,F-75005Paris,France
(2) Université de Paris,F-75006Paris,France
(3) LRDE, EPITA, France
Verification of properties expressed as 𝜔-regular languages such as LTL can benefit hugely from
stutter insensitivity, using a diverse set of reduction strategies. However properties that are not
stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting
in the logic, are not covered by these techniques in general.
We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive
language both adding and removing stutter to a word does not change its acceptance, any stuttering can
be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions.
We define a shortening insensitive language where any word that stutters less than a word in the language must
also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure
is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while
working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton’s transaction
reductions or Petri net agglomerations are examples of eligible structural reduction strategies.
An implementation and experimental evidence is provided showing most non- random properties sensitive to stutter
are actually shortening or lengthening in- sensitive. Performance of experiments on a large (random) benchmark from
the model-checking competition indicate that despite being a semi-decision proce- dure, the approach can still improve