Automata-Theoretic Characterisations of Branching-Time Temporal Logics
arxiv(2024)
摘要
Characterisations theorems serve as important tools in model theory and can
be used to assess and compare the expressive power of temporal languages used
for the specification and verification of properties in formal methods. While
complete connections have been established for the linear-time case between
temporal logics, predicate logics, algebraic models, and automata, the
situation in the branching-time case remains considerably more fragmented. In
this work, we provide an automata-theoretic characterisation of some important
branching-time temporal logics, namely CTL* and ECTL* interpreted on
arbitrary-branching trees, by identifying two variants of Hesitant Tree
Automata that are proved equivalent to those logics. The characterisations also
apply to Monadic Path Logic and the bisimulation-invariant fragment of Monadic
Chain Logic, again interpreted over trees. These results widen the
characterisation landscape of the branching-time case and solve a
forty-year-old open question.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要