Inherent Vacuity in Lattice Automata

Vacuity checking is traditionally performed after model checking has terminated successfully. It ensures that all the elements of the specification have played a role in its satisfaction by the system. The need to check the quality of specifications is even more acute in property-based design, where the specification is the only input, serving as a basis to the development of the system. Inherent vacuity adapts the theory of vacuity in model checking to the setting of property-based design. Essentially, a specification is inherently vacuous if it can be mutated into a simpler equivalent specification, which is known, in the case of specifications in linear temporal logic, to coincide with the fact the specification is satisfied vacuously in all systems. A recent development in formal methods is an extension of the Boolean setting to a multi-valued one. In particular, instead of Boolean automata, which either accept or reject their input, there is a growing interest in weighted ...

• Type: Journal
• Year: 2015
• Where: BIRTHDAY
• Authors: Hila Gonen, Orna Kupferman
• Keywords: Applied Computing, BIRTHDAY 2015