文章基本信息

标题：Temporal Logic with Recursion
本地全文：下载
作者：Florian Bruse ; Martin Lange
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：178
页码：6:1-6:14
DOI：10.4230/LIPIcs.TIME.2020.6
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We introduce extensions of the standard temporal logics CTL and LTL with a recursion operator that takes propositional arguments. Unlike other proposals for modal fixpoint logics of high expressive power, we obtain logics that retain some of the appealing pragmatic advantages of CTL and LTL, yet have expressive power beyond that of the modal Î¼-calculus or MSO. We advocate these logics by showing how the recursion operator can be used to express interesting non-regular properties. We also study decidability and complexity issues of the standard decision problems.
关键词：formal specification; temporal logic; expressive power