Showing 1–50 of 69 results for author: Jacobs, S

Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata

Authors: Tom Baumeister, Paul Eichler, Swen Jacobs, Mouhammad Sakr, Marcus Völp

Abstract: Threshold automata are a computational model that has proven to be versatile in modeling threshold-based distributed algorithms and enabling their completely automatic parameterized verification. We present novel techniques for the verification of threshold automata, based on well-structured transition systems, that allow us to extend the expressiveness of both the computational model and the spec… ▽ More Threshold automata are a computational model that has proven to be versatile in modeling threshold-based distributed algorithms and enabling their completely automatic parameterized verification. We present novel techniques for the verification of threshold automata, based on well-structured transition systems, that allow us to extend the expressiveness of both the computational model and the specifications that can be verified. In particular, we extend the model to allow decrements and resets of shared variables, possibly on cycles, and the specifications to general coverability. While these extensions of the model in general lead to undecidability, our algorithms provide a semi-decision procedure. We demonstrate the benefit of our extensions by showing that we can model complex round-based algorithms such as the phase king consensus algorithm and the Red Belly Blockchain protocol (published in 2019), and verify them fully automatically for the first time. △ Less

Submitted 28 June, 2024; originally announced June 2024.

Universal Checkpointing: Efficient and Flexible Checkpointing for Large Scale Distributed Training

Authors: Xinyu Lian, Sam Ade Jacobs, Lev Kurilenko, Masahiro Tanaka, Stas Bekman, Olatunji Ruwase, Minjia Zhang

Abstract: Existing checkpointing approaches seem ill-suited for distributed training even though hardware limitations make model parallelism, i.e., sharding model state across multiple accelerators, a requirement for model scaling. Consolidating distributed model state into a single checkpoint unacceptably slows down training, and is impractical at extreme scales. Distributed checkpoints, in contrast, are t… ▽ More Existing checkpointing approaches seem ill-suited for distributed training even though hardware limitations make model parallelism, i.e., sharding model state across multiple accelerators, a requirement for model scaling. Consolidating distributed model state into a single checkpoint unacceptably slows down training, and is impractical at extreme scales. Distributed checkpoints, in contrast, are tightly coupled to the model parallelism and hardware configurations of the training run, and thus unusable on different configurations. To address this problem, we propose Universal Checkpointing, a technique that enables efficient checkpoint creation while providing the flexibility of resuming on arbitrary parallelism strategy and hardware configurations. Universal Checkpointing unlocks unprecedented capabilities for large-scale training such as improved resilience to hardware failures through continued training on remaining healthy hardware, and reduced training time through opportunistic exploitation of elastic capacity. The key insight of Universal Checkpointing is the selection of the optimal representation in each phase of the checkpointing life cycle: distributed representation for saving, and consolidated representation for loading. This is achieved using two key mechanisms. First, the universal checkpoint format, which consists of a consolidated representation of each model parameter and metadata for map** parameter fragments into training ranks of arbitrary model-parallelism configuration. Second, the universal checkpoint language, a simple but powerful specification language for converting distributed checkpoints into the universal checkpoint format. Our evaluation demonstrates the effectiveness and generality of Universal Checkpointing on state-of-the-art model architectures and a wide range of parallelism techniques. △ Less

Submitted 27 June, 2024; v1 submitted 26 June, 2024; originally announced June 2024.

Leveraging Lecture Content for Improved Feedback: Explorations with GPT-4 and Retrieval Augmented Generation

Authors: Sven Jacobs, Steffen Jaschke

Abstract: This paper presents the use of Retrieval Augmented Generation (RAG) to improve the feedback generated by Large Language Models for programming tasks. For this purpose, corresponding lecture recordings were transcribed and made available to the Large Language Model GPT-4 as external knowledge source together with timestamps as metainformation by using RAG. The purpose of this is to prevent hallucin… ▽ More This paper presents the use of Retrieval Augmented Generation (RAG) to improve the feedback generated by Large Language Models for programming tasks. For this purpose, corresponding lecture recordings were transcribed and made available to the Large Language Model GPT-4 as external knowledge source together with timestamps as metainformation by using RAG. The purpose of this is to prevent hallucinations and to enforce the use of the technical terms and phrases from the lecture. In an exercise platform developed to solve programming problems for an introductory programming lecture, students can request feedback on their solutions generated by GPT-4. For this task GPT-4 receives the students' code solution, the compiler output, the result of unit tests and the relevant passages from the lecture notes available through the use of RAG as additional context. The feedback generated by GPT-4 should guide students to solve problems independently and link to the lecture content, using the time stamps of the transcript as meta-information. In this way, the corresponding lecture videos can be viewed immediately at the corresponding positions. For the evaluation, students worked with the tool in a workshop and decided for each feedback whether it should be extended by RAG or not. First results based on a questionnaire and the collected usage data show that the use of RAG can improve feedback generation and is preferred by students in some situations. Due to the slower speed of feedback generation, the benefits are situation dependent. △ Less

Submitted 5 May, 2024; originally announced May 2024.

Comments: accepted at CSEE&T 2024: 36th International Conference on Software Engineering Education and Training, Würzburg, Germany

Phi-3 Technical Report: A Highly Capable Language Model Locally on Your Phone

Authors: Marah Abdin, Sam Ade Jacobs, Ammar Ahmad Awan, Jyoti Aneja, Ahmed Awadallah, Hany Awadalla, Nguyen Bach, Amit Bahree, Arash Bakhtiari, Jianmin Bao, Harkirat Behl, Alon Benhaim, Misha Bilenko, Johan Bjorck, Sébastien Bubeck, Qin Cai, Martin Cai, Caio César Teodoro Mendes, Weizhu Chen, Vishrav Chaudhary, Dong Chen, Dongdong Chen, Yen-Chun Chen, Yi-Ling Chen, Parul Chopra , et al. (90 additional authors not shown)

Abstract: We introduce phi-3-mini, a 3.8 billion parameter language model trained on 3.3 trillion tokens, whose overall performance, as measured by both academic benchmarks and internal testing, rivals that of models such as Mixtral 8x7B and GPT-3.5 (e.g., phi-3-mini achieves 69% on MMLU and 8.38 on MT-bench), despite being small enough to be deployed on a phone. The innovation lies entirely in our dataset… ▽ More We introduce phi-3-mini, a 3.8 billion parameter language model trained on 3.3 trillion tokens, whose overall performance, as measured by both academic benchmarks and internal testing, rivals that of models such as Mixtral 8x7B and GPT-3.5 (e.g., phi-3-mini achieves 69% on MMLU and 8.38 on MT-bench), despite being small enough to be deployed on a phone. The innovation lies entirely in our dataset for training, a scaled-up version of the one used for phi-2, composed of heavily filtered publicly available web data and synthetic data. The model is also further aligned for robustness, safety, and chat format. We also provide some initial parameter-scaling results with a 7B and 14B models trained for 4.8T tokens, called phi-3-small and phi-3-medium, both significantly more capable than phi-3-mini (e.g., respectively 75% and 78% on MMLU, and 8.7 and 8.9 on MT-bench). Moreover, we also introduce phi-3-vision, a 4.2 billion parameter model based on phi-3-mini with strong reasoning capabilities for image and text prompts. △ Less

Submitted 23 May, 2024; v1 submitted 22 April, 2024; originally announced April 2024.

Comments: 19 pages

Evaluating the Application of Large Language Models to Generate Feedback in Programming Education

Authors: Sven Jacobs, Steffen Jaschke

Abstract: This study investigates the application of large language models, specifically GPT-4, to enhance programming education. The research outlines the design of a web application that uses GPT-4 to provide feedback on programming tasks, without giving away the solution. A web application for working on programming tasks was developed for the study and evaluated with 51 students over the course of one s… ▽ More This study investigates the application of large language models, specifically GPT-4, to enhance programming education. The research outlines the design of a web application that uses GPT-4 to provide feedback on programming tasks, without giving away the solution. A web application for working on programming tasks was developed for the study and evaluated with 51 students over the course of one semester. The results show that most of the feedback generated by GPT-4 effectively addressed code errors. However, challenges with incorrect suggestions and hallucinated issues indicate the need for further improvements. △ Less

Submitted 13 March, 2024; originally announced March 2024.

Comments: accepted at IEEE Global Engineering Education Conference 2024, Kos, Greece

Design and Development of a Multi-Purpose Collaborative Remote Laboratory Platform

Authors: Sven Jacobs, Timo Hardebusch, Esther Franke, Henning Peters, Rashed Al Amin, Veit Wiese, Steffen Jaschke

Abstract: This work-in-progress paper presents the current development of a new collaborative remote laboratory platform. The results are intended to serve as a foundation for future research on collaborative work in remote laboratories. Our platform, standing out with its adaptive and collaborative capabilities, integrates a distributed web-application for streamlined management and engagement in diverse r… ▽ More This work-in-progress paper presents the current development of a new collaborative remote laboratory platform. The results are intended to serve as a foundation for future research on collaborative work in remote laboratories. Our platform, standing out with its adaptive and collaborative capabilities, integrates a distributed web-application for streamlined management and engagement in diverse remote educational environments. △ Less

Submitted 10 March, 2024; originally announced March 2024.

Comments: accepted at IEEE Global Engineering Education Conference 2024, Kos, Greece

BaMn$_2$P$_2$: Highest magnetic ordering temperature 122-pnictide compound

Authors: B. S. Jacobs, Abhishek Pandey

Abstract: We report the growth of high-quality single crystals of ThCr$_2$Si$_2$-type tetragonal BaMn$_2$P$_2$ and investigation of its structural, electrical transport, thermal and magnetic properties. Our results of basal plane electrical resistivity and heat capacity measurements show that the compound has an insulating ground state with a small band gap. Anisotropic susceptibility $χ_{ab,c}(T)$ data inf… ▽ More We report the growth of high-quality single crystals of ThCr$_2$Si$_2$-type tetragonal BaMn$_2$P$_2$ and investigation of its structural, electrical transport, thermal and magnetic properties. Our results of basal plane electrical resistivity and heat capacity measurements show that the compound has an insulating ground state with a small band gap. Anisotropic susceptibility $χ_{ab,c}(T)$ data infer a collinear local-moment Néel-type antiferromagnetic (AFM) ground state below the ordering temperature $T_{\rm N} = 795(15)$~K, which is highest among all the ThCr$_2$Si$_2$- and CaAl$_2$Si$_2$-type 122-pnictide compounds reported so far suggesting that the strength of magnetic exchange interactions is strongest in this material. The magnetic transition temperatures of BaMn$_2$$Pn_{2}$ ($Pn$ = P, As, Sb, Bi) compounds exhibit a monotonic decrease with the increase of tetragonal unit cell parameters $a$ and $c$, suggesting a strong dependence of the strength of the decisive magnetic exchange interactions on the separation between the localized spins residing on the Mn-ions. The observed monotonic increase of both $χ_{ab}$ and $χ_{c}$ for $T > T_{\rm N}$ suggests that short-range dynamic quasi-two dimensional AFM correlations persist above the $T_{\rm N}$ up to the highest temperature of the measurements. The large $T_{\rm N}$ of BaMn$_2$P$_2$ demands for systematic hole-do** studies on this material as similar investigations on related BaMn$_2$As$_{2}$ with $T_{\rm N} = 618$~K have led to the discovery of an outstanding ground state where AFM of localized Mn-spins and itinerant half-metallic ferromagnetism with $T_{\rm c} \approx 100$~K originating from the doped holes coexist together. △ Less

Submitted 9 February, 2024; originally announced February 2024.

Comments: 9 pages, 7 figures

Journal ref: Phys. Rev. Mater. 7, 044410 (2023)

Tracking China's cross-strait bot networks against Taiwan

Authors: Charity S. Jacobs, Lynnette Hui Xian Ng, Kathleen M. Carley

Abstract: The cross-strait relationship between China and Taiwan is marked by increasing hostility around potential reunification. We analyze an unattributed bot network and how repeater bots engaged in an influence campaign against Taiwan following US House Speaker Nancy Pelosi's visit to Taiwan in 2022. We examine the message amplification tactics employed by four key bot sub-communities, the widespread d… ▽ More The cross-strait relationship between China and Taiwan is marked by increasing hostility around potential reunification. We analyze an unattributed bot network and how repeater bots engaged in an influence campaign against Taiwan following US House Speaker Nancy Pelosi's visit to Taiwan in 2022. We examine the message amplification tactics employed by four key bot sub-communities, the widespread dissemination of information across multiple platforms through URLs, and the potential targeted audiences of this bot network. We find that URL link sharing reveals circumvention around YouTube suspensions, in addition to the potential effectiveness of algorithmic bot connectivity to appear less bot-like, and detail a sequence of coordination within a sub-community for message amplification. We additionally find the narratives and targeted audience potentially shifting after account activity discrepancies, demonstrating how dynamic these bot networks can operate. △ Less

Submitted 16 October, 2023; originally announced October 2023.

Comments: 10 pages with 5 figures. Published in Conference Proceedings for Social, Cultural, and Behavioral Modeling (SBP-BRiMS 2023)

DeepSpeed Ulysses: System Optimizations for Enabling Training of Extreme Long Sequence Transformer Models

Authors: Sam Ade Jacobs, Masahiro Tanaka, Chengming Zhang, Minjia Zhang, Shuaiwen Leon Song, Samyam Rajbhandari, Yuxiong He

Abstract: Computation in a typical Transformer-based large language model (LLM) can be characterized by batch size, hidden dimension, number of layers, and sequence length. Until now, system works for accelerating LLM training have focused on the first three dimensions: data parallelism for batch size, tensor parallelism for hidden size and pipeline parallelism for model depth or layers. These widely studie… ▽ More Computation in a typical Transformer-based large language model (LLM) can be characterized by batch size, hidden dimension, number of layers, and sequence length. Until now, system works for accelerating LLM training have focused on the first three dimensions: data parallelism for batch size, tensor parallelism for hidden size and pipeline parallelism for model depth or layers. These widely studied forms of parallelism are not targeted or optimized for long sequence Transformer models. Given practical application needs for long sequence LLM, renewed attentions are being drawn to sequence parallelism. However, existing works in sequence parallelism are constrained by memory-communication inefficiency, limiting their scalability to long sequence large models. In this work, we introduce DeepSpeed-Ulysses, a novel, portable and effective methodology for enabling highly efficient and scalable LLM training with extremely long sequence length. DeepSpeed-Ulysses at its core partitions input data along the sequence dimension and employs an efficient all-to-all collective communication for attention computation. Theoretical communication analysis shows that whereas other methods incur communication overhead as sequence length increases, DeepSpeed-Ulysses maintains constant communication volume when sequence length and compute devices are increased proportionally. Furthermore, experimental evaluations show that DeepSpeed-Ulysses trains 2.5x faster with 4x longer sequence length than the existing method SOTA baseline. △ Less

Submitted 4 October, 2023; v1 submitted 25 September, 2023; originally announced September 2023.

Learning Broadcast Protocols

Authors: Dana Fisman, Noa Izsak, Swen Jacobs

Abstract: The problem of learning a computational model from examples has been receiving growing attention. For the particularly challenging problem of learning models of distributed systems, existing results are restricted to models with a fixed number of interacting processes. In this work we look for the first time (to the best of our knowledge) at the problem of learning a distributed system with an arb… ▽ More The problem of learning a computational model from examples has been receiving growing attention. For the particularly challenging problem of learning models of distributed systems, existing results are restricted to models with a fixed number of interacting processes. In this work we look for the first time (to the best of our knowledge) at the problem of learning a distributed system with an arbitrary number of processes, assuming only that there exists a cutoff, i.e., a number of processes that is sufficient to produce all observable behaviors. Specifically, we consider fine broadcast protocols, these are broadcast protocols (BPs) with a finite cutoff and no hidden states. We provide a learning algorithm that can infer a correct BP from a sample that is consistent with a fine BP, and a minimal equivalent BP if the sample is sufficiently complete. On the negative side we show that (a) characteristic sets of exponential size are unavoidable, (b) the consistency problem for fine BPs is NP hard, and (c) that fine BPs are not polynomially predictable. △ Less

Submitted 11 December, 2023; v1 submitted 25 June, 2023; originally announced June 2023.

Comments: 13 pages, 7 figures, 3 input files of plots

ACM Class: F.4.3

ZeRO++: Extremely Efficient Collective Communication for Giant Model Training

Authors: Guanhua Wang, Heyang Qin, Sam Ade Jacobs, Connor Holmes, Samyam Rajbhandari, Olatunji Ruwase, Feng Yan, Lei Yang, Yuxiong He

Abstract: Zero Redundancy Optimizer (ZeRO) has been used to train a wide range of large language models on massive GPUs clusters due to its ease of use, efficiency, and good scalability. However, when training on low-bandwidth clusters, or at scale which forces batch size per GPU to be small, ZeRO's effective throughput is limited because of high communication volume from gathering weights in forward pass,… ▽ More Zero Redundancy Optimizer (ZeRO) has been used to train a wide range of large language models on massive GPUs clusters due to its ease of use, efficiency, and good scalability. However, when training on low-bandwidth clusters, or at scale which forces batch size per GPU to be small, ZeRO's effective throughput is limited because of high communication volume from gathering weights in forward pass, backward pass, and averaging gradients. This paper introduces three communication volume reduction techniques, which we collectively refer to as ZeRO++, targeting each of the communication collectives in ZeRO. First is block-quantization based all-gather. Second is data remap** that trades-off communication for more memory. Third is a novel all-to-all based quantized gradient averaging paradigm as replacement of reduce-scatter collective, which preserves accuracy despite communicating low precision data. Collectively, ZeRO++ reduces communication volume of ZeRO by 4x, enabling up to 2.16x better throughput at 384 GPU scale. △ Less

Submitted 16 June, 2023; originally announced June 2023.

Comments: 12 pages

The K-band (24 GHz) Celestial Reference Frame determined from Very Long Baseline Interferometry sessions conducted over the past 20 years

Authors: Hana Krasna, David Gordon, Aletha de Witt, Christopher S. Jacobs

Abstract: The third realization of the International Celestial Reference Frame (ICRF3) was adopted in August 2018 and includes positions of extragalactic objects at three frequencies: 8.4 GHz, 24 GHz, and 32 GHz. In this paper, we present celestial reference frames estimated from Very Long Baseline Interferometry measurements at K-band (24 GHz) including data until June 2022. The data set starts in May 2002… ▽ More The third realization of the International Celestial Reference Frame (ICRF3) was adopted in August 2018 and includes positions of extragalactic objects at three frequencies: 8.4 GHz, 24 GHz, and 32 GHz. In this paper, we present celestial reference frames estimated from Very Long Baseline Interferometry measurements at K-band (24 GHz) including data until June 2022. The data set starts in May 2002 and currently consists of more than 120 24h observing sessions performed over the past 20 years. Since the publication of ICRF3, the additional observations of the sources during the last four years allow maintenance of the celestial reference frame and more than 200 additional radio sources ensure an expansion of the frame. A study of the presented solutions is carried out hel** us to understand systematic differences between the astrometric catalogs and moving us towards a better next ICRF solution. We compare K-band solutions (VIE-K-2022b and USNO-K-2022July05) computed by two analysts with two independent software packages (VieVS and Calc/Solve) and describe the differences in the solution strategy. We assess the systematic differences using vector spherical harmonics and describe the reasons for the most prominent ones. △ Less

Submitted 16 June, 2023; originally announced June 2023.

Comments: accepted for publication in International Association of Geodesy Symposia, peer-reviewed

On More than Two Decades of Celestial Reference Frame VLBI Observations in the Deep South: IVS-CRDS (1995-2021)

Authors: S. Weston, A. de Witt, Hana Krasna, Karine Le Bail, Sara Hardon, David Gordon, Shu Fengchun, Alan Fey, Matthias Schartner, Sayan Basu, Oleg Titov, Dirk Behrend, Christopher S. Jacobs, Warren Hankey, Febreico Salguero, John E. Reynolds

Abstract: The International VLBI Service for Geodesy & Astrometry (IVS) regularly provides high-quality data to produce Earth Orientation Parameters (EOP), and for the maintenance and realization of the International Terrestrial and Celestial Reference Frames, ITRF and ICRF. The first iteration of the celestial reference frame (CRF) at radio wavelengths, the ICRF1, was adopted by the International Astronomi… ▽ More The International VLBI Service for Geodesy & Astrometry (IVS) regularly provides high-quality data to produce Earth Orientation Parameters (EOP), and for the maintenance and realization of the International Terrestrial and Celestial Reference Frames, ITRF and ICRF. The first iteration of the celestial reference frame (CRF) at radio wavelengths, the ICRF1, was adopted by the International Astronomical Union (IAU) in 1997 to replace the FK5 optical frame. Soon after, the IVS began official operations and in 2009 there was a significant increase in data sufficient to warrant a second iteration of the CRF, ICRF2. The most recent ICRF3, was adopted by the IAU in 2018. However, due to the geographic distribution of observing stations being concentrated in the Northern hemisphere, CRFs are generally weaker in the South due to there being fewer Southern Hemisphere observations. To increase the Southern Hemisphere observations, and the density, precision of the sources, a series of deep South observing sessions was initiated in 1995. This initiative in 2004 became the IVS Celestial Reference Frame Deep South (IVS-CRDS) observing program. This paper covers the evolution of the CRDS observing program for the period 1995 to 2021, details the data products and results, and concludes with a summary of upcoming improvements to this ongoing project. △ Less

Submitted 13 June, 2023; v1 submitted 11 June, 2023; originally announced June 2023.

Comments: 25 pages, 16 figures, 3 tables, accepted for publication in PASA 2nd June 2023. Resubmit as a co-author was missed in the arXiv metadata, paper is the same

The Brain Tumor Segmentation (BraTS-METS) Challenge 2023: Brain Metastasis Segmentation on Pre-treatment MRI

Authors: Ahmed W. Moawad, Anastasia Janas, Ujjwal Baid, Divya Ramakrishnan, Rachit Saluja, Nader Ashraf, Leon Jekel, Raisa Amiruddin, Maruf Adewole, Jake Albrecht, Udunna Anazodo, Sanjay Aneja, Syed Muhammad Anwar, Timothy Bergquist, Evan Calabrese, Veronica Chiang, Verena Chung, Gian Marco Marco Conte, Farouk Dako, James Eddy, Ivan Ezhov, Ariana Familiar, Keyvan Farahani, Juan Eugenio Iglesias, Zhifan Jiang , et al. (206 additional authors not shown)

Abstract: The translation of AI-generated brain metastases (BM) segmentation into clinical practice relies heavily on diverse, high-quality annotated medical imaging datasets. The BraTS-METS 2023 challenge has gained momentum for testing and benchmarking algorithms using rigorously annotated internationally compiled real-world datasets. This study presents the results of the segmentation challenge and chara… ▽ More The translation of AI-generated brain metastases (BM) segmentation into clinical practice relies heavily on diverse, high-quality annotated medical imaging datasets. The BraTS-METS 2023 challenge has gained momentum for testing and benchmarking algorithms using rigorously annotated internationally compiled real-world datasets. This study presents the results of the segmentation challenge and characterizes the challenging cases that impacted the performance of the winning algorithms. Untreated brain metastases on standard anatomic MRI sequences (T1, T2, FLAIR, T1PG) from eight contributed international datasets were annotated in stepwise method: published UNET algorithms, student, neuroradiologist, final approver neuroradiologist. Segmentations were ranked based on lesion-wise Dice and Hausdorff distance (HD95) scores. False positives (FP) and false negatives (FN) were rigorously penalized, receiving a score of 0 for Dice and a fixed penalty of 374 for HD95. Eight datasets comprising 1303 studies were annotated, with 402 studies (3076 lesions) released on Synapse as publicly available datasets to challenge competitors. Additionally, 31 studies (139 lesions) were held out for validation, and 59 studies (218 lesions) were used for testing. Segmentation accuracy was measured as rank across subjects, with the winning team achieving a LesionWise mean score of 7.9. Common errors among the leading teams included false negatives for small lesions and misregistration of masks in space.The BraTS-METS 2023 challenge successfully curated well-annotated, diverse datasets and identified common errors, facilitating the translation of BM segmentation across varied clinical environments and providing personalized volumetric reports to patients undergoing BM treatment. △ Less

Submitted 17 June, 2024; v1 submitted 1 June, 2023; originally announced June 2023.

EMOTE: An Explainable architecture for Modelling the Other Through Empathy

Authors: Manisha Senadeera, Thommen Karimpanal George, Sunil Gupta, Stephan Jacobs, Santu Rana

Abstract: We can usually assume others have goals analogous to our own. This assumption can also, at times, be applied to multi-agent games - e.g. Agent 1's attraction to green pellets is analogous to Agent 2's attraction to red pellets. This "analogy" assumption is tied closely to the cognitive process known as empathy. Inspired by empathy, we design a simple and explainable architecture to model another a… ▽ More We can usually assume others have goals analogous to our own. This assumption can also, at times, be applied to multi-agent games - e.g. Agent 1's attraction to green pellets is analogous to Agent 2's attraction to red pellets. This "analogy" assumption is tied closely to the cognitive process known as empathy. Inspired by empathy, we design a simple and explainable architecture to model another agent's action-value function. This involves learning an "Imagination Network" to transform the other agent's observed state in order to produce a human-interpretable "empathetic state" which, when presented to the learning agent, produces behaviours that mimic the other agent. Our approach is applicable to multi-agent scenarios consisting of a single learning agent and other (independent) agents acting according to fixed policies. This architecture is particularly beneficial for (but not limited to) algorithms using a composite value or reward function. We show our method produces better performance in multi-agent games, where it robustly estimates the other's model in different environment configurations. Additionally, we show that the empathetic states are human interpretable, and thus verifiable. △ Less

Submitted 31 May, 2023; originally announced June 2023.

Automatic and Incremental Repair for Speculative Information Leaks

Authors: Joachim Bard, Swen Jacobs, Yakir Vizel

Abstract: We present CureSpec, the first model-checking based framework for automatic repair of programs with respect to information leaks in the presence of side-channels and speculative execution. CureSpec is based on formal models of attacker capabilities, including observable side channels, inspired by the Spectre attacks. For a given attacker model, CureSpec is able to either prove that the program is… ▽ More We present CureSpec, the first model-checking based framework for automatic repair of programs with respect to information leaks in the presence of side-channels and speculative execution. CureSpec is based on formal models of attacker capabilities, including observable side channels, inspired by the Spectre attacks. For a given attacker model, CureSpec is able to either prove that the program is secure, or detect potential side-channel vulnerabilities and automatically insert mitigations such that the resulting code is provably secure. Moreover, CureSpec can provide a certificate for the security of the program that can be independently checked. We have implemented CureSpec in the SeaHorn framework and show that it can effectively repair security-critical code, for example the AES encryption from the OpenSSL library. △ Less

Submitted 17 May, 2023; originally announced May 2023.

Comments: 25 pages

Parameterized Verification of Disjunctive Timed Networks

Authors: Étienne André, Paul Eichler, Swen Jacobs, Shyam Lal Karra

Abstract: We introduce new techniques for the parameterized verification of disjunctive timed networks (DTNs), i.e., networks of timed automata (TAs) that communicate via location guards that enable a transition only if there is another process in a given location. This computational model has been considered in the literature before, example applications are gossi** clock synchronization protocols or pla… ▽ More We introduce new techniques for the parameterized verification of disjunctive timed networks (DTNs), i.e., networks of timed automata (TAs) that communicate via location guards that enable a transition only if there is another process in a given location. This computational model has been considered in the literature before, example applications are gossi** clock synchronization protocols or planning problems. We address the minimum-time reachability problem (Minreach) in DTNs, and show how to efficiently solve it based on a novel zone graph algorithm. We further show that solving Minreach allows us to construct a summary TA capturing exactly the possible behaviors of a single TA within a DTN of arbitrary size. The combination of these two results enables the parameterized verification of DTNs, while avoiding the construction of an exponential-size cutoff system required by existing results. Additionally, we develop sufficient conditions for solving Minreach and parameterized verification problems even in certain cases where locations that appear in location guards can have clock invariants, a case that has usually been excluded in the literature. Our techniques are also implemented, and experiments show their practicality. △ Less

Submitted 2 January, 2024; v1 submitted 12 May, 2023; originally announced May 2023.

Comments: 21 pages, 6 figures

ACM Class: D.2.4; F.1.2

Journal ref: VMCAI 2024

The Temporal Logic Synthesis Format TLSF v1.2

Authors: Swen Jacobs, Guillermo A. Perez, Philipp Schlehuber-Caissier

Abstract: We present an extension of the Temporal Logic Synthesis Format (TLSF). TLSF builds on standard LTL, but additionally supports high-level constructs, such as sets and functions, as well as parameters that allow a specification to define a whole a family of problems. Our extension introduces operators and a new semantics option for LTLf , i.e., LTL on finite executions. We present an extension of the Temporal Logic Synthesis Format (TLSF). TLSF builds on standard LTL, but additionally supports high-level constructs, such as sets and functions, as well as parameters that allow a specification to define a whole a family of problems. Our extension introduces operators and a new semantics option for LTLf , i.e., LTL on finite executions. △ Less

Submitted 7 March, 2023; originally announced March 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:1604.02284, arXiv:1601.05228

Position and Proper Motion of Sagittarius A* in the ICRF3 Frame from VLBI Absolute Astrometry

Authors: David Gordon, Aletha de Witt, Christopher S. Jacobs

Abstract: Sagittarius A* (Sgr A*) is a strong, compact radio source believed to be powered by a super-massive black hole at the galactic center. Extinction by dust and gas in the galactic plane prevents observing it optically, but its position and proper motion have previously been estimated using radio interferometry. We present new VLBI absolute astrometry measurements of its precise position and proper m… ▽ More Sagittarius A* (Sgr A*) is a strong, compact radio source believed to be powered by a super-massive black hole at the galactic center. Extinction by dust and gas in the galactic plane prevents observing it optically, but its position and proper motion have previously been estimated using radio interferometry. We present new VLBI absolute astrometry measurements of its precise position and proper motion in the frame of the third realization of the International Celestial Reference Frame, ICRF3. The observations used were made at 52 epochs on the VLBA at K-band (24 GHz) between June 2006 and August 2022. We find the proper motion of Sgr A* to be -3.128 $\pm$ 0.042 mas/yr in right ascension and -5.584 $\pm$ 0.075 mas/yr in declination, or 6.400 $\pm$ 0.073 mas/yr at a position angle of 209.26 $\pm$ 0.51 degrees. We also find its J2000 ICRF3 coordinates at the 2015.0 proper motion epoch to be 17$^h$45$^m$40.034047$^s$ $\pm$ 0.000018$^s$, -29$^o$00'28.21601'' $\pm$ 0.00044''. In galactic coordinates, Sgr A* shows proper motion of -6.396 $\pm$ 0.071 mas/yr in galactic longitude and -0.239 $\pm$ 0.045 mas/yr in galactic latitude, indicating solar motion of 248.0 $\pm$ 2.8 km/sec in the galactic plane and 9.3 $\pm$ 1.9 km/sec towards the north galactic pole. △ Less

Submitted 1 December, 2022; originally announced December 2022.

Comments: Accepted for publication in the Astronomical Journal

Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification (Extended Version)

Authors: Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, Roopsha Samanta

Abstract: Distributed agreement-based (DAB) systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality. While automated verification for DAB systems is undecidable in general, recent work identifies a large class of DAB systems for which verification is efficiently-decidable. Unfortunately, the conditions characterizing such a c… ▽ More Distributed agreement-based (DAB) systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality. While automated verification for DAB systems is undecidable in general, recent work identifies a large class of DAB systems for which verification is efficiently-decidable. Unfortunately, the conditions characterizing such a class can be opaque and non-intuitive, and can pose a significant challenge to system designers trying to model their systems in this class. In this paper, we present a synthesis-driven tool, Cinnabar, to help system designers building DAB systems "fit" their intended designs into an efficiently-decidable class. In particular, starting from an initial sketch provided by the designer, Cinnabar generates sketch completions using a counterexample-guided procedure. The core technique relies on a compact encoding of a set of related counterexamples. We demonstrate Cinnabar's effectiveness by successfully and efficiently synthesizing completions for a variety of interesting DAB systems. △ Less

Submitted 14 January, 2023; v1 submitted 25 August, 2022; originally announced August 2022.

Comments: TACAS 2023

The Reactive Synthesis Competition (SYNTCOMP): 2018-2021

Authors: Swen Jacobs, Guillermo A. Perez, Remco Abraham, Veronique Bruyere, Michael Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaetan Staquet, Clement Tamines, Leander Tentrup, Adam Walker

Abstract: We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, inclu… ▽ More We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, including a ranking of tools with respect to quantity and quality - that is, the total size in terms of logic and memory elements - of solutions. △ Less

Submitted 6 May, 2024; v1 submitted 1 June, 2022; originally announced June 2022.

Comments: accepted for publication in STTT

A Framework for Controlling Multi-Robot Systems Using Bayesian Optimization and Linear Combination of Vectors

Authors: Stephen Jacobs, R. Michael Butts, Yu Gu, Ali Baheri, Guilherme A. S. Pereira

Abstract: We propose a general framework for creating parameterized control schemes for decentralized multi-robot systems. A variety of tasks can be seen in the decentralized multi-robot literature, each with many possible control schemes. For several of them, the agents choose control velocities using algorithms that extract information from the environment and combine that information in meaningful ways.… ▽ More We propose a general framework for creating parameterized control schemes for decentralized multi-robot systems. A variety of tasks can be seen in the decentralized multi-robot literature, each with many possible control schemes. For several of them, the agents choose control velocities using algorithms that extract information from the environment and combine that information in meaningful ways. From this basic formation, a framework is proposed that classifies each robots' measurement information as sets of relevant scalars and vectors and creates a linear combination of the measured vector sets. Along with an optimizable parameter set, the scalar measurements are used to generate the coefficients for the linear combination. With this framework and Bayesian optimization, we can create effective control systems for several multi-robot tasks, including cohesion and segregation, pattern formation, and searching/foraging. △ Less

Submitted 23 March, 2022; originally announced March 2022.

Comments: 7 pages, 8 figures

Learning Interpretable Models Through Multi-Objective Neural Architecture Search

Authors: Zachariah Carmichael, Tim Moon, Sam Ade Jacobs

Abstract: Monumental advances in deep learning have led to unprecedented achievements across various domains. While the performance of deep neural networks is indubitable, the architectural design and interpretability of such models are nontrivial. Research has been introduced to automate the design of neural network architectures through neural architecture search (NAS). Recent progress has made these meth… ▽ More Monumental advances in deep learning have led to unprecedented achievements across various domains. While the performance of deep neural networks is indubitable, the architectural design and interpretability of such models are nontrivial. Research has been introduced to automate the design of neural network architectures through neural architecture search (NAS). Recent progress has made these methods more pragmatic by exploiting distributed computation and novel optimization algorithms. However, there is little work in optimizing architectures for interpretability. To this end, we propose a multi-objective distributed NAS framework that optimizes for both task performance and "introspectability," a surrogate metric for aspects of interpretability. We leverage the non-dominated sorting genetic algorithm (NSGA-II) and explainable AI (XAI) techniques to reward architectures that can be better comprehended by domain experts. The framework is evaluated on several image classification datasets. We demonstrate that jointly optimizing for task error and introspectability leads to more disentangled and debuggable architectures that perform within tolerable error. △ Less

Submitted 4 July, 2023; v1 submitted 16 December, 2021; originally announced December 2021.

Comments: International Conference on Automated Machine Learning (AutoML) Workshop

Automatic Repair and Deadlock Detection for Parameterized Systems

Authors: Swen Jacobs, Mouhammad Sakr, Marcus Völp

Abstract: We present an algorithm for the repair of parameterized systems. The repair problem is, for a given process implementation, to find a refinement such that a given safety property is satisfied by the resulting parameterized system, and deadlocks are avoided. Our algorithm uses a parameterized model checker to determine the correctness of candidate solutions and employs a constraint system to rule o… ▽ More We present an algorithm for the repair of parameterized systems. The repair problem is, for a given process implementation, to find a refinement such that a given safety property is satisfied by the resulting parameterized system, and deadlocks are avoided. Our algorithm uses a parameterized model checker to determine the correctness of candidate solutions and employs a constraint system to rule out candidates. We apply this algorithm on systems that can be represented as well-structured transition systems (WSTS), including disjunctive systems, pairwise rendezvous systems, and broadcast protocols. Moreover, we show that parameterized deadlock detection can be decided in EXPTIME for disjunctive systems, and that deadlock detection is in general undecidable for broadcast protocols. △ Less

Submitted 28 July, 2022; v1 submitted 5 November, 2021; originally announced November 2021.

Hosting Industry Centralization and Consolidation

Authors: Luciano Zembruzki, Raffaele Sommese, Lisandro Zambenedetti Granville, Arthur Selle Jacobs, Mattijs Jonker, Giovane C. M. Moura

Abstract: There have been growing concerns about the concentration and centralization of Internet infrastructure. In this work, we scrutinize the hosting industry on the Internet by using active measurements, covering 19 Top-Level Domains (TLDs). We show how the market is heavily concentrated: 1/3 of the domains are hosted by only 5 hosting providers, all US-based companies. For the country-code TLDs (ccTLD… ▽ More There have been growing concerns about the concentration and centralization of Internet infrastructure. In this work, we scrutinize the hosting industry on the Internet by using active measurements, covering 19 Top-Level Domains (TLDs). We show how the market is heavily concentrated: 1/3 of the domains are hosted by only 5 hosting providers, all US-based companies. For the country-code TLDs (ccTLDs), however, hosting is primarily done by local, national hosting providers and not by the large American cloud and content providers. We show how shared languages (and borders) shape the hosting market -- German hosting companies have a notable presence in Austrian and Swiss markets, given they all share German as official language. While hosting concentration has been relatively high and stable over the past four years, we see that American hosting companies have been continuously increasing their presence in the market related to high traffic, popular domains within ccTLDs -- except for Russia, notably. △ Less

Submitted 25 January, 2022; v1 submitted 2 September, 2021; originally announced September 2021.

Comments: to appear in IEEE/IFIP Network Operations and Management Symposium https://noms2022.ieee-noms.org/

The Three Ghosts of Medical AI: Can the Black-Box Present Deliver?

Authors: Thomas P. Quinn, Stephan Jacobs, Manisha Senadeera, Vuong Le, Simon Coghlan

Abstract: Our title alludes to the three Christmas ghosts encountered by Ebenezer Scrooge in \textit{A Christmas Carol}, who guide Ebenezer through the past, present, and future of Christmas holiday events. Similarly, our article will take readers through a journey of the past, present, and future of medical AI. In doing so, we focus on the crux of modern machine learning: the reliance on powerful but intri… ▽ More Our title alludes to the three Christmas ghosts encountered by Ebenezer Scrooge in \textit{A Christmas Carol}, who guide Ebenezer through the past, present, and future of Christmas holiday events. Similarly, our article will take readers through a journey of the past, present, and future of medical AI. In doing so, we focus on the crux of modern machine learning: the reliance on powerful but intrinsically opaque models. When applied to the healthcare domain, these models fail to meet the needs for transparency that their clinician and patient end-users require. We review the implications of this failure, and argue that opaque models (1) lack quality assurance, (2) fail to elicit trust, and (3) restrict physician-patient dialogue. We then discuss how upholding transparency in all aspects of model design and model validation can help ensure the reliability of medical AI. △ Less

Submitted 10 December, 2020; originally announced December 2020.

The third realization of the International Celestial Reference Frame by very long baseline interferometry

Authors: P. Charlot, C. S. Jacobs, D. Gordon, S. Lambert, A. de Witt, J. Böhm, A. L. Fey, R. Heinkelmann, E. Skurikhina, O. Titov, E. F. Arias, S. Bolotin, G. Bourda, C. Ma, Z. Malkin, A. Nothnagel, D. Mayer, D. S. MacMillan, T. Nilsson, R. Gaume

Abstract: A new realization of the International Celestial Reference Frame (ICRF) is presented based on the work achieved by a working group of the International Astronomical Union (IAU) mandated for this purpose. This new realization, referred to as ICRF3, is based on nearly 40 years of data acquired by very long baseline interferometry. The ICRF3 includes positions at 8.4 GHz for 4536 sources, supplemente… ▽ More A new realization of the International Celestial Reference Frame (ICRF) is presented based on the work achieved by a working group of the International Astronomical Union (IAU) mandated for this purpose. This new realization, referred to as ICRF3, is based on nearly 40 years of data acquired by very long baseline interferometry. The ICRF3 includes positions at 8.4 GHz for 4536 sources, supplemented with positions at 24 GHz for 824 sources and at 32 GHz for 678 sources, for a total of 4588 sources. A subset of 303 sources among these, uniformly distributed on the sky, are identified as "defining sources" and as such serve to define the axes of the frame. Source positions are reported for epoch 2015.0 and must be propagated for observations at other epochs for the most accurate needs, accounting for the acceleration toward the Galactic center, which results in a dipolar proper motion field of amplitude 0.0058 milliarcsecond/yr (mas/yr). The frame shows a median positional uncertainty of about 0.1 mas in right ascension and 0.2 mas in declination, with a noise floor of 0.03 mas in the individual source coordinates. A subset of 500 sources is found to have extremely accurate positions at 8.4 GHz, in the range of 0.03 to 0.06 mas. Comparing ICRF3 with the Gaia Celestial Reference Frame 2 in the optical domain, there is no evidence for deformations larger than 0.03 mas between the two frames. Significant positional offsets between the three ICRF3 frequencies are detected for about 5% of the sources. Moreover, a notable fraction (22%) of the sources shows optical and radio positions that are significantly offset. There are indications that these positional offsets may be the manifestation of extended source structures. This third realization of the ICRF was adopted by the IAU at its 30th General Assembly in August 2018 and replaced the previous realization, ICRF2, on January 1, 2019. △ Less

Submitted 26 October, 2020; originally announced October 2020.

Comments: 28 pages, 22 figures

Journal ref: A&A 644, A159 (2020)

Trust and Medical AI: The challenges we face and the expertise needed to overcome them

Authors: Thomas P. Quinn, Manisha Senadeera, Stephan Jacobs, Simon Coghlan, Vuong Le

Abstract: Artificial intelligence (AI) is increasingly of tremendous interest in the medical field. However, failures of medical AI could have serious consequences for both clinical outcomes and the patient experience. These consequences could erode public trust in AI, which could in turn undermine trust in our healthcare institutions. This article makes two contributions. First, it describes the major conc… ▽ More Artificial intelligence (AI) is increasingly of tremendous interest in the medical field. However, failures of medical AI could have serious consequences for both clinical outcomes and the patient experience. These consequences could erode public trust in AI, which could in turn undermine trust in our healthcare institutions. This article makes two contributions. First, it describes the major conceptual, technical, and humanistic challenges in medical AI. Second, it proposes a solution that hinges on the education and accreditation of new expert groups who specialize in the development, verification, and operation of medical AI technologies. These groups will be required to maintain trust in our healthcare institutions. △ Less

Submitted 18 August, 2020; originally announced August 2020.

Comments: 6 pages, 2 figures

Refining Network Intents for Self-Driving Networks

Authors: Arthur Selle Jacobs, Ricardo José Pfitscher, Ronaldo Alves Ferreira, Lisandro Zambenedetti Granville

Abstract: Recent advances in artificial intelligence (AI) offer an opportunity for the adoption of self-driving networks. However, network operators or home-network users still do not have the right tools to exploit these new advancements in AI, since they have to rely on low-level languages to specify network policies. Intent-based networking (IBN) allows operators to specify high-level policies that dicta… ▽ More Recent advances in artificial intelligence (AI) offer an opportunity for the adoption of self-driving networks. However, network operators or home-network users still do not have the right tools to exploit these new advancements in AI, since they have to rely on low-level languages to specify network policies. Intent-based networking (IBN) allows operators to specify high-level policies that dictate how the network should behave without worrying how they are translated into configuration commands in the network devices. However, the existing research proposals for IBN fail to exploit the knowledge and feedback from the network operator to validate or improve the translation of intents. In this paper, we introduce a novel intent-refinement process that uses machine learning and feedback from the operator to translate the operator's utterances into network configurations. Our refinement process uses a sequence-to-sequence learning model to extract intents from natural language and the feedback from the operator to improve learning. The key insight of our process is an intermediate representation that resembles natural language that is suitable to collect feedback from the operator but is structured enough to facilitate precise translations. Our prototype interacts with a network operator using natural language and translates the operator input to the intermediate representation before translating to SDN rules. Our experimental results show that our process achieves a correlation coefficient squared (i.e., R-squared) of 0.99 for a dataset with 5000 entries and the operator feedback significantly improves the accuracy of our model. △ Less

Submitted 12 August, 2020; originally announced August 2020.

Comments: 9 pages, 5 figures, 3 listings, 1 grammar

ACM Class: C.2.3; C.2.1

Journal ref: ACM SIGCOMM Computer Communication Review (CCR), vol. 48, issue 5, p. 55-63, October 2018

Validation of Abstract Side-Channel Models for Computer Architectures

Authors: Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Swen Jacobs

Abstract: Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment… ▽ More Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs which invalidate the models due to hidden microarchitectural behavior. △ Less

Submitted 11 May, 2020; originally announced May 2020.

Parameterized Verification of Systems with Global Synchronization and Guards

Authors: Nouraldin Jaber, Swen Jacobs, Christopher Wagner, Milind Kulkarni, Roopsha Samanta

Abstract: Inspired by distributed applications that use consensus or other agreement protocols for global coordination, we define a new computational model for parameterized systems that is based on a general global synchronization primitive and allows for global transition guards. Our model generalizes many existing models in the literature, including broadcast protocols and guarded protocols. We show that… ▽ More Inspired by distributed applications that use consensus or other agreement protocols for global coordination, we define a new computational model for parameterized systems that is based on a general global synchronization primitive and allows for global transition guards. Our model generalizes many existing models in the literature, including broadcast protocols and guarded protocols. We show that reachability properties are decidable for systems without guards, and give sufficient conditions under which they remain decidable in the presence of guards. Furthermore, we investigate cutoffs for reachability properties and provide sufficient conditions for small cutoffs in a number of cases that are inspired by our target applications. △ Less

Submitted 5 May, 2021; v1 submitted 9 April, 2020; originally announced April 2020.

Comments: Conference version published at CAV 2020; this version contains a correction of guard-compatibility conditions C2.1 and C2.2

Journal ref: Lecture Notes in Computer Science, vol 12224. Springer (2020)

QuickSilver: A Modeling and Parameterized Verification Framework for Systems with Distributed Agreement (Extended Version)

Authors: Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, Roopsha Samanta

Abstract: The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond the core protocols and target applications that are built on top of agreement protocols. This is unfortunate, as agreement-based distributed services such as data stores, locks, a… ▽ More The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond the core protocols and target applications that are built on top of agreement protocols. This is unfortunate, as agreement-based distributed services such as data stores, locks, and ledgers are ubiquitous and potentially permit modular, scalable verification approaches that mimic their modular design. We address this need for verification of distributed agreement-based systems through our novel modeling and verification framework, QuickSilver, that is not only modular, but also fully automated. The key enabling feature of QuickSilver is our encoding of abstractions of verified agreement protocols that facilitates modular, decidable, and scalable automated verification. We demonstrate the potential of QuickSilver by modeling and efficiently verifying a series of tricky case studies, adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more. △ Less

Submitted 13 September, 2021; v1 submitted 9 April, 2020; originally announced April 2020.

Comments: Accepted at OOPSLA 2021

BAD to the Bone: Big Active Data at its Core

Authors: Steven Jacobs, Xikui Wang, Michael J. Carey, Vassilis J. Tsotras, Md Yusuf Sarwar Uddin

Abstract: Virtually all of today's Big Data systems are passive in nature, responding to queries posted by their users. Instead, we are working to shift Big Data platforms from passive to active. In our view, a Big Active Data (BAD) system should continuously and reliably capture Big Data while enabling timely and automatic delivery of relevant information to a large pool of interested users, as well as sup… ▽ More Virtually all of today's Big Data systems are passive in nature, responding to queries posted by their users. Instead, we are working to shift Big Data platforms from passive to active. In our view, a Big Active Data (BAD) system should continuously and reliably capture Big Data while enabling timely and automatic delivery of relevant information to a large pool of interested users, as well as supporting retrospective analyses of historical information. While various scalable streaming query engines have been created, their active behavior is limited to a (relatively) small window of the incoming data. To this end we have created a BAD platform that combines ideas and capabilities from both Big Data and Active Data (e.g., Publish/Subscribe, Streaming Engines). It supports complex subscriptions that consider not only newly arrived items but also their relationships to past, stored data. Further, it can provide actionable notifications by enriching the subscription results with other useful data. Our platform extends an existing open-source Big Data Management System, Apache AsterixDB, with an active toolkit. The toolkit contains features to rapidly ingest semistructured data, share execution pipelines among users, manage scaled user data subscriptions, and actively monitor the state of the data to produce individualized information for each user. This paper describes the features and design of our current BAD data platform and demonstrates its ability to scale without sacrificing query capabilities or result individualization. △ Less

Submitted 23 May, 2020; v1 submitted 22 February, 2020; originally announced February 2020.

Comments: 30 pages. Accepted by VLDBJ

Enabling Machine Learning-Ready HPC Ensembles with Merlin

Authors: J. Luc Peterson, Ben Bay, Joe Koning, Peter Robinson, Jessica Semler, Jeremy White, Rushil Anirudh, Kevin Athey, Peer-Timo Bremer, Francesco Di Natale, David Fox, Jim A. Gaffney, Sam A. Jacobs, Bhavya Kailkhura, Bogdan Kustowski, Steven Langer, Brian Spears, Jayaraman Thiagarajan, Brian Van Essen, Jae-Seung Yeom

Abstract: With the growing complexity of computational and experimental facilities, many scientific researchers are turning to machine learning (ML) techniques to analyze large scale ensemble data. With complexities such as multi-component workflows, heterogeneous machine architectures, parallel file systems, and batch scheduling, care must be taken to facilitate this analysis in a high performance computin… ▽ More With the growing complexity of computational and experimental facilities, many scientific researchers are turning to machine learning (ML) techniques to analyze large scale ensemble data. With complexities such as multi-component workflows, heterogeneous machine architectures, parallel file systems, and batch scheduling, care must be taken to facilitate this analysis in a high performance computing (HPC) environment. In this paper, we present Merlin, a workflow framework to enable large ML-friendly ensembles of scientific HPC simulations. By augmenting traditional HPC with distributed compute technologies, Merlin aims to lower the barrier for scientific subject matter experts to incorporate ML into their analysis. In addition to its design, we describe some example applications that Merlin has enabled on leadership-class HPC resources, such as the ML-augmented optimization of nuclear fusion experiments and the calibration of infectious disease models to study the progression of and possible mitigation strategies for COVID-19. △ Less

Submitted 1 July, 2021; v1 submitted 5 December, 2019; originally announced December 2019.

Comments: 28 pages, 9 figures; Submitted to FGCS

Report number: LLNL-JRNL-821884

Promptness and Bounded Fairness in Concurrent and Parameterized Systems

Authors: Swen Jacobs, Mouhammad Sakr, Martin Zimmermann

Abstract: We investigate the satisfaction of specifications in Prompt Linear Temporal Logic (Prompt-LTL) by concurrent systems. Prompt-LTL is an extension of LTL that allows to specify parametric bounds on the satisfaction of eventualities, thus adding a quantitative aspect to the specification language. We establish a connection between bounded fairness, bounded stutter equivalence, and the satisfaction of… ▽ More We investigate the satisfaction of specifications in Prompt Linear Temporal Logic (Prompt-LTL) by concurrent systems. Prompt-LTL is an extension of LTL that allows to specify parametric bounds on the satisfaction of eventualities, thus adding a quantitative aspect to the specification language. We establish a connection between bounded fairness, bounded stutter equivalence, and the satisfaction of Prompt-LTL\X formulas. Based on this connection, we prove the first cutoff results for different classes of systems with a parametric number of components and quantitative specifications, thereby identifying previously unknown decidable fragments of the parameterized model checking problem. △ Less

Submitted 15 November, 2019; v1 submitted 8 November, 2019; originally announced November 2019.

Comments: Accepted for publication in VMCAI 2020

Parallelizing Training of Deep Generative Models on Massive Scientific Datasets

Authors: Sam Ade Jacobs, Brian Van Essen, David Hysom, Jae-Seung Yeom, Tim Moon, Rushil Anirudh, Jayaraman J. Thiagaranjan, Shusen Liu, Peer-Timo Bremer, Jim Gaffney, Tom Benson, Peter Robinson, Luc Peterson, Brian Spears

Abstract: Training deep neural networks on large scientific data is a challenging task that requires enormous compute power, especially if no pre-trained models exist to initialize the process. We present a novel tournament method to train traditional as well as generative adversarial networks built on LBANN, a scalable deep learning framework optimized for HPC systems. LBANN combines multiple levels of par… ▽ More Training deep neural networks on large scientific data is a challenging task that requires enormous compute power, especially if no pre-trained models exist to initialize the process. We present a novel tournament method to train traditional as well as generative adversarial networks built on LBANN, a scalable deep learning framework optimized for HPC systems. LBANN combines multiple levels of parallelism and exploits some of the worlds largest supercomputers. We demonstrate our framework by creating a complex predictive model based on multi-variate data from high-energy-density physics containing hundreds of millions of images and hundreds of millions of scalar values derived from tens of millions of simulations of inertial confinement fusion. Our approach combines an HPC workflow and extends LBANN with optimized data ingestion and the new tournament-style training algorithm to produce a scalable neural network architecture using a CORAL-class supercomputer. Experimental results show that 64 trainers (1024 GPUs) achieve a speedup of 70.2 over a single trainer (16 GPUs) baseline, and an effective 109% parallel efficiency. △ Less

Submitted 5 October, 2019; originally announced October 2019.

Scalable Topological Data Analysis and Visualization for Evaluating Data-Driven Models in Scientific Applications

Authors: Shusen Liu, Di Wang, Dan Maljovec, Rushil Anirudh, Jayaraman J. Thiagarajan, Sam Ade Jacobs, Brian C. Van Essen, David Hysom, Jae-Seung Yeom, Jim Gaffney, Luc Peterson, Peter B. Robinson, Harsh Bhatia, Valerio Pascucci, Brian K. Spears, Peer-Timo Bremer

Abstract: With the rapid adoption of machine learning techniques for large-scale applications in science and engineering comes the convergence of two grand challenges in visualization. First, the utilization of black box models (e.g., deep neural networks) calls for advanced techniques in exploring and interpreting model behaviors. Second, the rapid growth in computing has produced enormous datasets that re… ▽ More With the rapid adoption of machine learning techniques for large-scale applications in science and engineering comes the convergence of two grand challenges in visualization. First, the utilization of black box models (e.g., deep neural networks) calls for advanced techniques in exploring and interpreting model behaviors. Second, the rapid growth in computing has produced enormous datasets that require techniques that can handle millions or more samples. Although some solutions to these interpretability challenges have been proposed, they typically do not scale beyond thousands of samples, nor do they provide the high-level intuition scientists are looking for. Here, we present the first scalable solution to explore and analyze high-dimensional functions often encountered in the scientific data analysis pipeline. By combining a new streaming neighborhood graph construction, the corresponding topology computation, and a novel data aggregation scheme, namely topology aware datacubes, we enable interactive exploration of both the topological and the geometric aspect of high-dimensional data. Following two use cases from high-energy-density (HED) physics and computational biology, we demonstrate how these capabilities have led to crucial new insights in both applications. △ Less

Submitted 18 July, 2019; originally announced July 2019.

The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results

Authors: Swen Jacobs, Roderick Bloem, Maximilien Colange, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Philipp J. Meyer, Thibaud Michaud, Mouhammad Sakr, Salomon Sickert, Leander Tentrup, Adam Walker

Abstract: We report on the fifth reactive synthesis competition (SYNTCOMP 2018). We introduce four new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the evaluation scheme and the experimental setup of SYNTCOMP 2018. We give an overview of the participants of SYNTCOMP 2018 and highlight changes compared to previous years. Finally, we present and analyze the results of o… ▽ More We report on the fifth reactive synthesis competition (SYNTCOMP 2018). We introduce four new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the evaluation scheme and the experimental setup of SYNTCOMP 2018. We give an overview of the participants of SYNTCOMP 2018 and highlight changes compared to previous years. Finally, we present and analyze the results of our experimental evaluation, including a ranking of tools with respect to quantity and quality of solutions. △ Less

Submitted 15 April, 2019; originally announced April 2019.

Comments: arXiv admin note: substantial text overlap with arXiv:1711.11439, arXiv:1609.00507

Distinguishing between Normal and Cancer Cells Using Autoencoder Node Saliency

Authors: Ya Ju Fan, Jonathan E. Allen, Sam Ade Jacobs, Brian C. Van Essen

Abstract: Gene expression profiles have been widely used to characterize patterns of cellular responses to diseases. As data becomes available, scalable learning toolkits become essential to processing large datasets using deep learning models to model complex biological processes. We present an autoencoder to capture nonlinear relationships recovered from gene expression profiles. The autoencoder is a nonl… ▽ More Gene expression profiles have been widely used to characterize patterns of cellular responses to diseases. As data becomes available, scalable learning toolkits become essential to processing large datasets using deep learning models to model complex biological processes. We present an autoencoder to capture nonlinear relationships recovered from gene expression profiles. The autoencoder is a nonlinear dimension reduction technique using an artificial neural network, which learns hidden representations of unlabeled data. We train the autoencoder on a large collection of tumor samples from the National Cancer Institute Genomic Data Commons, and obtain a generalized and unsupervised latent representation. We leverage a HPC-focused deep learning toolkit, Livermore Big Artificial Neural Network (LBANN) to efficiently parallelize the training algorithm, reducing computation times from several hours to a few minutes. With the trained autoencoder, we generate latent representations of a small dataset, containing pairs of normal and cancer cells of various tumor types. A novel measure called autoencoder node saliency (ANS) is introduced to identify the hidden nodes that best differentiate various pairs of cells. We compare our findings of the best classifying nodes with principal component analysis and the visualization of t-distributed stochastic neighbor embedding. We demonstrate that the autoencoder effectively extracts distinct gene features for multiple learning tasks in the dataset. △ Less

Submitted 30 January, 2019; originally announced January 2019.

Comments: Second Workshop on HPC Applications in Precision Medicine, June 2018

The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results

Authors: Swen Jacobs, Nicolas Basset, Roderick Bloem, Romain Brenguier, Maximilien Colange, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Thibaud Michaud, Guillermo A. Pérez, Jean-François Raskin, Ocan Sankur, Leander Tentrup

Abstract: We report on the fourth reactive synthesis competition (SYNTCOMP 2017). We introduce two new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the benchmark selection, evaluation scheme and the experimental setup of SYNTCOMP 2017. We present the participants of SYNTCOMP 2017, with a focus on changes with respect to the previous years and on the two completely new… ▽ More We report on the fourth reactive synthesis competition (SYNTCOMP 2017). We introduce two new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the benchmark selection, evaluation scheme and the experimental setup of SYNTCOMP 2017. We present the participants of SYNTCOMP 2017, with a focus on changes with respect to the previous years and on the two completely new tools that have entered the competition. Finally, we present and analyze the results of our experimental evaluation, including a ranking of tools with respect to quantity and quality of solutions. △ Less

Submitted 28 November, 2017; originally announced November 2017.

Comments: In Proceedings SYNT 2017, arXiv:1711.10224. arXiv admin note: text overlap with arXiv:1609.00507

Journal ref: EPTCS 260, 2017, pp. 116-143

Proceedings Sixth Workshop on Synthesis

Authors: Dana Fisman, Swen Jacobs

Abstract: The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. App… ▽ More The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. Application domains include software, hardware, embedded, and cyber-physical systems. Computation models include functional, reactive, hybrid and timed systems. Identifying, formalizing, and evaluating synthesis in particular application domains is encouraged. The sixth iteration of the workshop took place in Heidelberg, Germany. It was co-located with the 29th International Conference on Computer Aided Verification. The workshop included four contributed talks, four invited talks, and reports on the Syntax-Guided Synthesis Competition (SyGuS) and the Reactive Synthesis Competition (SYNTCOMP). △ Less

Submitted 28 November, 2017; originally announced November 2017.

Journal ref: EPTCS 260, 2017

Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity

Authors: Swen Jacobs, Mouhammad Sakr

Abstract: We study cutoff results for parameterized verification and synthesis of guarded protocols, as introduced by Emerson and Kahlon (2000). Guarded protocols describe systems of processes whose transitions are enabled or disabled depending on the existence of other processes in certain local states. Cutoff results reduce reasoning about systems with an arbitrary number of processes to systems of a dete… ▽ More We study cutoff results for parameterized verification and synthesis of guarded protocols, as introduced by Emerson and Kahlon (2000). Guarded protocols describe systems of processes whose transitions are enabled or disabled depending on the existence of other processes in certain local states. Cutoff results reduce reasoning about systems with an arbitrary number of processes to systems of a determined, fixed size. Our work is based on the observation that existing cutoff results for guarded protocols are often impractical, since they scale linearly in the number of local states of processes in the system. We provide new cutoffs that scale not with the number of local states, but with the number of guards in the system, which is in many cases much smaller. Furthermore, we consider natural extensions of the classes of systems and specifications under consideration, and present results for problems that have not been known to admit cutoffs before. △ Less

Submitted 5 July, 2017; originally announced July 2017.

Distributed Synthesis for Parameterized Temporal Logics

Authors: Swen Jacobs, Leander Tentrup, Martin Zimmermann

Abstract: We consider the synthesis of distributed implementations for specifications in parameterized temporal logics such as PROMPT-LTL, which extends LTL by temporal operators equipped with parameters that bound their scope. For single process synthesis it is well-established that such parametric extensions do not increase worst-case complexities. For synchronous distributed systems we show that, despite… ▽ More We consider the synthesis of distributed implementations for specifications in parameterized temporal logics such as PROMPT-LTL, which extends LTL by temporal operators equipped with parameters that bound their scope. For single process synthesis it is well-established that such parametric extensions do not increase worst-case complexities. For synchronous distributed systems we show that, despite being more powerful, the realizability problem for PROMPT-LTL is not harder than its LTL counterpart. For asynchronous systems we have to express scheduling assumptions and therefore consider an assume-guarantee synthesis problem. As asynchronous distributed synthesis is already undecidable for LTL, we give a semi-decision procedure for the PROMPT-LTL assume-guarantee synthesis problem based on bounded synthesis. Finally, we show that our results extend to the stronger logics PLTL and PLDL. △ Less

Submitted 26 February, 2018; v1 submitted 23 May, 2017; originally announced May 2017.

Comments: Extended version of arXiv:1509.05144. Preprint submitted to Information and Computation

The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond

Authors: Swen Jacobs, Roderick Bloem

Abstract: We report on the design of the third reactive synthesis competition (SYNTCOMP 2016), including a major extension of the competition to specifications in full linear temporal logic. We give a brief overview of the synthesis problem as considered in SYNTCOMP, and present the rules of the competition in 2016, as well as the ideas behind our design choices. Furthermore, we evaluate the recent changes… ▽ More We report on the design of the third reactive synthesis competition (SYNTCOMP 2016), including a major extension of the competition to specifications in full linear temporal logic. We give a brief overview of the synthesis problem as considered in SYNTCOMP, and present the rules of the competition in 2016, as well as the ideas behind our design choices. Furthermore, we evaluate the recent changes to the competition based on the experiences with SYNTCOMP 2016. Finally, we give an outlook on further changes and extensions of the competition that are planned for the future. △ Less

Submitted 22 November, 2016; originally announced November 2016.

Comments: In Proceedings SYNT 2016, arXiv:1611.07178

Journal ref: EPTCS 229, 2016, pp. 133-148

The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results

Authors: Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker

Abstract: We report on the benchmarks, participants and results of the third reactive synthesis competition(SYNTCOMP 2016). The benchmark library of SYNTCOMP 2016 has been extended to benchmarks in the new LTL-based temporal logic synthesis format (TLSF), and 2 new sets of benchmarks for the existing AIGER-based format for safety specifications. The participants of SYNTCOMP 2016 can be separated according t… ▽ More We report on the benchmarks, participants and results of the third reactive synthesis competition(SYNTCOMP 2016). The benchmark library of SYNTCOMP 2016 has been extended to benchmarks in the new LTL-based temporal logic synthesis format (TLSF), and 2 new sets of benchmarks for the existing AIGER-based format for safety specifications. The participants of SYNTCOMP 2016 can be separated according to these two classes of specifications, and we give an overview of the 6 tools that entered the competition in the AIGER-based track, and the 3 participants that entered the TLSF-based track. We briefly describe the benchmark selection, evaluation scheme and the experimental setup of SYNTCOMP 2016. Finally, we present and analyze the results of our experimental evaluation, including a comparison to participants of previous competitions and a legacy tool. △ Less

Submitted 23 November, 2016; v1 submitted 2 September, 2016; originally announced September 2016.

Comments: In Proceedings SYNT 2016, arXiv:1611.07178

Journal ref: EPTCS 229, 2016, pp. 149-177

A High-Level LTL Synthesis Format: TLSF v1.1

Authors: Swen Jacobs, Felix Klein, Sebastian Schirmer

Abstract: We present the Temporal Logic Synthesis Format (TLSF), a high-level format to describe synthesis problems via Linear Temporal Logic (LTL). The format builds upon standard LTL, but additionally allows to use high-level constructs, such as sets and functions, to provide a compact and human-readable representation. Furthermore, the format allows to identify parameters of a specification such that a s… ▽ More We present the Temporal Logic Synthesis Format (TLSF), a high-level format to describe synthesis problems via Linear Temporal Logic (LTL). The format builds upon standard LTL, but additionally allows to use high-level constructs, such as sets and functions, to provide a compact and human-readable representation. Furthermore, the format allows to identify parameters of a specification such that a single description can be used to define a family of problems. Additionally, we present a tool to automatically translate the format into plain LTL, which then can be used for synthesis by a solver. The tool also allows to adjust parameters of the specification and to apply standard transformations on the resulting formula. △ Less

Submitted 22 November, 2016; v1 submitted 8 April, 2016; originally announced April 2016.

Comments: In Proceedings SYNT 2016, arXiv:1611.07178. arXiv admin note: substantial text overlap with arXiv:1601.05228

Journal ref: EPTCS 229, 2016, pp. 112-132

The Second Reactive Synthesis Competition (SYNTCOMP 2015)

Authors: Swen Jacobs, Roderick Bloem, Romain Brenguier, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker

Abstract: We report on the design and results of the second reactive synthesis competition (SYNTCOMP 2015). We describe our extended benchmark library, with 6 completely new sets of benchmarks, and additional challenging instances for 4 of the benchmark sets that were already used in SYNTCOMP 2014. To enhance the analysis of experimental results, we introduce an extension of our benchmark format with meta-i… ▽ More We report on the design and results of the second reactive synthesis competition (SYNTCOMP 2015). We describe our extended benchmark library, with 6 completely new sets of benchmarks, and additional challenging instances for 4 of the benchmark sets that were already used in SYNTCOMP 2014. To enhance the analysis of experimental results, we introduce an extension of our benchmark format with meta-information, including a difficulty rating and a reference size for solutions. Tools are evaluated on a set of 250 benchmarks, selected to provide a good coverage of benchmarks from all classes and difficulties. We report on changes of the evaluation scheme and the experimental setup. Finally, we describe the entrants into SYNTCOMP 2015, as well as the results of our experimental evaluation. In our analysis, we emphasize progress over the tools that participated last year. △ Less

Submitted 2 February, 2016; originally announced February 2016.

Comments: In Proceedings SYNT 2015, arXiv:1602.00786

Journal ref: EPTCS 202, 2016, pp. 27-57

A High-Level LTL Synthesis Format: TLSF v1.0

Authors: Swen Jacobs, Felix Klein

Abstract: We present the Temporal Logic Synthesis Format (TLSF), a high-level format to describe synthesis problems via Linear Temporal Logic (LTL). The format builds upon standard LTL, but additionally allows to use high level constructs, such as sets and functions, to provide a compact and human readable representation. Furthermore, the format allows to identify parameters of a specification such that a s… ▽ More We present the Temporal Logic Synthesis Format (TLSF), a high-level format to describe synthesis problems via Linear Temporal Logic (LTL). The format builds upon standard LTL, but additionally allows to use high level constructs, such as sets and functions, to provide a compact and human readable representation. Furthermore, the format allows to identify parameters of a specification such that a single description can be used to define a family of problems. We also present a tool to automatically translate the format into plain LTL, which then can be used for synthesis by a solver. The tool also allows to adjust parameters of the specification and to apply standard transformations on the resulting formula. △ Less

Submitted 20 January, 2016; originally announced January 2016.

Long-range dispersal, stochasticity and the broken accelerating wave of advance

Authors: Guy S. Jacobs, Tim J. Sluckin

Abstract: Rare long distance dispersal events are thought to have a disproportionate impact on the spread of invasive species. Modelling using integrodifference equations suggests that, when long distance contacts are represented by a fat-tailed dispersal kernel, an accelerating wave of advance can ensue. Invasions spreading in this manner could have particularly dramatic effects. Recently, various authors… ▽ More Rare long distance dispersal events are thought to have a disproportionate impact on the spread of invasive species. Modelling using integrodifference equations suggests that, when long distance contacts are represented by a fat-tailed dispersal kernel, an accelerating wave of advance can ensue. Invasions spreading in this manner could have particularly dramatic effects. Recently, various authors have suggested that demographic stochasticity disrupts wave acceleration. Integrodifference models have been widely used in movement ecology, and as such a clearer understanding of stochastic effects is needed. Here, we present a stochastic non-linear one-dimensional lattice model in which demographic stochasticity and the dispersal regime can be systematically varied. Extensive simulations show that stochasticity has a profound effect on model behaviour, and usually breaks acceleration for fat-tailed kernels. Exceptions are seen for some power law kernels, $K(l) \propto |l|^{-β}$ with $β< 3$, for which acceleration persists despite stochasticity. Such kernels lack a second moment and are important in `accelerating' phenomena such as Lévy flights. Furthermore, for long-range kernels the approach to the continuum limit behaviour as stochasticity is reduced is generally slow. Given that real-world populations are finite, stochastic models may give better predictive power when long-range dispersal is important. Insights from mean-field models such as integrodifference equations should be applied with caution in such circumstances. △ Less

Submitted 30 November, 2015; originally announced November 2015.

Comments: Preprint version (October 2014) of TPB article accepted for publication December 2014

Journal ref: Theoretical Population Biology (2015) Vol. 100 Pages 39-55

The ICRF-3: Status, plans, and progress on the next generation International Celestial Reference Frame

Authors: Z. Malkin, C. S. Jacobs, F. Arias, D. Boboltz, J. Boehm, S. Bolotin, G. Bourda, P. Charlot, A. De Witt, A. Fey, R. Gaume, R. Heinkelmann, S. Lambert, C. Ma, A. Nothnagel, M. Seitz, D. Gordon, E. Skurikhina, J. Souchay, O. Titov

Abstract: The goal of this presentation is to report the latest progress in creation of the next generation of VLBI-based International Celestial Reference Frame, ICRF3. Two main directions of ICRF3 development are improvement of the S/X-band frame and extension of the ICRF to higher frequencies. Another important task of this work is the preparation for comparison of ICRF3 with the new generation optical f… ▽ More The goal of this presentation is to report the latest progress in creation of the next generation of VLBI-based International Celestial Reference Frame, ICRF3. Two main directions of ICRF3 development are improvement of the S/X-band frame and extension of the ICRF to higher frequencies. Another important task of this work is the preparation for comparison of ICRF3 with the new generation optical frame GCRF expected by the end of the decade as a result of the Gaia mission. △ Less

Submitted 25 November, 2015; originally announced November 2015.

Journal ref: Proceedings of the Journees 2014 Systemes de Reference Spatio-temporels, St. Petersburg, Russia, 22-24 Sep 2014, Eds. Z. Malkin, N. Capitaine, 2015, pp.~3-8