Declarative approaches to control-flow modeling use logic-based languages to formalize a number of constraints that valid traces must satisfy. The most noticeable example is the Declare framework based on linear… Click to show full abstract
Declarative approaches to control-flow modeling use logic-based languages to formalize a number of constraints that valid traces must satisfy. The most noticeable example is the Declare framework based on linear temporal logic. Despite the interest that Declare has been attracting, the current knowledge about its formal properties was rather limited. The goal of this paper is to fill this gap by: (i) analyzing the behavioral properties of Declare by comparing it with the modeling capabilities of traditional procedural design approaches, in particular, block-structured processes; (ii) analyzing Declare from the computational point of view. As for the former point, we identify both the block-structured processes constructs that can be simulated in Declare and the features of Declare that can be encoded in block-structured processes. As for the latter point, we show that checking whether a given set of Declare patterns admits a satisfying trace is an ${\mathrm {NP}}$ NP -hard problem. In particular, we identify some Declare specifications whose satisfying traces are all of exponential length and some useful Declare fragments where a satisfying trace whose length is polynomially bounded is guaranteed to exist. The paper also discusses the declare2sat prototype system and the results of a thorough experimental validation.
