Possibilistic Reasoning on Finite-Time Linear Temporal Logic

Linear temporal logic on finite time (LTLf) has been successfully employed as a declarative language to represent and reason about business processes. However, in their classical form they are unable to handle the uncertainty inherent to many application domains and model learning methods. To alleviate this, we propose a possibilistic extension of LTLf designed to deal with qualitative uncertainty, first in a restricted form where uncertainty refers to full formulas, and then in a more expressive formalism with possibility as a full formula constructor. We present effective automata-based reasoning methods for this new language and show that it behaves computationally better than recently proposed probabilistic temporal logics.