Model-checking precision agriculture logistics: the case of the differential harvest

被引：0
作者：
Rim Saddem-yagoubi
Olivier Naud
Karen Godary-dejean
Didier Crestani
机构：
[1] ITAP,
[2] Univ Montpellier,undefined
[3] INRAE,undefined
[4] Montpellier SupAgro,undefined
[5] LIRMM,undefined
[6] Univ Montpellier,undefined
[7] CNRS,undefined
来源：
Discrete Event Dynamic Systems | 2020年 / 30卷
关键词：
Timed automata; Formal verification; Model-checking; Controller synthesis; Vehicle routing; UPPAAL-CORA; Optimisation; Precision agriculture;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
The development, in the last decades, of technologies for precision agriculture allows the acquisition of crop data with a high spatial resolution. This offers possibilities for innovative control and raises new logistics issues that may be solved using discrete event models. In vineyards, some technologies make it possible to define zones with different qualities of grapes and sort the grapes at harvest to make different vintages. In this context, the Differential Harvest Problem (DHP) consists in finding a trajectory of the harvesting machine in the field in order to obtain at least a given quantity of higher quality grapes and minimising working time. In available literature, the DHP has been solved using Constraint Programming. In this paper, we investigate if it is possible to solve the DHP using the Cost Optimal Reachability Analysis feature of a model-checking tool such as UPPAAL-CORA. A model named DHP_PTA has been designed based on the priced timed automata formalism and the UPPAAL-CORA tool. The method made it possible to obtain the optimal trajectory of a harvesting machine for a vine plot composed of up to 14 rows. The study is based on real vineyard data. This paper is an extended version of a communication presented at WODES 2018 (Saddem-Yagoubi IFAC-PapersOnLine 51(7):57–63, 2018).
引用
收藏
页码：579 / 604
页数：25
相关论文
共 50 条
  • [1] Alur R(1993)Model-checking in dense real-time Inform comput 104 2-34
  • [2] Courcoubetis C(1994)A theory of timed automata Theor Comput Sci 126 183-235
  • [3] Dill D(1991)Modeling and verification of time dependent systems using time petri nets IEEE Trans Soft Eng 17 259-273
  • [4] Alur R(2001)Heuristic search planner 2.0 AI Mag 22 77-77
  • [5] Dill DL(2006)Structural translation from time petri nets to timed automata J Syst Softw 79 1456-1468
  • [6] Berthomieu B(1986)“sometimes” and “not never” revisited: on branching versus linear time temporal logic J ACM (JACM) 33 151-178
  • [7] Diaz M(2003)Pddl2. 1: an extension to pddl for expressing temporal planning domains J Artif Intell Res 20 61-124
  • [8] Bonet B(2008)Using timed automata and model-checking to simulate material flow in agricultural production systems - application to animal waste management Comput Electron Agric 63 183-192
  • [9] Geffner H(2012)Use of timed automata and model-checking to explore scenarios on ecosystem models Environ Modell Softw 30 123-138
  • [10] Cassez Franck(2003)Compact data structures and state-space reduction for model-checking real-time systems Real-Time Systems 25 255-275
12345