Output details
11 - Computer Science and Informatics
University of Westminster
Deontic extension of deductive verification of component model: combining computation tree logic and deontic logic in natural deduction style calculus
<11> Originality: Normative reasoning is core in modelling the behaviour of component based systems while non-deterministic temporal reasoning is core in capturing its dynamic nature. This paper is the first to merge these two frameworks extending the underlying computation tree logic with norms - permissions, obligations.
Significance: Not only the paper formally defines the concept of configuration/re-configuration but it also brings the methodological power of natural deduction goal-directed reasoning. This provides more transparent proofs and leads us to a lower complexity of the overall verification scenario.
Rigour: Mathematical proofs of the soundness and completeness of the proposed method are established.