Inherent Vacuity in Lattice Automata

8 years 3 days ago

Download www.cs.huji.ac.il

Vacuity checking is traditionally performed after model checking has terminated successfully. It ensures that all the elements of the speciﬁcation have played a role in its satisfaction by the system. The need to check the quality of speciﬁcations is even more acute in property-based design, where the speciﬁcation 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 speciﬁcation is inherently vacuous if it can be mutated into a simpler equivalent speciﬁcation, which is known, in the case of speciﬁcations in linear temporal logic, to coincide with the fact the speciﬁcation is satisﬁed 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 ...

Hila Gonen, Orna Kupferman

Real-time Traffic