|Institutional Office Address
DMIF, Room NN1, Phone: +39 0432 558440
|Research Project Title
Satisfiability and synthesis techniques for linear temporal logics with different degrees of expressiveness.
|Research Project Description
The project aims at systematically investigating satisfiability checking and synthesis techniques for linear temporal logics with different degrees of expressiveness in the context of model-based design.By different degrees of expressiveness, we refer to the ability of a logic to express properties which others are not able to define, e.g. temporal logics in which atoms (the simplest type of formula) are not simply propositional variables but belong to a theory or for example temporal logics interpreted over dense time.
The satisfiability problem for a given logic L is the problem of deciding whether a given formula of L has at least one model. The satisfiability problem for linear temporal logics is of great importance in the context of model-based design, and in particular in the context of formal specification and verification. As an example, before running a model checking algorithm, it is necessary to check if the input formula is consistent, i.e., if it meets the requirements. This preliminary step can be viewed as a sanity check and it basically consists in checking the input formula for satisfiability.
The synthesis problem is the problem of synthesizing a controller which by construction satisfies a given property. When the property is written in a temporal logic, this problem is particularly interesting as it allows us to specify an expected behavior over time and to synthesize a program which by construction satisfies it.