logics with different degrees of expressiveness
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.