On the analysis of temporal logic specifications

OData support
Vörös András
Department of Measurement and Information Systems

Since the failures of safety-critical systems may have disastrous consequences,

ensuring their correct behaviour is an important task. To verify that the system

is working without errors, the use of formal methods are practical.

Model-checking is such a method which can be used during the design period to

find faults in the system. During the execution of model-checking the validity

of requirements expressed with temporal logics are examined. Several kinds of

temporal logics exist, my work is based on Linear Temporal Logic.

If a requirement is not valid on a model, we recieve a counterexample as the

result of the model-checking process, with which we can identify faults of the

model. In contrast if the requirement is valid on the model, we do not recieve

any additional information. This presents a problem because the incorrect

translation of an invalid requirement frequently results in a trivially valid

LTL-formula, therefore it is impossible to identify the fault.

Finding the so-called vacuity values of an LTL-formula can help us to

identify these incorrect translations by providing information on which parts of

the formula are unnecessary for the validity of the requirement.

In my work I present a method based on the examination of vacuity values, with

which we can warn the user in case of this type of error. Furthermore I

developed an algorithm to analyise the vacuity of the specification, what I

implemented as part of the PetriDotNet model-checking framework.


Please sign in to download the files of this thesis.