Deontic action logic, atomic boolean algebras and fault-tolerance |
| |
Authors: | Pablo F. Castro T.S.E. Maibaum |
| |
Affiliation: | aDepartment of Computing & Software, McMaster University, Main Street West 1280, Hamilton, Canada |
| |
Abstract: | We introduce a deontic action logic and its axiomatization. This logic has some useful properties (soundness, completeness, compactness and decidability), extending the properties usually associated with such logics. Though the propositional version of the logic is quite expressive, we augment it with temporal operators, and we outline an axiomatic system for this more expressive framework. An important characteristic of this deontic action logic is that we use boolean combinators on actions, and, because of finiteness restrictions, the generated boolean algebra is atomic, which is a crucial point in proving the completeness of the axiomatic system. As our main goal is to use this logic for reasoning about fault-tolerant systems, we provide a complete example of a simple application, with an attempt at formalization of some concepts usually associated with fault-tolerance. |
| |
Keywords: | Deontic logic Fault-tolerance Temporal logic Software engineering Formal methods |
本文献已被 ScienceDirect 等数据库收录! |
|