التفاصيل البيبلوغرافية
العنوان: |
Defeasible linear temporal logic. |
المؤلفون: |
Chafik, Anasse, Cheikh-Alili, Fahima, Condotta, Jean-François, Varzinczak, Ivan |
المصدر: |
Journal of Applied Non-Classical Logics; Mar2023, Vol. 33 Issue 1, p1-51, 51p |
مصطلحات موضوعية: |
DESCRIPTION logics, ARTIFICIAL intelligence, LOGIC, NONMONOTONIC logic, COMPUTER systems, MODAL logic |
الشركة/الكيان: |
KLM Royal Dutch Airlines (Company) |
مستخلص: |
After the seminal work of Kraus, Lehmann and Magidor (formally known as the KLM approach) on conditionals and preferential models, many aspects of defeasibility in more complex formalisms have been studied in recent years. Examples of these aspects are the notion of typicality in description logic and defeasible necessity in modal logic. We discuss a new aspect of defeasibility that can be expressed in the case of temporal logic, which is the normality in an execution. In this contribution, we take Linear Temporal Logic ( L T L ) as case study for this defeasible aspect. L T L has found extensive applications in Computer Science and Artificial Intelligence, notably as a formal framework for representing and verifying computer systems that vary over time. However, some systems may presents exceptions at some innocuous time points where they can be tolerated, or conversely, exceptions at other crucial time points where they need to be addressed. In order to ensure the reliability of such systems, we study a preferential extension of L T L , called defeasible linear temporal logic ( L T L ~ ). In the first part of this paper, we show how semantics of KLM's preferential models can be integrated with L T L . We also discuss the addition of non-monotonic temporal operators as a way to formalise defeasible properties of these systems. The second part of this paper is a study of the satisfiability problem of L T L ~ sentences. Based on Sistla and Clarke's work on the complexity of the classical L T L language, we show the bounded-model property of two fragments of L T L ~ language. Moreover, we provide a procedure to check the satisfiability of sentences in both of these fragments. [ABSTRACT FROM AUTHOR] |
|
Copyright of Journal of Applied Non-Classical Logics is the property of Taylor & Francis Ltd and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
قاعدة البيانات: |
Complementary Index |