文章基本信息

标题：On the Expressiveness of QCTL
本地全文：下载
作者：Am{\'e}lie David ; Francois Laroussinie ; Nicolas Markey 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2016
卷号：59
页码：28:1-28:15
DOI：10.4230/LIPIcs.CONCUR.2016.28
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QkCTL, with at most k nested blocks of quantifiers, is (k+1)-EXPTIME-complete), very few results are known about the expressiveness of this logic. We address such expressiveness questions in this paper. We first consider the distinguishing power of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their expressive power (i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QkCTL collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).
关键词：Specification; Verification; Temporal Logic; Expressiveness; Tree automata