Abstract
Precision agriculture (PA) has grown strongly in recent decades with advances in locating methods and sensor and remote sensing technologies. The principle of the PA is to seek and implement the Right action at the Right time and in the Right place ("3R"), with the objective of improving the efficiency of agriculture according to the criteria of agriculture sustainable. We consider in this thesis the evaluation of the feasibility of agricultural operations with respect to the criteria set in a PA recommendation, using formal modeling and verification techniques.To model and verify these operations, a representation of temporal and spatial dynamics is necessary. The model-checking of timed automata systems with requests in temporal tree logic answers these needs. The spatial positions can be represented in an ad-hoc manner within the framework of these formalisms. Three examples of agricultural operations are considered in this thesis. The first relates to the computing of an optimal sequence of commands for a precision spraying in viticulture. The second concerns selective harvesting in viticulture. The last one is related to the verification of an agricultural robotics mission. We study in these examples the reachability of a target state for the operation, or the reachability with an optimal cost criterion.To overcome the combinatorial explosion problem encountered in the treated cases, a decomposition methodology for reachability model-checking has been developed. The experimental results with and without decomposition are presented for the 3 examples of operation studied. The decomposition methodology was applied to 2 of the 3 examples and the experimental results indicate its efficient.