文章基本信息

标题：Causality for General LTL-definable Properties
本地全文：下载
作者：Georgiana Caltais ; Sophie Linnea Guetlein ; Stefan Leue 等
期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2019
卷号：286
页码：1-15
DOI：10.4204/EPTCS.286.1
语种：English
出版社：Open Publishing Association
摘要：In this paper we provide a notion of causality for the violation of general Linear Temporal Logic (LTL) properties. The current work is a natural extension of the previously proposed approach handling causality in the context of LTL-definable safety properties. The major difference is that now, counterexamples of general LTL properties are not merely finite traces, but infinite lasso-shaped traces. We analyze such infinite counterexamples and identify the relevant ordered occurrences of causal events, obtained by unfolding the looping part of the lasso shaped counterexample sufficiently many times. The focus is on LTL properties from practical considerations: the current results are to be implemented in QuantUM, a tool for causality checking, that exploits explicit state LTL model checking.