|
Abstract : |
Abstract. In this paper compositional verification of agents in dynamic environments is studied. Dynamic properties of an example agent in a dynamic environment are identified in relation to the different abstraction levels of the compositional structure of the system. The properties are formalised using temporal models. Mathematical proofs relate the properties at the different process abstraction levels. The dynamics of the environment has several consequences for the verification process. Properties often have to contain conditions concerning the dynamic behaviour of the world. In the proofs, the partly unpredictable behaviour of the word has to be taken into account. This complicates the verification process. A number of aspects of proof pragmatics (i.e., heuristics for finding proofs) identified during this analysis and aimed at controlling the proof complexity, are discussed. 1, |
