Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints (Q269503)

This paper presents a study of a certain extension of the full computation tree logic \textsf{CTL}* by eliminating the path formulas and replacing the temporal operators by a general framework of automata. The resulting extended computation tree logic \textsf{ECTL}* thus has no syntactic restrictions on the applications of temporal operators and path quantifiers, and can describe regular (i.e., \textsf{MSO}-definable) properties of paths. While the original formulation of \textsf{ECTL}* makes use of the Büchi automata, the paper under review replaces the classical \textsf{CTL}* path formulas by \textsf{MSO}-formulas. As the main result, the authors prove that satisfiability and finite satisfiability for \textsf{ECTL}* with certain constraints over \(\mathbb{Z}\) are decidable. It is also shown that the choice of the mentioned constraints in the form of certain path formulas is necessary for the result.