Skip to main content
SpringerLink
Log in

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

  • Published:
Discrete Event Dynamic Systems Aims and scope Submit manuscript

Abstract

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).

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9

Similar content being viewed by others

Notes

  1. All these data were provided by Montpellier SupAgro.

  2. It is important to remind here that the number of explored states is not the total number of possible states, but the ones that are explored until the optimum is found.

  3. One may refer for details to the PhD thesis manuscript of Mrs Saddem-Yagoubi (2019)

References

  • Alur R, Courcoubetis C, Dill D (1993) Model-checking in dense real-time. Inform comput 104(1):2–34

    Article  MathSciNet  MATH  Google Scholar 

  • Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126:183–235

    Article  MathSciNet  MATH  Google Scholar 

  • Alur R, La Torre S, Pappas GJ (2001) Optimal paths in weighted timed automata. In: International workshop on hybrid systems: computation and control, pages 49–62. Springer

  • Asarin E, Maler O, Pnueli A, Sifakis J, Controller synthesis for timed automata. IFAC Proceedings Volumes 31(18):447 – 452. 5th IFAC Conference on System Structure and Control 1998 (SSC’98) Nantes (1998)

  • Behrmann G, Fehnker A, Hune T, Larsen K, Pettersson P, Romijn J, Vaandrager F (2001a) Minimum-cost reachability for priced timed automata. In: International workshop on hybrid systems: computation and control, volume 1, pages 147–161. Springer

  • Behrmann G, Fehnker A, Hune T, Larsen KG, Petterson P, Romijn J (2001b) Guiding and cost-optimality in UPPAAL. In: AAAI-Spring Symposium on Model-based Validation of Intelligence, pages 66–74

  • Behrmann G, Larsen KG, Rasmussen JI (2004) Priced timed automata: Algorithms and applications. In: FMCO, volume 3657, pages 162–182. Springer

  • Bengtsson J, Automata WY (2004) Timed semantics, algorithms and tools. Springer, Berlin, pp 87–124

    MATH  Google Scholar 

  • Bérard B, Cassez F, Haddad S, Lime D, Roux OH (2005) Comparison of the expressiveness of timed automata and time petri nets. In: International conference on formal modeling and analysis of timed systems, pages 211–225. Springer

  • Berthomieu B, Diaz M (1991) Modeling and verification of time dependent systems using time petri nets. IEEE Trans Soft Eng 17(3):259–273

    Article  MathSciNet  Google Scholar 

  • Bonet B, Geffner H (2001) Heuristic search planner 2.0. AI Mag 22(3):77–77

    MATH  Google Scholar 

  • Bouyer P, Cassez F, Fleury E, Larsen KG (2004). In: International Conference on Foundations of Software Technology and Theoretical Computer Science, pages 148–160. Springer

  • Briot N, Bessiere C, Tisseyre B, Vismara P (2015a) Integration of operational constraints to optimize differential harvest in viticulture. In: Proc. 10th European Conference on Precision Agriculture (ECPA 2015), pages 487–494

  • Briot N, Bessiere C, Vismara P (2015b) A constraint-based approach to the differential harvest problem. In: Proc. 21st International Conference on Principles and Practice of Constraint Programming (CP 2015), volume 9255 of Lecture Notes in Computer Science, pages 541–556. Springer Berlin

  • Briot N, Bessiere C, Vismara P (2015c) Programmation par contraintes pour la vendange sélective. In: Actes des Onzièmes Journé,es Francophones de Programmation par Contraintes (JFPC 2015), pages 51–56

  • Cassez Franck, Roux Olivier H (2006) Structural translation from time petri nets to timed automata. J Syst Softw 79(10):1456–1468

    Article  MATH  Google Scholar 

  • Cimatti A (2000) Industrial applications of model checking. In: Summer school on modeling and verification of parallel processes, pages 153–168. Springer

  • Clabaut M, Ge N, Breton N, Jenn E, Delmas R, Fonteneau Y (2016) Industrial grade model checking: use cases, constraints tools and applications

  • Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on logic of programs, pages 52–71. Springer

  • Clarke EM, Grumberg O, Peled D (1999) Model checking MIT press

  • Dechter R (2003) Constraint processing morgan kaufmann

  • Duflot M, Kwiatkowska M, Norman G, parker D, Peyronnet S, Picaronny C, Sproston J (2012) Practical applications of probabilistic model checking to communication protocols

  • Emerson EA, Halpern JY (1986) “sometimes” and “not never” revisited: on branching versus linear time temporal logic. J ACM (JACM) 33(1):151–178

    Article  MathSciNet  MATH  Google Scholar 

  • Fahrenberg U, Larsen KG, Legay A (2013) Model-based verification, optimization, synthesis and performance evaluation of real-time systems. In: Unifying theories of programming and formal engineering methods, pages 67–108. Springer

  • Fox M, Derek L (2003) Pddl2. 1: an extension to pddl for expressing temporal planning domains. J Artif Intell Res 20:61–124

    Article  MATH  Google Scholar 

  • Grumberg O, Veith H (2008) 25 years of model checking: history, achievements, perspectives, vol 5000. Springer, Berlin

    Book  MATH  Google Scholar 

  • Hélias A, Guerrin F, Steyer JP (2008) Using timed automata and model-checking to simulate material flow in agricultural production systems - application to animal waste management. Comput Electron Agric 63(2):183–192

    Article  Google Scholar 

  • CPLEX, IBM ILOG. 12.6 Reference Manual. IBM ILOG: France, 2013, vol. 12

  • Kilby P, Shaw P (2006) Chapter 23 - vehicle routing. In: Francesca Rossi, Peter van Beek, and Toby Walsh, (eds), Handbook of constraint programming, volume 2 of foundations of artificial intelligence, pages 801–836. Elsevier

  • Largouët C, Krichen O, Zhao Y (2016) Temporal planning with extended timed automata. In: 2016 IEEE 28th International Conference on Tools with Artificial Intelligence (ICTAI), pages 522–529. IEEE

  • Largouët C, Cordier MO, Bozec YM, Zhao Y, Fontenelle G (2012) Use of timed automata and model-checking to explore scenarios on ecosystem models. Environ Modell Softw 30:123–138

    Article  Google Scholar 

  • Larsen KG, Larsson F, Pettersson P, Yi W (2003) Compact data structures and state-space reduction for model-checking real-time systems. Real-Time Systems 25 (2-3):255–275

    Article  MATH  Google Scholar 

  • Larsen KG, Pettersson P, Yi W (1997) Uppaal in a nutshell. Int J Softw Tools Technol Transfer 1(1-2):134–152

    Article  MATH  Google Scholar 

  • Lowder SK, Skoet J, Raney T (2016) The number, size, and distribution of farms, smallholder farms, and family farms worldwide. World Dev 87:16–29

    Article  Google Scholar 

  • McBratney A, Whelan B, Ancev T, Bouma J (2005) Future directions of precision agriculture. Precis agri 6(1):7–23

    Article  Google Scholar 

  • McBratney AB, Taylor JA (2000) Pv or not pv?. In: proceedings of the 5th international symposium on cool climate viticulture and œnology. Melbourne, Australia

  • Pnueli A (1977) The temporal logic of programs. In: Foundations of computer science, 1977., 18th Annual Symposium on, pages 46–57. IEEE

  • Prud’homme C, Fages JG, Lorca X, Choco3 Documentation.. TASC INRIA Rennes LINA CNRS UMR 6241 (2014)

  • Queille JP , Sifakis J (1982) Specification and verification of concurrent systems in cesar. In: International Symposium on programming, pages 337–351. Springer

  • Rajeev A, David D (1990) Automata for modeling real-time systems. In: International colloquium on automata, languages, and programming, pages 322–335. Springer

  • Saddem R, Naud O, Cazenave P, Godary-Dejean K, Crestani D (2017) Precision spraying: from map to sprayer control using model-checking. J Agri Inform 8 (3):1–10

    Google Scholar 

  • Saddem R, Naud O, Godary K, Crestani D (2017) Decomposing the model-checking of mobile robotics actions on a grid. (20th IFAC World Congress). IFAC-PapersOnLine 50(1):11156–11162

    Article  Google Scholar 

  • Saddem-Yagoubi R (2019) Model-checking pour l’agriculture de precision. PhD thesis, Univ. of Montpellier, In french

  • Saddem-Yagoubi R, Naud O, Godary K, Crestani D (2018) New approach for differential harvest problem: The model checking way. (14th IFAC Workshop on Discrete Event Systems WODES). IFAC-PapersOnLine 51(7):57–63

    Article  Google Scholar 

  • Zhao Y (2014) Modélisation qualitative des agro-écosystèmes et aide à leur gestion par utilisation d’outils de model-checking. PhD thesis, Univ. of Rennes 1, In French

Download references

Acknowledgments

We thank the authors of Briot et al. (2015a) for sharing vineyard data.

Author information

Authors and Affiliations

  1. ITAP, Univ Montpellier, INRAE, Montpellier SupAgro, Montpellier, France

    Rim Saddem-yagoubi & Olivier Naud

  2. LIRMM, Univ Montpellier, CNRS, Montpellier, France

    Rim Saddem-yagoubi, Karen Godary-dejean & Didier Crestani

Authors
  1. Rim Saddem-yagoubi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Olivier Naud
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Karen Godary-dejean
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Didier Crestani
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rim Saddem-yagoubi.

Additional information

Publisher’s note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This article belongs to the Topical Collection: Topical Collection on Applications-2020

Guest Editors: Francesco Basile, Jan Komenda, and Christoforos Hadjicostis

This work has received the support of French National Research Agency under the grant number ANR-14-CE27-0004 attributed to AdAP2E project.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Saddem-yagoubi, R., Naud, O., Godary-dejean, K. et al. Model-checking precision agriculture logistics: the case of the differential harvest. Discrete Event Dyn Syst 30, 579–604 (2020). https://doi.org/10.1007/s10626-020-00313-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10626-020-00313-1

Keywords

Search

Navigation