LTL under reductions with weaker conditions than stutter invariance

From LRDE

Abstract

Verification of properties expressed as omega-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 state of the art verification tools. 1 Introduction Model checking is an automatic verification technique for proving the correctness of systems that have finite state abstractions. Properties can be expressed using the popular Linear-time Temporal Logic (LTL). To verify LTL propertiesthe automata-theoretic approach [25] builds a product between a Buchi automaton representing the negation of the LTL formula and the reachable state graph of the system (seen as a set of infinite runs). This approach has been used successfully to verify both hardware and software components, but it suffers from the so called "state explosion problem": as the number of state variables in the system increases, the size of the system state space grows exponentially.

Documents

Bibtex (lrde.bib)

@InProceedings{	  paviot.22.forte,
  author	= {Emmanuel Paviot-Adet and Denis Poitrenaud and Etienne
		  Renault and Yann Thierry-Mieg},
  title		= {LTL under reductions with weaker conditions than stutter
		  invariance},
  booktitle	= {Proceedings of the 41th IFIP International Conference on
		  Formal Techniques for Distributed Objects, Components and
		  Systems (FORTE'22)},
  year		= 2022,
  month		= jun,
  series	= {Lecture Notes in Computer Science},
  volume	= 13273,
  pages		= {170--187},
  publisher	= {Springer},
  doi		= {10.1007/978-3-031-08679-3_11},
  abstract	= { Verification of properties expressed as omega-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 state of the art verification tools. 1 Introduction
		  Model checking is an automatic verification technique for
		  proving the correctness of systems that have finite state
		  abstractions. Properties can be expressed using the popular
		  Linear-time Temporal Logic (LTL). To verify LTL properties,
		  the automata-theoretic approach [25] builds a product
		  between a Buchi automaton representing the negation of the
		  LTL formula and the reachable state graph of the system
		  (seen as a set of infinite runs). This approach has been
		  used successfully to verify both hardware and software
		  components, but it suffers from the so called "state
		  explosion problem": as the number of state variables in the
		  system increases, the size of the system state space grows
		  exponentially.}
}