# Timed Vacuity (Joint work with Hana Chockler, Orna Kupferman)

Submitted by gperez on Sun, 29/04/2018 - 09:33

Shibashis Guha

ULB

Friday, 11 May, 2018 - 11:45

ULB La Plaine NO, Salle Solvay

Vacuity is a leading sanity check in model-checking, applied when the
system is found to satisfy the specification. The check detects
situations where the specification passes in a trivial way, say when a
specification that requires every request to be followed by a grant is
satisfied in a system with no requests. Such situations typically reveal
serious problems in the modelling of the system or the specification,
and indeed vacuity detection is a part of most industrial model-checking
tools.
Existing research and tools for vacuity concern discrete-time systems
and specification formalisms. We introduce {\em real-time vacuity},
which aims to detect problems with real-time modelling. Real-time logics
are used for the specification and verification of systems with a
continuous-time behavior. We study vacuity for the branching real-time
logic TCTL, and focus on vacuity with respect to the time constraints in
the specification. Specifically, the logic TCTL includes a single
temporal operator $U^J$, which specifies real-time eventualities in
real-time systems: the parameter $J \subseteq \realpos$ is an interval
with integral boundaries that bounds the time in which the eventuality
should hold. We define several tightenings for the $U^J$ operator. These
tightenings require the eventuality to hold within a strict subset of
$J$. We prove that vacuity detection for TCTL is PSPACE-complete, thus
it does not increase the complexity of model-checking of TCTL. Our
contribution involves an extension, termed TCTL$^+$, of TCTL, which
allows the interval $J$ not to be continuous, and for which
model-checking stays in PSPACE. Finally, we discuss ways to rank vacuity
results by their significance, and extend the framework of ranking
vacuity to TCTL.