Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints (Q269503)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints |
scientific article |
Statements
Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints (English)
0 references
18 April 2016
0 references
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.
0 references
temporal logic
0 references
computation tree logic
0 references
extended computation tree logic
0 references
integer constraints
0 references
bounding quantifiers
0 references
satisfiability
0 references
decidability
0 references
0 references