تقرير
Causality for General LTL-definable Properties
| العنوان: | Causality for General LTL-definable Properties |
|---|---|
| المؤلفون: | Caltais, Georgiana, Guetlein, Sophie Linnea, Leue, Stefan |
| المصدر: | EPTCS 286, 2019, pp. 1-15 |
| سنة النشر: | 2019 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Formal Languages and Automata Theory |
| الوصف: | 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. Comment: In Proceedings CREST 2018, arXiv:1901.00073 |
| نوع الوثيقة: | Working Paper |
| DOI: | 10.4204/EPTCS.286.1 |
| URL الوصول: | http://arxiv.org/abs/1901.00588 |
| رقم الأكسشن: | edsarx.1901.00588 |
| قاعدة البيانات: | arXiv |
| DOI: | 10.4204/EPTCS.286.1 |
|---|