Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

• URL: http://arxiv.org/abs/2511.15227v1
• Date: Wed, 19 Nov 2025 08:28:30 GMT
• Title: Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca
• Authors: Hiep Hong Trinh, Marjan Sirjani, Federico Ciccozzi, Abu Naser Masud, Mikael Sjödin,
• Abstract summary: Timed Rebeca is an actor-based modelling language supporting reactive, concurrent and time semantics.<n>We show how to use models to design and verify a multi-robot system, how to discretely model a continuous system to do model-checking efficiently.<n>The released Rebeca and ROS2 codes can serve as a foundation for modelling multiple autonomous robots systems.
• Score: 1.3048920509133806
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Model-based development enables quicker prototyping, earlier experimentation and validation of design intents. For a multi-agent system with complex asynchronous interactions and concurrency, formal verification, model-checking in particular, offers an automated mechanism for verifying desired properties. Timed Rebeca is an actor-based modelling language supporting reactive, concurrent and time semantics, accompanied with a model-checking compiler. These capabilities allow using Timed Rebeca to correctly model ROS2 node topographies, recurring physical signals, motion primitives and other timed and time-convertible behaviors. The biggest challenges in modelling and verifying a multi-robot system lie in abstracting complex information, bridging the gap between a discrete model and a continuous system and compacting the state space, while maintaining the model's accuracy. We develop different discretization strategies for different kinds of information, identifying the 'enough' thresholds of abstraction, and applying efficient optimization techniques to boost computations. With this work we demonstrate how to use models to design and verify a multi-robot system, how to discretely model a continuous system to do model-checking efficiently, and the round-trip engineering flow between the model and the implementation. The released Rebeca and ROS2 codes can serve as a foundation for modelling multiple autonomous robots systems.

Related papers

• Heterogeneous Model Alignment in Digital Twin [0.0]
  Key challenge in model-driven DTs is aligning heterogeneous models across abstraction layers.<n>Existing methods, relying on static mappings and manual updates, are often inflexible, error-prone, and risk compromising data integrity.<n>We present a heterogeneous model alignment approach for multi-layered, model-driven DTs.
  arXiv  Detail & Related papers  (2025-12-17T10:36:55Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  We show that the decoding mechanism of dLLMs can be used as a powerful tool for model attribution.<n>We propose a novel information extraction scheme called the Directed Decoding Map (DDM), which captures structural relationships between decoding steps and better reveals model-specific behaviors.
  arXiv  Detail & Related papers  (2025-10-02T06:25:10Z)
• OptMerge: Unifying Multimodal LLM Capabilities and Modalities via Model Merging [124.91183814854126]
  Model merging seeks to combine multiple expert models into a single model.<n>We introduce a benchmark for model merging research that clearly divides the tasks for MLLM training and evaluation.<n>We find that model merging offers a promising way for building improved MLLMs without requiring training data.
  arXiv  Detail & Related papers  (2025-05-26T12:23:14Z)
• Generative diffusion model surrogates for mechanistic agent-based biological models [0.003897077734517544]
  The Cellular-Potts Model (CPM) is a powerful and popular framework for developing and interrogating CPMs.<n>Surrogate models may allow for the accelerated evaluation of CPMs of complex biological systems.<n>We train a generative AI surrogate classifier of a CPM used to investigate in vitro vasculogenesis.<n>Our work represents a step towards the implementation of DDPMs to develop digital twins of biological systems.
  arXiv  Detail & Related papers  (2025-05-01T08:19:51Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  This paper aims to improve model-based anomaly detection in CPPS by combining the learned timed automaton with a formal knowledge graph about the system. Both the model and the detected anomalies are described in the knowledge graph in order to allow operators an easier interpretation of the model and the detected anomalies.
  arXiv  Detail & Related papers  (2023-08-25T15:25:57Z)
• Domain-aware Control-oriented Neural Models for Autonomous Underwater Vehicles [2.4779082385578337]
  We present control-oriented parametric models with varying levels of domain-awareness. We employ universal differential equations to construct data-driven blackbox and graybox representations of the AUV dynamics.
  arXiv  Detail & Related papers  (2022-08-15T17:01:14Z)
• Closed-form Continuous-Depth Models [99.40335716948101]
  Continuous-depth neural models rely on advanced numerical differential equation solvers. We present a new family of models, termed Closed-form Continuous-depth (CfC) networks, that are simple to describe and at least one order of magnitude faster.
  arXiv  Detail & Related papers  (2021-06-25T22:08:51Z)
• Anomaly Detection of Time Series with Smoothness-Inducing Sequential Variational Auto-Encoder [59.69303945834122]
  We present a Smoothness-Inducing Sequential Variational Auto-Encoder (SISVAE) model for robust estimation and anomaly detection of time series. Our model parameterizes mean and variance for each time-stamp with flexible neural networks. We show the effectiveness of our model on both synthetic datasets and public real-world benchmarks.
  arXiv  Detail & Related papers  (2021-02-02T06:15:15Z)
• A Novel Anomaly Detection Algorithm for Hybrid Production Systems based on Deep Learning and Timed Automata [73.38551379469533]
  DAD:DeepAnomalyDetection is a new approach for automatic model learning and anomaly detection in hybrid production systems. It combines deep learning and timed automata for creating behavioral model from observations. The algorithm has been applied to few data sets including two from real systems and has shown promising results.
  arXiv  Detail & Related papers  (2020-10-29T08:27:43Z)
• Action-Conditional Recurrent Kalman Networks For Forward and Inverse Dynamics Learning [17.80270555749689]
  Estimating accurate forward and inverse dynamics models is a crucial component of model-based control for robots. We present two architectures for forward model learning and one for inverse model learning. Both architectures significantly outperform exist-ing model learning frameworks as well as analytical models in terms of prediction performance.
  arXiv  Detail & Related papers  (2020-10-20T11:28:25Z)
• Hybrid modeling: Applications in real-time diagnosis [64.5040763067757]
  We outline a novel hybrid modeling approach that combines machine learning inspired models and physics-based models. We are using such models for real-time diagnosis applications.
  arXiv  Detail & Related papers  (2020-03-04T00:44:57Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.