--- _id: '5959' abstract: - lang: eng text: Formalizing properties of systems with continuous dynamics is a challenging task. In this paper, we propose a formal framework for specifying and monitoring rich temporal properties of real-valued signals. We introduce signal first-order logic (SFO) as a specification language that combines first-order logic with linear-real arithmetic and unary function symbols interpreted as piecewise-linear signals. We first show that while the satisfiability problem for SFO is undecidable, its membership and monitoring problems are decidable. We develop an offline monitoring procedure for SFO that has polynomial complexity in the size of the input trace and the specification, for a fixed number of quantifiers and function symbols. We show that the algorithm has computation time linear in the size of the input trace for the important fragment of bounded-response specifications interpreted over input traces with finite variability. We can use our results to extend signal temporal logic with first-order quantifiers over time and value parameters, while preserving its efficient monitoring. We finally demonstrate the practical appeal of our logic through a case study in the micro-electronics domain. article_processing_charge: No author: - first_name: Alexey full_name: Bakhirkin, Alexey last_name: Bakhirkin - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Deian full_name: Nickovicl, Deian last_name: Nickovicl citation: ama: 'Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. Keynote: The first-order logic of signals. In: 2018 International Conference on Embedded Software. IEEE; 2018:1-10. doi:10.1109/emsoft.2018.8537203' apa: 'Bakhirkin, A., Ferrere, T., Henzinger, T. A., & Nickovicl, D. (2018). Keynote: The first-order logic of signals. In 2018 International Conference on Embedded Software (pp. 1–10). Turin, Italy: IEEE. https://doi.org/10.1109/emsoft.2018.8537203' chicago: 'Bakhirkin, Alexey, Thomas Ferrere, Thomas A Henzinger, and Deian Nickovicl. “Keynote: The First-Order Logic of Signals.” In 2018 International Conference on Embedded Software, 1–10. IEEE, 2018. https://doi.org/10.1109/emsoft.2018.8537203.' ieee: 'A. Bakhirkin, T. Ferrere, T. A. Henzinger, and D. Nickovicl, “Keynote: The first-order logic of signals,” in 2018 International Conference on Embedded Software, Turin, Italy, 2018, pp. 1–10.' ista: 'Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. 2018. Keynote: The first-order logic of signals. 2018 International Conference on Embedded Software. EMSOFT: International Conference on Embedded Software, 1–10.' mla: 'Bakhirkin, Alexey, et al. “Keynote: The First-Order Logic of Signals.” 2018 International Conference on Embedded Software, IEEE, 2018, pp. 1–10, doi:10.1109/emsoft.2018.8537203.' short: A. Bakhirkin, T. Ferrere, T.A. Henzinger, D. Nickovicl, in:, 2018 International Conference on Embedded Software, IEEE, 2018, pp. 1–10. conference: end_date: 2018-10-05 location: Turin, Italy name: 'EMSOFT: International Conference on Embedded Software' start_date: 2018-09-30 date_created: 2019-02-13T09:19:28Z date_published: 2018-09-30T00:00:00Z date_updated: 2023-09-19T10:41:29Z day: '30' ddc: - '000' department: - _id: ToHe doi: 10.1109/emsoft.2018.8537203 external_id: isi: - '000492828500005' file: - access_level: open_access checksum: 234a33ad9055b3458fcdda6af251b33a content_type: application/pdf creator: dernst date_created: 2020-05-14T16:01:29Z date_updated: 2020-07-14T12:47:13Z file_id: '7839' file_name: 2018_EMSOFT_Bakhirkin.pdf file_size: 338006 relation: main_file file_date_updated: 2020-07-14T12:47:13Z has_accepted_license: '1' isi: 1 language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: 1-10 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: 2018 International Conference on Embedded Software publication_identifier: isbn: - '9781538655603' publication_status: published publisher: IEEE quality_controlled: '1' scopus_import: '1' status: public title: 'Keynote: The first-order logic of signals' type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 year: '2018' ... --- _id: '5962' abstract: - lang: eng text: Stochastic Gradient Descent (SGD) is a fundamental algorithm in machine learning, representing the optimization backbone for training several classic models, from regression to neural networks. Given the recent practical focus on distributed machine learning, significant work has been dedicated to the convergence properties of this algorithm under the inconsistent and noisy updates arising from execution in a distributed environment. However, surprisingly, the convergence properties of this classic algorithm in the standard shared-memory model are still not well-understood. In this work, we address this gap, and provide new convergence bounds for lock-free concurrent stochastic gradient descent, executing in the classic asynchronous shared memory model, against a strong adaptive adversary. Our results give improved upper and lower bounds on the "price of asynchrony'' when executing the fundamental SGD algorithm in a concurrent setting. They show that this classic optimization tool can converge faster and with a wider range of parameters than previously known under asynchronous iterations. At the same time, we exhibit a fundamental trade-off between the maximum delay in the system and the rate at which SGD can converge, which governs the set of parameters under which this algorithm can still work efficiently. article_processing_charge: No author: - first_name: Dan-Adrian full_name: Alistarh, Dan-Adrian id: 4A899BFC-F248-11E8-B48F-1D18A9856A87 last_name: Alistarh orcid: 0000-0003-3650-940X - first_name: Christopher full_name: De Sa, Christopher last_name: De Sa - first_name: Nikola H full_name: Konstantinov, Nikola H id: 4B9D76E4-F248-11E8-B48F-1D18A9856A87 last_name: Konstantinov citation: ama: 'Alistarh D-A, De Sa C, Konstantinov NH. The convergence of stochastic gradient descent in asynchronous shared memory. In: Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18. ACM Press; 2018:169-178. doi:10.1145/3212734.3212763' apa: 'Alistarh, D.-A., De Sa, C., & Konstantinov, N. H. (2018). The convergence of stochastic gradient descent in asynchronous shared memory. In Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18 (pp. 169–178). Egham, United Kingdom: ACM Press. https://doi.org/10.1145/3212734.3212763' chicago: Alistarh, Dan-Adrian, Christopher De Sa, and Nikola H Konstantinov. “The Convergence of Stochastic Gradient Descent in Asynchronous Shared Memory.” In Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18, 169–78. ACM Press, 2018. https://doi.org/10.1145/3212734.3212763. ieee: D.-A. Alistarh, C. De Sa, and N. H. Konstantinov, “The convergence of stochastic gradient descent in asynchronous shared memory,” in Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18, Egham, United Kingdom, 2018, pp. 169–178. ista: 'Alistarh D-A, De Sa C, Konstantinov NH. 2018. The convergence of stochastic gradient descent in asynchronous shared memory. Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18. PODC: Principles of Distributed Computing, 169–178.' mla: Alistarh, Dan-Adrian, et al. “The Convergence of Stochastic Gradient Descent in Asynchronous Shared Memory.” Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18, ACM Press, 2018, pp. 169–78, doi:10.1145/3212734.3212763. short: D.-A. Alistarh, C. De Sa, N.H. Konstantinov, in:, Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18, ACM Press, 2018, pp. 169–178. conference: end_date: 2018-07-27 location: Egham, United Kingdom name: 'PODC: Principles of Distributed Computing' start_date: 2018-07-23 date_created: 2019-02-13T09:58:58Z date_published: 2018-07-23T00:00:00Z date_updated: 2023-09-19T10:42:53Z day: '23' department: - _id: DaAl doi: 10.1145/3212734.3212763 external_id: arxiv: - '1803.08841' isi: - '000458186900022' isi: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1803.08841 month: '07' oa: 1 oa_version: Preprint page: 169-178 publication: Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing - PODC '18 publication_identifier: isbn: - '9781450357951' publication_status: published publisher: ACM Press quality_controlled: '1' scopus_import: '1' status: public title: The convergence of stochastic gradient descent in asynchronous shared memory type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 year: '2018' ... --- _id: '5860' abstract: - lang: eng text: 'A major problem for evolutionary theory is understanding the so-called open-ended nature of evolutionary change, from its definition to its origins. Open-ended evolution (OEE) refers to the unbounded increase in complexity that seems to characterize evolution on multiple scales. This property seems to be a characteristic feature of biological and technological evolution and is strongly tied to the generative potential associated with combinatorics, which allows the system to grow and expand their available state spaces. Interestingly, many complex systems presumably displaying OEE, from language to proteins, share a common statistical property: the presence of Zipf''s Law. Given an inventory of basic items (such as words or protein domains) required to build more complex structures (sentences or proteins) Zipf''s Law tells us that most of these elements are rare whereas a few of them are extremely common. Using algorithmic information theory, in this paper we provide a fundamental definition for open-endedness, which can be understood as postulates. Its statistical counterpart, based on standard Shannon information theory, has the structure of a variational problem which is shown to lead to Zipf''s Law as the expected consequence of an evolutionary process displaying OEE. We further explore the problem of information conservation through an OEE process and we conclude that statistical information (standard Shannon information) is not conserved, resulting in the paradoxical situation in which the increase of information content has the effect of erasing itself. We prove that this paradox is solved if we consider non-statistical forms of information. This last result implies that standard information theory may not be a suitable theoretical framework to explore the persistence and increase of the information content in OEE systems.' article_number: '20180395' article_processing_charge: No author: - first_name: Bernat full_name: Corominas-Murtra, Bernat id: 43BE2298-F248-11E8-B48F-1D18A9856A87 last_name: Corominas-Murtra orcid: 0000-0001-9806-5643 - first_name: Luís F. full_name: Seoane, Luís F. last_name: Seoane - first_name: Ricard full_name: Solé, Ricard last_name: Solé citation: ama: Corominas-Murtra B, Seoane LF, Solé R. Zipf’s Law, unbounded complexity and open-ended evolution. Journal of the Royal Society Interface. 2018;15(149). doi:10.1098/rsif.2018.0395 apa: Corominas-Murtra, B., Seoane, L. F., & Solé, R. (2018). Zipf’s Law, unbounded complexity and open-ended evolution. Journal of the Royal Society Interface. Royal Society Publishing. https://doi.org/10.1098/rsif.2018.0395 chicago: Corominas-Murtra, Bernat, Luís F. Seoane, and Ricard Solé. “Zipf’s Law, Unbounded Complexity and Open-Ended Evolution.” Journal of the Royal Society Interface. Royal Society Publishing, 2018. https://doi.org/10.1098/rsif.2018.0395. ieee: B. Corominas-Murtra, L. F. Seoane, and R. Solé, “Zipf’s Law, unbounded complexity and open-ended evolution,” Journal of the Royal Society Interface, vol. 15, no. 149. Royal Society Publishing, 2018. ista: Corominas-Murtra B, Seoane LF, Solé R. 2018. Zipf’s Law, unbounded complexity and open-ended evolution. Journal of the Royal Society Interface. 15(149), 20180395. mla: Corominas-Murtra, Bernat, et al. “Zipf’s Law, Unbounded Complexity and Open-Ended Evolution.” Journal of the Royal Society Interface, vol. 15, no. 149, 20180395, Royal Society Publishing, 2018, doi:10.1098/rsif.2018.0395. short: B. Corominas-Murtra, L.F. Seoane, R. Solé, Journal of the Royal Society Interface 15 (2018). date_created: 2019-01-20T22:59:19Z date_published: 2018-12-12T00:00:00Z date_updated: 2023-09-19T10:40:38Z day: '12' department: - _id: EdHa doi: 10.1098/rsif.2018.0395 external_id: arxiv: - '1612.01605' isi: - '000456783800002' intvolume: ' 15' isi: 1 issue: '149' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1612.01605 month: '12' oa: 1 oa_version: Preprint publication: Journal of the Royal Society Interface publication_identifier: issn: - '17425689' publication_status: published publisher: Royal Society Publishing quality_controlled: '1' scopus_import: '1' status: public title: Zipf's Law, unbounded complexity and open-ended evolution type: journal_article user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 15 year: '2018' ... --- _id: '5961' abstract: - lang: eng text: "The area of machine learning has made considerable progress over the past decade, enabled by the widespread availability of large datasets, as well as by improved algorithms and models. Given the large computational demands of machine learning workloads, parallelism, implemented either through single-node concurrency or through multi-node distribution, has been a third key ingredient to advances in machine learning.\r\nThe goal of this tutorial is to provide the audience with an overview of standard distribution techniques in machine learning, with an eye towards the intriguing trade-offs between synchronization and communication costs of distributed machine learning algorithms, on the one hand, and their convergence, on the other.The tutorial will focus on parallelization strategies for the fundamental stochastic gradient descent (SGD) algorithm, which is a key tool when training machine learning models, from classical instances such as linear regression, to state-of-the-art neural network architectures.\r\nThe tutorial will describe the guarantees provided by this algorithm in the sequential case, and then move on to cover both shared-memory and message-passing parallelization strategies, together with the guarantees they provide, and corresponding trade-offs. The presentation will conclude with a broad overview of ongoing research in distributed and concurrent machine learning. The tutorial will assume no prior knowledge beyond familiarity with basic concepts in algebra and analysis.\r\n" article_processing_charge: No author: - first_name: Dan-Adrian full_name: Alistarh, Dan-Adrian id: 4A899BFC-F248-11E8-B48F-1D18A9856A87 last_name: Alistarh orcid: 0000-0003-3650-940X citation: ama: 'Alistarh D-A. A brief tutorial on distributed and concurrent machine learning. In: Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18. ACM Press; 2018:487-488. doi:10.1145/3212734.3212798' apa: 'Alistarh, D.-A. (2018). A brief tutorial on distributed and concurrent machine learning. In Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18 (pp. 487–488). Egham, United Kingdom: ACM Press. https://doi.org/10.1145/3212734.3212798' chicago: Alistarh, Dan-Adrian. “A Brief Tutorial on Distributed and Concurrent Machine Learning.” In Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18, 487–88. ACM Press, 2018. https://doi.org/10.1145/3212734.3212798. ieee: D.-A. Alistarh, “A brief tutorial on distributed and concurrent machine learning,” in Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18, Egham, United Kingdom, 2018, pp. 487–488. ista: 'Alistarh D-A. 2018. A brief tutorial on distributed and concurrent machine learning. Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18. PODC: Principles of Distributed Computing, 487–488.' mla: Alistarh, Dan-Adrian. “A Brief Tutorial on Distributed and Concurrent Machine Learning.” Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18, ACM Press, 2018, pp. 487–88, doi:10.1145/3212734.3212798. short: D.-A. Alistarh, in:, Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing  - PODC ’18, ACM Press, 2018, pp. 487–488. conference: end_date: 2018-07-27 location: Egham, United Kingdom name: 'PODC: Principles of Distributed Computing' start_date: 2018-07-23 date_created: 2019-02-13T09:48:55Z date_published: 2018-07-27T00:00:00Z date_updated: 2023-09-19T10:42:28Z day: '27' department: - _id: DaAl doi: 10.1145/3212734.3212798 external_id: isi: - '000458186900063' isi: 1 language: - iso: eng month: '07' oa_version: None page: 487-488 publication: Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing - PODC '18 publication_identifier: isbn: - '9781450357951' publication_status: published publisher: ACM Press quality_controlled: '1' scopus_import: '1' status: public title: A brief tutorial on distributed and concurrent machine learning type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 year: '2018' ... --- _id: '5960' abstract: - lang: eng text: In this paper we present a reliable method to verify the existence of loops along the uncertain trajectory of a robot, based on proprioceptive measurements only, within a bounded-error context. The loop closure detection is one of the key points in simultaneous localization and mapping (SLAM) methods, especially in homogeneous environments with difficult scenes recognitions. The proposed approach is generic and could be coupled with conventional SLAM algorithms to reliably reduce their computing burden, thus improving the localization and mapping processes in the most challenging environments such as unexplored underwater extents. To prove that a robot performed a loop whatever the uncertainties in its evolution, we employ the notion of topological degree that originates in the field of differential topology. We show that a verification tool based on the topological degree is an optimal method for proving robot loops. This is demonstrated both on datasets from real missions involving autonomous underwater vehicles and by a mathematical discussion. article_processing_charge: No author: - first_name: Simon full_name: Rohou, Simon last_name: Rohou - first_name: Peter full_name: Franek, Peter id: 473294AE-F248-11E8-B48F-1D18A9856A87 last_name: Franek orcid: 0000-0001-8878-8397 - first_name: Clément full_name: Aubry, Clément last_name: Aubry - first_name: Luc full_name: Jaulin, Luc last_name: Jaulin citation: ama: Rohou S, Franek P, Aubry C, Jaulin L. Proving the existence of loops in robot trajectories. The International Journal of Robotics Research. 2018;37(12):1500-1516. doi:10.1177/0278364918808367 apa: Rohou, S., Franek, P., Aubry, C., & Jaulin, L. (2018). Proving the existence of loops in robot trajectories. The International Journal of Robotics Research. SAGE Publications. https://doi.org/10.1177/0278364918808367 chicago: Rohou, Simon, Peter Franek, Clément Aubry, and Luc Jaulin. “Proving the Existence of Loops in Robot Trajectories.” The International Journal of Robotics Research. SAGE Publications, 2018. https://doi.org/10.1177/0278364918808367. ieee: S. Rohou, P. Franek, C. Aubry, and L. Jaulin, “Proving the existence of loops in robot trajectories,” The International Journal of Robotics Research, vol. 37, no. 12. SAGE Publications, pp. 1500–1516, 2018. ista: Rohou S, Franek P, Aubry C, Jaulin L. 2018. Proving the existence of loops in robot trajectories. The International Journal of Robotics Research. 37(12), 1500–1516. mla: Rohou, Simon, et al. “Proving the Existence of Loops in Robot Trajectories.” The International Journal of Robotics Research, vol. 37, no. 12, SAGE Publications, 2018, pp. 1500–16, doi:10.1177/0278364918808367. short: S. Rohou, P. Franek, C. Aubry, L. Jaulin, The International Journal of Robotics Research 37 (2018) 1500–1516. date_created: 2019-02-13T09:36:20Z date_published: 2018-10-24T00:00:00Z date_updated: 2023-09-19T10:41:59Z day: '24' department: - _id: UlWa doi: 10.1177/0278364918808367 external_id: arxiv: - '1712.01341' isi: - '000456881100004' intvolume: ' 37' isi: 1 issue: '12' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1712.01341 month: '10' oa: 1 oa_version: Preprint page: 1500-1516 publication: The International Journal of Robotics Research publication_identifier: eissn: - 1741-3176 issn: - 0278-3649 publication_status: published publisher: SAGE Publications quality_controlled: '1' scopus_import: '1' status: public title: Proving the existence of loops in robot trajectories type: journal_article user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 37 year: '2018' ...