Compositional Verification of Knowledge-Based Task Models and Problem-Solving Methods |
| |
Authors: | Frank?Cornelissen Email author" target="_blank">Catholijn M?JonkerEmail author Jan?Treur |
| |
Affiliation: | (1) Department of Artificial Intelligence, Vrije Universiteit Amsterdam, Amsterdam, The Netherlands;(2) Dept of Artificial Intelligence, Vrije Universiteit Amsterdam, De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands |
| |
Abstract: | In this paper a compositional verification method for task models and problem-solving methods for knowledge-based systems is introduced. Required properties of a system are formally verified by deriving them from assumptions that themselves are properties of sub-components, which in their turn may be derived from assumptions on sub-sub-components, and so on. The method is based on properties that are formalized in terms of temporal semantics; both static and dynamic properties are covered. The compositional verification method imposes structure on the verification process. Because of the possibility of focusing at one level of abstraction (information and process hiding), compositional verification provides transparency and limits the complexity per level. Since verification proofs are structured in a compositional manner, they can be reused in the event of reuse of models or modification of an existing system. The method is illustrated for a generic model for diagnostic reasoning. |
| |
Keywords: | Compositional verification Diagnostic reasoning model Formal compositional modeling Knowledge-based systems |
本文献已被 SpringerLink 等数据库收录! |
|