{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T22:20:38Z","timestamp":1780957238791,"version":"3.54.1"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2020,5,8]],"date-time":"2020-05-08T00:00:00Z","timestamp":1588896000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,5,8]],"date-time":"2020-05-08T00:00:00Z","timestamp":1588896000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-14-CE27-0004"],"award-info":[{"award-number":["ANR-14-CE27-0004"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s10626-020-00313-1","type":"journal-article","created":{"date-parts":[[2020,5,8]],"date-time":"2020-05-08T20:02:30Z","timestamp":1588968150000},"page":"579-604","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Model-checking precision agriculture logistics: the case of the differential harvest"],"prefix":"10.1007","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6663-5170","authenticated-orcid":false,"given":"Rim","family":"Saddem-yagoubi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Olivier","family":"Naud","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Karen","family":"Godary-dejean","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Didier","family":"Crestani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,5,8]]},"reference":[{"issue":"1","key":"313_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur R, Courcoubetis C, Dill D (1993) Model-checking in dense real-time. Inform comput 104(1):2\u201334","journal-title":"Inform comput"},{"key":"313_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126:183\u2013235","journal-title":"Theor Comput Sci"},{"key":"313_CR3","doi-asserted-by":"crossref","unstructured":"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\u201362. Springer","DOI":"10.1007\/3-540-45351-2_8"},{"key":"313_CR4","doi-asserted-by":"crossref","unstructured":"Asarin E, Maler O, Pnueli A, Sifakis J, Controller synthesis for timed automata. IFAC Proceedings Volumes 31(18):447 \u2013 452. 5th IFAC Conference on System Structure and Control 1998 (SSC\u201998) Nantes (1998)","DOI":"10.1016\/S1474-6670(17)42032-5"},{"key":"313_CR5","doi-asserted-by":"crossref","unstructured":"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\u2013161. Springer","DOI":"10.1007\/3-540-45351-2_15"},{"key":"313_CR6","doi-asserted-by":"crossref","unstructured":"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\u201374","DOI":"10.7146\/brics.v8i4.20458"},{"key":"313_CR7","doi-asserted-by":"crossref","unstructured":"Behrmann G, Larsen KG, Rasmussen JI (2004) Priced timed automata: Algorithms and applications. In: FMCO, volume 3657, pages 162\u2013182. Springer","DOI":"10.1007\/11561163_8"},{"key":"313_CR8","first-page":"87","volume-title":"Timed semantics, algorithms and tools","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson J, Automata WY (2004) Timed semantics, algorithms and tools. Springer, Berlin, pp 87\u2013124"},{"key":"313_CR9","doi-asserted-by":"crossref","unstructured":"B\u00e9rard 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\u2013225. Springer","DOI":"10.1007\/11603009_17"},{"issue":"3","key":"313_CR10","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B Berthomieu","year":"1991","unstructured":"Berthomieu B, Diaz M (1991) Modeling and verification of time dependent systems using time petri nets. IEEE Trans Soft Eng 17(3):259\u2013273","journal-title":"IEEE Trans Soft Eng"},{"issue":"3","key":"313_CR11","first-page":"77","volume":"22","author":"B Bonet","year":"2001","unstructured":"Bonet B, Geffner H (2001) Heuristic search planner 2.0. AI Mag 22(3):77\u201377","journal-title":"AI Mag"},{"key":"313_CR12","doi-asserted-by":"crossref","unstructured":"Bouyer P, Cassez F, Fleury E, Larsen KG (2004). In: International Conference on Foundations of Software Technology and Theoretical Computer Science, pages 148\u2013160. Springer","DOI":"10.1007\/978-3-540-30538-5_13"},{"key":"313_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013494","DOI":"10.3920\/978-90-8686-814-8_60"},{"key":"313_CR14","doi-asserted-by":"crossref","unstructured":"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\u2013556. Springer Berlin","DOI":"10.1007\/978-3-319-23219-5_38"},{"key":"313_CR15","unstructured":"Briot N, Bessiere C, Vismara P (2015c) Programmation par contraintes pour la vendange s\u00e9lective. In: Actes des Onzi\u00e8mes Journ\u00e9,es Francophones de Programmation par Contraintes (JFPC 2015), pages 51\u201356"},{"issue":"10","key":"313_CR16","doi-asserted-by":"publisher","first-page":"1456","DOI":"10.1016\/j.jss.2005.12.021","volume":"79","author":"Franck Cassez","year":"2006","unstructured":"Cassez Franck, Roux Olivier H (2006) Structural translation from time petri nets to timed automata. J Syst Softw 79(10):1456\u20131468","journal-title":"J Syst Softw"},{"key":"313_CR17","doi-asserted-by":"crossref","unstructured":"Cimatti A (2000) Industrial applications of model checking. In: Summer school on modeling and verification of parallel processes, pages 153\u2013168. Springer","DOI":"10.1007\/3-540-45510-8_6"},{"key":"313_CR18","unstructured":"Clabaut M, Ge N, Breton N, Jenn E, Delmas R, Fonteneau Y (2016) Industrial grade model checking: use cases, constraints tools and applications"},{"key":"313_CR19","doi-asserted-by":"crossref","unstructured":"Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on logic of programs, pages 52\u201371. Springer","DOI":"10.1007\/BFb0025774"},{"key":"313_CR20","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking MIT press"},{"key":"313_CR21","unstructured":"Dechter R (2003) Constraint processing morgan kaufmann"},{"key":"313_CR22","doi-asserted-by":"crossref","unstructured":"Duflot M, Kwiatkowska M, Norman G, parker D, Peyronnet S, Picaronny C, Sproston J (2012) Practical applications of probabilistic model checking to communication protocols","DOI":"10.1002\/9781118459898.ch7"},{"issue":"1","key":"313_CR23","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson EA, Halpern JY (1986) \u201csometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. J ACM (JACM) 33(1):151\u2013178","journal-title":"J ACM (JACM)"},{"key":"313_CR24","doi-asserted-by":"crossref","unstructured":"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\u2013108. Springer","DOI":"10.1007\/978-3-642-39721-9_2"},{"key":"313_CR25","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1613\/jair.1129","volume":"20","author":"M Fox","year":"2003","unstructured":"Fox M, Derek L (2003) Pddl2. 1: an extension to pddl for expressing temporal planning domains. J Artif Intell Res 20:61\u2013124","journal-title":"J Artif Intell Res"},{"key":"313_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0","volume-title":"25 years of model checking: history, achievements, perspectives, vol 5000","author":"O Grumberg","year":"2008","unstructured":"Grumberg O, Veith H (2008) 25 years of model checking: history, achievements, perspectives, vol 5000. Springer, Berlin"},{"issue":"2","key":"313_CR27","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.compag.2008.02.008","volume":"63","author":"A H\u00e9lias","year":"2008","unstructured":"H\u00e9lias 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\u2013192","journal-title":"Comput Electron Agric"},{"key":"313_CR28","unstructured":"CPLEX, IBM ILOG. 12.6 Reference Manual. IBM ILOG: France, 2013, vol. 12"},{"key":"313_CR29","doi-asserted-by":"crossref","unstructured":"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\u2013836. Elsevier","DOI":"10.1016\/S1574-6526(06)80027-1"},{"key":"313_CR30","doi-asserted-by":"crossref","unstructured":"Largou\u00ebt 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\u2013529. IEEE","DOI":"10.1109\/ICTAI.2016.0086"},{"key":"313_CR31","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/j.envsoft.2011.08.005","volume":"30","author":"C Largou\u00ebt","year":"2012","unstructured":"Largou\u00ebt 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\u2013138","journal-title":"Environ Modell Softw"},{"issue":"2-3","key":"313_CR32","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1023\/A:1025132427497","volume":"25","author":"KG Larsen","year":"2003","unstructured":"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\u2013275","journal-title":"Real-Time Systems"},{"issue":"1-2","key":"313_CR33","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) Uppaal in a nutshell. Int J Softw Tools Technol Transfer 1(1-2):134\u2013152","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"313_CR34","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1016\/j.worlddev.2015.10.041","volume":"87","author":"SK Lowder","year":"2016","unstructured":"Lowder SK, Skoet J, Raney T (2016) The number, size, and distribution of farms, smallholder farms, and family farms worldwide. World Dev 87:16\u201329","journal-title":"World Dev"},{"issue":"1","key":"313_CR35","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s11119-005-0681-8","volume":"6","author":"A McBratney","year":"2005","unstructured":"McBratney A, Whelan B, Ancev T, Bouma J (2005) Future directions of precision agriculture. Precis agri 6(1):7\u201323","journal-title":"Precis agri"},{"key":"313_CR36","unstructured":"McBratney AB, Taylor JA (2000) Pv or not pv?. In: proceedings of the 5th international symposium on cool climate viticulture and \u0153nology. Melbourne, Australia"},{"key":"313_CR37","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Foundations of computer science, 1977., 18th Annual Symposium on, pages 46\u201357. IEEE","DOI":"10.1109\/SFCS.1977.32"},{"key":"313_CR38","unstructured":"Prud\u2019homme C, Fages JG, Lorca X, Choco3 Documentation.. TASC INRIA Rennes LINA CNRS UMR 6241 (2014)"},{"key":"313_CR39","doi-asserted-by":"crossref","unstructured":"Queille JP , Sifakis J (1982) Specification and verification of concurrent systems in cesar. In: International Symposium on programming, pages 337\u2013351. Springer","DOI":"10.1007\/3-540-11494-7_22"},{"key":"313_CR40","unstructured":"Rajeev A, David D (1990) Automata for modeling real-time systems. In: International colloquium on automata, languages, and programming, pages 322\u2013335. Springer"},{"issue":"3","key":"313_CR41","first-page":"1","volume":"8","author":"R Saddem","year":"2017","unstructured":"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\u201310","journal-title":"J Agri Inform"},{"issue":"1","key":"313_CR42","doi-asserted-by":"publisher","first-page":"11156","DOI":"10.1016\/j.ifacol.2017.08.1236","volume":"50","author":"R Saddem","year":"2017","unstructured":"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\u201311162","journal-title":"IFAC-PapersOnLine"},{"key":"313_CR43","unstructured":"Saddem-Yagoubi R (2019) Model-checking pour l\u2019agriculture de precision. PhD thesis, Univ. of Montpellier, In french"},{"issue":"7","key":"313_CR44","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.ifacol.2018.06.279","volume":"51","author":"R Saddem-Yagoubi","year":"2018","unstructured":"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\u201363","journal-title":"IFAC-PapersOnLine"},{"key":"313_CR45","unstructured":"Zhao Y (2014) Mod\u00e9lisation qualitative des agro-\u00e9cosyst\u00e8mes et aide \u00e0 leur gestion par utilisation d\u2019outils de model-checking. PhD thesis, Univ. of Rennes 1, In French"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-020-00313-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-020-00313-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-020-00313-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,8]],"date-time":"2021-05-08T01:45:19Z","timestamp":1620438319000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-020-00313-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,8]]},"references-count":45,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["313"],"URL":"https:\/\/doi.org\/10.1007\/s10626-020-00313-1","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,5,8]]},"assertion":[{"value":"13 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 February 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 May 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}