Model checking has been traditionally concerned on verifying a (critical) system against its specification, which is generally expressed in temporal logic. Despite this verification technique is mature, it becomes useless when the specification incorporates vagueness, especially for the temporal constraints. This is often the case when non-critical adaptive systems are considered. These systems may tolerate small violations or may need to be aware of the satisfaction degree of their specification for re-configuration purposes. We present FTL (Fuzzy-time Temporal Logic), an extension of LTL that relaxes the notion of time, and propose a verification technique to evaluate the truth degree of such vague temporal properties. Our verification technique has been implemented in a prototype and the experimental results are promising.
Time Modalities over Many-valued Logics
SPOLETINI, PAOLA
2012-01-01
Abstract
Model checking has been traditionally concerned on verifying a (critical) system against its specification, which is generally expressed in temporal logic. Despite this verification technique is mature, it becomes useless when the specification incorporates vagueness, especially for the temporal constraints. This is often the case when non-critical adaptive systems are considered. These systems may tolerate small violations or may need to be aware of the satisfaction degree of their specification for re-configuration purposes. We present FTL (Fuzzy-time Temporal Logic), an extension of LTL that relaxes the notion of time, and propose a verification technique to evaluate the truth degree of such vague temporal properties. Our verification technique has been implemented in a prototype and the experimental results are promising.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
