Defeasible Temporal Logic for the specification and verification of exception-tolerant systems
- PhD Student:
- Anasse Chafik
- Co-Advisors :
- Jean-François Condotta
- Ivan Varzinczak
- Co-Supervisor :
- Fahima Cheikh-Alili
- Funding : Artois
- PhD defended on :
- Sep 9, 2022 • thesis room, Faculty of Science Jean Perrin, Lens
Specification and verification of computer systems with dynamic behavior are important tasks, given the increasing number of new computer technologies that are being designed. Recent examples include blockchain technology and the various existing tools for home automation or the various production chains planned by Industry 4.0. Therefore, it is fundamental to ensure that systems based on these have the desired behavior but, above all, meet increasingly demanding security standards. This becomes even more critical with the increasing deployment of artificial intelligence techniques as well as the need to explain their behavior.
Several approaches for the qualitative analysis of computer systems have been developed. Among the most successful are the different families of temporal logics. The success of these logics is mainly due to their simplified syntax (compared to first order logic), their intuitive semantics, based on transition systems and automata, their good computational properties, and the fact that they are more easily implemented. This is confirmed by the existence of several tools based on these logics.
Despite the success and wide use of temporal logics, they remain limited for modeling and reasoning about real aspects of computer systems or those that depend on them. Indeed, computer systems are not either 100% safe or 100% faulty, and the properties one wishes to verify may have trivial and tolerable exceptions, or on the contrary, exceptions that must be carefully handled in order to guarantee the overall reliability of the system. Similarly, the expected behavior of a system may not be correct for every possible execution, but rather for its most “normal” or probable executions. Moreover, exceptions foreseen in advance by the designer may also have exceptional cases.
It so happens that temporal logics, because they are logical formalisms of the so-called classical type, i.e., whose underlying reasoning is mathematics and not the common sense, do not allow at all to formalize the different nuances of exceptions and even less to treat them. Technically the reason being that these logics (1) at the level of propositions, are often based on two truth values (true or false), (2) at the level of the object language, have operators behaving in a monotonous way, and (3) at the level of reasoning, have a notion of logical consequence which is also monotonous and, consequently, is not adapted to the evolution of the deductible facts.
The so-called non-monotonic reasoning, allowing to formalize and reason with exceptions and information dynamism, has been widely studied by the AI community for almost 40 years. However, the major contributions in this field are limited to the propositional framework, which is not very expressive for the above tasks. It is only recently that some approaches for non-monotonic reasoning, such as circumscription, default rules and preferential approaches, have been studied for logics more expressive than propositional logic, notably modal and description logics, but in settings other than specification and verification. The bridge between temporal formalisms for the specification and verification of computer systems and the different approaches for non-monotonic reasoning, allowing to satisfactorily solve the limitations raised above, remains to be built. This is the general objective of this thesis.
Required knowledge :
- Propositional and first order logic.
Technical skills to be developed during the internship:
- Modal logic
- Temporal logics
- Approaches to non-monotonic reasoning
- Model theory and proof theory related to the above formalisms
References (not exhaustive):
O. Arieli and A. Avron. General patterns for nonmonotonic reasoning : From basic entailments to plausible relations. Logic Journal of the IGPL. Volume 8, Pages 119-148. 2000.
M. Ben-Ari. Mathematical Logic for Computer Science. 3rd edition. Springer-Verlag. 2012.
J. van Benthem. Modal Logic for Open Minds. Center for the Study of Language and Informa- tion. 2010.
D. Harel and J. Tiuryn and D. Kozen. Dynamic Logic. MIT Press. 2000.
D. Makinson. Bridges from Classical to Nonmonotonic Logic. King’s College Publications. Volume 5 in Texts in Computing. 2005.
D. Makinson. How to go nonmonotonic. Handbook of Philosophical Logic, Volume 12. Pages 175-278. 2005.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Vol. I : Specification. Springer, New York, NY, 1992.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Vol. II : Safety. Springer, New York, NY, 1995.