Amministrazione trasparente

Linear temporal logics on finite traces are used to specify temporal properties over finite executions. In (reactive) synthesis, we automatically construct a strategy (a program) that satisfies the specification for all possible behaviors of the environment. However, sometimes such a winning strategy does not exist; that is, the specification is unrealizable. In such cases, instead of giving up, one can adopt best-effort synthesis, which extends standard synthesis to deal gracefully with unrealizable specifications. This research aims to study this form of synthesis for variants of Linear Temporal Logics on finite traces, including LTLf, LDLf, PPLTL, and other formalisms that may arise during the research itself.