{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T12:23:21Z","timestamp":1780489401574,"version":"3.54.1"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"2-3","license":[{"start":{"date-parts":[[2020,7,1]],"date-time":"2020-07-01T00:00:00Z","timestamp":1593561600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T00:00:00Z","timestamp":1584921600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["731869"],"award-info":[{"award-number":["731869"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["694277"],"award-info":[{"award-number":["694277"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2020,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Developing robotic applications is a complex task, which requires skills that are usually only possessed by highly-qualified robotic developers. While formal methods that help developers in the creation and design of robotic applications exist, they must be explicitly customized to be impactful in the robotics domain and to support effectively the growth of the robotic market. Specifically, the robotic market is asking for techniques that: (i) enable a systematic and rigorous design of robotic applications though high-level languages; and (ii) enable the automatic synthesis of low-level controllers, which allow robots to achieve their missions. To address these problems we present the PuRSUE (Planner for RobotS in Uncontrollable Environments) approach, which aims to support developers in the rigorous and systematic design of high-level run-time control strategies for robotic applications. The approach includes PuRSUE-ML a high-level language that allows for modeling the environment, the agents deployed therein, and their missions. PuRSUE is able to check automatically whether a controller that allows robots to achieve their missions might exist and, then, it synthesizes a controller. We evaluated how PuRSUE helps designers in modeling robotic applications, the effectiveness of its automatic computation of controllers, and how the approach supports the deployment of controllers on actual robots. The evaluation is based on 13 scenarios derived from 3 different robotic applications presented in the literature. The results show that: (i) PuRSUE-ML is effective in supporting designers in the formal modeling of robotic applications compared to a direct encoding of robotic applications in low-level modeling formalisms; (ii) PuRSUE enables the automatic generation of controllers that are difficult to create manually; and (iii) the plans generated with PuRSUE are indeed effective when deployed on actual robots.<\/jats:p>","DOI":"10.1007\/s00165-020-00509-0","type":"journal-article","created":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T11:03:26Z","timestamp":1584961406000},"page":"187-227","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["PuRSUE -from specification of robotic environments to synthesis of controllers"],"prefix":"10.1145","volume":"32","author":[{"given":"Marcello M.","family":"Bersani","sequence":"first","affiliation":[{"name":"Dipartimento di Elettronica, Informazione e Bioingegneria, Politecnico di Milano, Milan, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matteo","family":"Soldo","sequence":"additional","affiliation":[{"name":"Dipartimento di Elettronica, Informazione e Bioingegneria, Politecnico di Milano, Milan, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Claudio","family":"Menghi","sequence":"additional","affiliation":[{"name":"SnT - University of Luxembourg, Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Patrizio","family":"Pelliccione","sequence":"additional","affiliation":[{"name":"Chalmers | University of Gothenburg, Gothenburg, Sweden"},{"name":"University of L\u2019Aquila, L\u2019Aquila, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[{"name":"Dipartimento di Meccanica, Politecnico di Milano, Milan, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1024"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Asarin E Maler O Pnueli A (1995) Symbolic controller synthesis for discrete and timed systems. In: Hybrid Systems II. Springer","DOI":"10.1007\/3-540-60472-3_1"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Askarpour M Mandrioli D Rossi M Vicentini F (2017) Modeling operator behavior in the safety analysis of collaborative robotic applications. In: Computer safety reliability and security. Springer pp 89\u2013104","DOI":"10.1007\/978-3-319-66266-4_6"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.rcim.2019.01.001"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Behrmann G Cougnard A David A Fleury E Larsen KG Lime D (2007) Uppaal-tiga: time for playing games!. In: Computer aided verification. Springer pp 121\u2013125","DOI":"10.1007\/978-3-540-73368-3_14"},{"issue":"4","key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","first-page":"3332","DOI":"10.1109\/LRA.2019.2926669","article-title":"Guiding autonomous exploration with signal temporal logic","volume":"4","author":"Barbosa FS","year":"2019","journal-title":"IEEE Robot Autom Lett"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Behrmann G David A Larsen KG (2004) A tutorial on uppaal. In: Formal methods for the design of real-time systems. Springer pp 200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bouyer P (2009) Model-checking timed temporal logics. In: Electronic notes in theoretical computer science. pp 231:323\u2013341. Workshop on Methods for Modalities (M4M5 2007)","DOI":"10.1016\/j.entcs.2009.02.044"},{"issue":"2","key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1109\/MAES.2007.323296","article-title":"Coordinated continual planning methods for cooperating rovers","volume":"22","author":"Barrett A","year":"2007","journal-title":"IEEE Aerosp Electron Syst Mag"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Bozhinoski D Ruscio DD Malavolta I Pelliccione P Tivoli M (2015) FLYAQ: enabling non-expert users to specify and generate missions of autonomous multicopters. In: International conference on automated software engineering. IEEE pp 801\u2013806","DOI":"10.1109\/ASE.2015.104"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0229-y"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90088-5"},{"key":"e_1_2_1_2_14_2","unstructured":"Ceballos A Bensalem S Cesta A de\u00a0Silva L Fratini S Ingrand F Oc\u00f3n J Orlandini A Py F Rajan K Rasconi R van Winnendael M (2011) A goal oriented autonomous controller for space exploration. http:\/\/robotics.estec.esa.int\/ASTRA\/Astra2011\/Astra2011_Proceedings.zip1"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Cassez F David A Fleury E Larsen KG Lime D (2005) Efficient on-the-fly algorithms for the analysis of timed games. In: Concurrency theory. Springer pp 66\u201380","DOI":"10.1007\/11539452_9"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.06.002"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Chen T Forejt V Kwiatkowska M Parker D Simaitis A (2013) Prism-games: a model checker for stochastic multi-player games. In: International conference on TOOLS and algorithms for the construction and analysis of systems. Springer pp 185\u2013191","DOI":"10.1007\/978-3-642-36742-7_13"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Cimatti A Hunsberger L Micheli A Roveri M (2014) Using timed game automata to synthesize execution strategies for simple temporal networks with uncertainty. In: AAAI. AAAI Press pp 2242\u20132249","DOI":"10.1609\/aaai.v28i1.9040"},{"key":"e_1_2_1_2_20_2","unstructured":"Cassez F Larsen KG Raskin JF Reynier PA (2011) Timed controller synthesis: an industrial case study. Deliverable no.: D5. 12 Title of Deliverable: Industrial Handbook p 150"},{"key":"e_1_2_1_2_21_2","unstructured":"Cesta A Orlandini A Umbrico A (2013) Toward a general purpose software environment for timeline-based planning. https:\/\/core.ac.uk\/download\/pdf\/37835325.pdf"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2016.2613642"},{"issue":"8","key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","first-page":"974","DOI":"10.1016\/S1474-6670(17)32107-9","article-title":"Stochastic discrete event model of a multi-robot team playing an adversarial game","volume":"37","author":"Damas B","year":"2004","journal-title":"IFAC Proc"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCB.2004.832155"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Finucane C Jing G Kress-Gazit H (2010) LTLMoP: Experimenting with language temporal logic and robot control. In: Intelligent Robots and Systems. IEEE pp 1988\u20131993","DOI":"10.1109\/IROS.2010.5650371"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Farrell M Luckcuck M Fisher M (2018) Robotics and integrated formal methods: necessity meets opportunity. In: Integrated formal methods. Springer pp 161\u2013171","DOI":"10.1007\/978-3-319-98938-9_10"},{"key":"e_1_2_1_2_27_2","unstructured":"Foote T Wise M (2019) Turtlebot home page Last access 27 March https:\/\/www.turtlebot.com\/"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Gainer P Dixon C Dautenhahn K Fisher M Hustadt U Saunders J Webster M (2017) Cruton: automatic verification of a robotic assistant's behaviours. In: Critical systems: formal methods and automated verification. Springer pp 119\u2013133","DOI":"10.1007\/978-3-319-67113-0_8"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"G\u00f6tz S Leuth\u00e4user M Reimann J Schroeter J Wende C Wilke C A\u00dfmann U (2011) A role-based language for collaborative robot applications. In: International symposium on leveraging applications of formal methods verification and validation. Springer pp 1\u201315","DOI":"10.1007\/978-3-642-34781-8_1"},{"key":"e_1_2_1_2_30_2","unstructured":"Gigante N Montanari A Mayer MC Orlandini A Reynolds M (2018) A game-theoretic approach to timeline-based planning with uncertainty. arXiv preprint arXiv:1807.04837"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Garc\u00eda S Pelliccione P Menghi C Berger T Bures T (2019) High-level mission specification for multiple robots. In: International conference on software language engineering. ACM pp 127\u2013140","DOI":"10.1145\/3357766.3359535"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Jessen JJ Rasmussen JI Larsen KG David A (2007) Guided controller synthesis for climate controller using uppaal tiga. In: Formal modeling and analysis of timed systems. Springer pp 227\u2013240","DOI":"10.1007\/978-3-540-75454-1_17"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Konur S Dixon C Fisher M (2010) Formal verification of probabilistic swarm behaviours. In: International conference on swarm intelligence. Springer pp 440\u2013447","DOI":"10.1007\/978-3-642-15461-4_42"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-control-060117-104838"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. In: Computer aided verification. Springer pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Kunze L Roehm T Beetz M (2011) Towards semantic robot description languages. In: International conference on robotics and automation. IEEE pp 5589\u20135595","DOI":"10.1109\/ICRA.2011.5980170"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Luckcuck M Farrell M Dennis LA Dixon C Fisher M (2019) Formal specification and verification of autonomous robotic systems: a survey. ACM Comput Surv 52(5):100:1\u2013100:41","DOI":"10.1145\/3342355"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Largou\u00ebt C Krichen O Zhao Y (2016) Temporal planning with extended timed automata. In: International conference on tools with artificial intelligence. IEEE pp 522\u2013529","DOI":"10.1109\/ICTAI.2016.0086"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10514-014-9418-8"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Loetzsch M Risler M J\u00fcngel M (2006) XABSL-A pragmatic approach to behavior engineering. In: International Conference on Intelligent Robots and Systems. IEEE\/RSG pp 5124\u20135129","DOI":"10.1109\/IROS.2006.282605"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11721-016-0119-0"},{"key":"e_1_2_1_2_42_2","unstructured":"Morse J Araiza-Illan D Lawry J Richards A Eder K (2016) Formal specification and analysis of autonomous systems under partial compliance. arXiv preprint arXiv:1603.01082"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Menghi C Garc\u00eda S Pelliccione P T\u016fmov\u00e1 J (2018) Multi-robot LTL planning under uncertainty. In: International symposium on formal methods. Springer pp 399\u2013417","DOI":"10.1007\/978-3-319-95582-7_24"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Menghi C Garc\u00eda S Pelliccione P T\u016fmov\u00e1 J (2018) Towards multi-robot applications planning under uncertainty. In: International conference on software engineering: companion proceeedings. ACM pp 438\u2013439","DOI":"10.1145\/3183440.3195046"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Mayer MC Orlandini A (2015) An executable semantics of flexible plans in terms of timed game automata. In: Temporal Representation and Reasoning. IEEE pp 160\u2013169","DOI":"10.1109\/TIME.2015.16"},{"key":"e_1_2_1_2_46_2","unstructured":"Maoz S Ringert JO (2019) Spectra. http:\/\/smlab.cs.tau.ac.il\/syntech\/spectra\/userguide.pdf"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Miyazawa A Ribeiro P Li W Cavalcanti A Timmis J (2017) Automatic property checking of robotic applications. In: International conference on intelligent robots and systems. IEEE\/RJS pp 3869\u20133876","DOI":"10.1109\/IROS.2017.8206238"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Miyazawa A Ribeiro P Li W Cavalcanti A Timmis J Woodcock J (2019) RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw Syst Model","DOI":"10.1007\/s10270-018-00710-z"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Menghi C Tsigkanos C Berger T Pelliccione P Ghezzi C (2018) Poster: property specification patterns for robotic missions. In: International conference on software engineering: companion proceeedings. IEEE\/ACM pp 434\u2013435","DOI":"10.1145\/3183440.3195044"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Menghi C Tsigkanos C Berger T Pelliccione P (2019) Psalm: specification of dependable robotic missions. In: International conference on software engineering: companion proceedings. IEEE\/ACM pp 99\u2013102","DOI":"10.1109\/ICSE-Companion.2019.00048"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Menghi C Tsigkanos C Pelliccione P Ghezzi C Berger T (2019) Specification patterns for robotic missions. IEEE Trans Softw Eng pp 1\u20131","DOI":"10.1145\/3183440.3195044"},{"key":"e_1_2_1_2_52_2","unstructured":"https:\/\/www.ald.softbankrobotics.com\/en\/robots\/nao\/find-out-more-about-nao"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Nordmann A Hochgeschwender N Wrede S (2014) A survey on domain-specific languages in robotics. In: International Conference on Simulation Modeling and Programming for Autonomous Robots. Springer pp 195\u2013206","DOI":"10.1007\/978-3-319-11900-7_17"},{"key":"e_1_2_1_2_54_2","unstructured":"Orlandini A Finzi A Cesta A Fratini S Tronci E (2011) Enriching apsi with validation capabilities: The keen environment and its use in robotics. In: Advanced Space Technologies in Robotics and Automation. http:\/\/robotics.estec.esa.int\/ASTRA\/Astra2011\/Astra2011_Proceedings.zip1"},{"key":"e_1_2_1_2_55_2","unstructured":"Online appendix (2019) https:\/\/drive.google.com\/drive\/folders\/117-MVWDYYo-6Gir6KAzlVTsvshGu2Uvf"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Peter H Ehlers R Mattm\u00fcller R (2011) Synthia: Verification and synthesis for timed automata. In: International conference on computer aided verification. Springer pp 649\u2013655","DOI":"10.1007\/978-3-642-22110-1_52"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Pinheiro LP Lopes YK Leal AB Junior RS (2015) Nadzoru: a software tool for supervisory control of discrete event systems. IFAC-PapersOnLine 48(7):182 \u2013 187. International Workshop on Dependable Control of Discrete Systems","DOI":"10.1016\/j.ifacol.2015.06.491"},{"key":"e_1_2_1_2_58_2","unstructured":"PuRSUE - Planner for RobotS in Uncontrollable Environments (2019). https:\/\/github.com\/deib-polimi\/PuRSUE"},{"key":"e_1_2_1_2_59_2","unstructured":"Quigley M Conley K Gerkey B Faust J Foote T Leibs J Wheeler R Ng AY (2009) ROS: an open-source robot operating system. In: ICRA workshop on open source software vol\u00a03. IEEE p\u00a05"},{"key":"e_1_2_1_2_60_2","unstructured":"Quattrini\u00a0Li A Fioratto R Amigoni F Isler V (2018) A search-based approach to solve pursuit-evasion games with limited visibility in polygonal environments. In: International conference on autonomous agents and multiAgent systems. ACM pp 1693\u20131701"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Rugg-Gunn N Cameron S (1994) A formal semantics for multiple vehicle task and motion planning. In: International conference on robotics and automation. IEEE pp 2464\u20132469","DOI":"10.1109\/ROBOT.1994.351142"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"crossref","unstructured":"Ruscio DD Malavolta I Pelliccione P Tivoli M (2016) Automatic generation of detailed flight plans from high-level mission descriptions. In: International conference on model driven engineering languages and systems. ACM pp 45\u201355","DOI":"10.1145\/2976767.2976794"},{"key":"e_1_2_1_2_63_2","doi-asserted-by":"publisher","DOI":"10.5555\/3002858"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"crossref","unstructured":"T\u016fmov\u00e1 J Dimarogonas DV (2014) A receding horizon approach to multi-agent planning from local LTL specifications. In: 2014 American Control Conference. IEEE pp 1775\u20131780","DOI":"10.1109\/ACC.2014.6859413"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2016.04.006"},{"key":"e_1_2_1_2_66_2","unstructured":"Truszkowski W Rash J Hinchey M Rouff C. A survey of formal methods for intelligent swarms. https:\/\/ntrs.nasa.gov\/archive\/nasa\/casi.ntrs.nasa.gov\/20050156631.pdf"},{"issue":"6","key":"e_1_2_1_2_67_2","first-page":"2863","article-title":"Pursuit algorithm for robot trash can based on fuzzy-cell decomposition","volume":"6","author":"Tunggal TP","year":"2016","journal-title":"Int J Electr Comput Eng"},{"issue":"1","key":"e_1_2_1_2_68_2","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1109\/TRO.2019.2937471","article-title":"Safety assessment of collaborative robotics through automated formal verification","volume":"31","author":"Vicentini F","year":"2020","journal-title":"IEEE Trans Robot"},{"key":"e_1_2_1_2_69_2","unstructured":"Ecobot. https:\/\/youtu.be\/w6SfCmgdCsk https:\/\/youtu.be\/XmOY-urEDD0"},{"key":"e_1_2_1_2_70_2","doi-asserted-by":"crossref","unstructured":"Verginis CK Vrohidis C Bechlioulis CP Kyriakopoulos KJ Dimarogonas DV (2019) Reconfigurable motion planning and control in obstacle cluttered environments under timed temporal tasks. In: International Conference on Robotics and Automation. IEEE pp 951\u2013957","DOI":"10.1109\/ICRA.2019.8794000"},{"key":"e_1_2_1_2_71_2","unstructured":"International Federation of Robotics . https:\/\/ifr.org\/worldrobotics\/"},{"issue":"3","key":"e_1_2_1_2_72_2","doi-asserted-by":"crossref","first-page":"1003","DOI":"10.1109\/TCNS.2017.2670330","article-title":"Compositional abstraction for networks of control systems: a dissipativity approach","volume":"5","author":"Zamani M","year":"2018","journal-title":"IEEE Trans Control Netw Syst"},{"issue":"7","key":"e_1_2_1_2_73_2","doi-asserted-by":"crossref","first-page":"1804","DOI":"10.1109\/TAC.2011.2176409","article-title":"Symbolic models for nonlinear control systems without stability assumptions","volume":"57","author":"Zamani M","year":"2011","journal-title":"Trans Autom Control"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00509-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-020-00509-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00509-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-020-00509-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T14:15:35Z","timestamp":1666188935000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-020-00509-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7]]},"references-count":73,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2020,7]]}},"alternative-id":["10.1007\/s00165-020-00509-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-020-00509-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,7]]},"assertion":[{"value":"1 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 February 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 March 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}