Bounded Synthesis of Synchronized Distributed Models from Lightweight Specifications

• URL: http://arxiv.org/abs/2502.13955v1
• Date: Wed, 19 Feb 2025 18:54:32 GMT
• Title: Bounded Synthesis of Synchronized Distributed Models from Lightweight Specifications
• Authors: Pablo F. Castro, Luciano Putruele, Renzo Degiovanni, Nazareno Aguirre,
• Abstract summary: We present an approach to automatically synthesize synchronized models from lightweight formal specifications. Our approach takes as input a specification of a distributed system along with a global linear time constraint. It produces executable models for the component specifications whose concurrent execution satisfies the global constraint.
• Score: 4.08734863805696
• License:
• Abstract: We present an approach to automatically synthesize synchronized models from lightweight formal specifications. Our approach takes as input a specification of a distributed system along with a global linear time constraint, which must be fulfilled by the interaction of the system's components. It produces executable models for the component specifications (in the style of Promela language) whose concurrent execution satisfies the global constraint. The component specifications consist of a collection of actions described by means of pre and post conditions together with first-order relational formulas prescribing their behavior. We use the Alloy Analyzer to encode the component specifications and enumerate their potential implementations up to some bound, whose concurrent composition is model checked against the global property. Even though this approach is sound and complete up to the selected bound, it is impractical as the number of candidate implementations grows exponentially. To address this, we propose an algorithm that uses batches of counterexamples to prune the solution space, it has two main phases: exploration, the algorithm collects a batch of counterexamples, and exploitation, where this knowledge is used to speed up the search. The approach is sound, while its completeness depends on the batches used. We present a prototype tool, describe some experiments, and compare it with related approaches.

Related papers

• Fast sampling and model selection for Bayesian mixture models [0.6345523830122168]
  We describe two Monte Carlo algorithms for sampling from the integrated posterior distributions of a range of Bayesian mixture models. The first algorithm is a traditional collapsed Gibbs sampler, albeit with an unusual move-set. The second builds on the first, adding rejection-free sampling from the prior over component assignments.
  arXiv  Detail & Related papers  (2025-01-13T19:58:37Z)
• A Bayesian Mixture Model of Temporal Point Processes with Determinantal Point Process Prior [21.23523473330637]
  Asynchronous event sequence clustering aims to group similar event sequences in an unsupervised manner. Our work provides a flexible learning framework for event sequence clustering, enabling automatic identification of the potential number of clusters. It is applicable to a wide range of parametric temporal point processes, including neural network-based models.
  arXiv  Detail & Related papers  (2024-11-07T03:21:30Z)
• Probabilistic Modeling for Sequences of Sets in Continuous-Time [14.423456635520084]
  We develop a general framework for modeling set-valued data in continuous-time. We also develop inference methods that can use such models to answer probabilistic queries.
  arXiv  Detail & Related papers  (2023-12-22T20:16:10Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  We discuss the problem of bounding partially identifiable queries, such as counterfactuals, in Pearlian structural causal models. A recently proposed iterated EM scheme yields an inner approximation of those bounds by sampling the initialisation parameters. We show how a single symbolic knowledge compilation allows us to obtain the circuit structure with symbolic parameters to be replaced by their actual values.
  arXiv  Detail & Related papers  (2023-10-05T07:10:40Z)
• Single-Stage Visual Relationship Learning using Conditional Queries [60.90880759475021]
  TraCQ is a new formulation for scene graph generation that avoids the multi-task learning problem and the entity pair distribution. We employ a DETR-based encoder-decoder conditional queries to significantly reduce the entity label space as well. Experimental results show that TraCQ not only outperforms existing single-stage scene graph generation methods, it also beats many state-of-the-art two-stage methods on the Visual Genome dataset.
  arXiv  Detail & Related papers  (2023-06-09T06:02:01Z)
• Mutual Exclusivity Training and Primitive Augmentation to Induce Compositionality [84.94877848357896]
  Recent datasets expose the lack of the systematic generalization ability in standard sequence-to-sequence models. We analyze this behavior of seq2seq models and identify two contributing factors: a lack of mutual exclusivity bias and the tendency to memorize whole examples. We show substantial empirical improvements using standard sequence-to-sequence models on two widely-used compositionality datasets.
  arXiv  Detail & Related papers  (2022-11-28T17:36:41Z)
• Flexible Networks for Learning Physical Dynamics of Deformable Objects [2.567499374977917]
  We propose a model named time-wise PointNet (TP-Net) to infer the future state of a deformable object with particle-based representation. TP-Net consists of a shared feature extractor that extracts global features from each input point set in parallel and a prediction network that aggregates and reasons on these features for future prediction. Experiments demonstrate that our model achieves state-of-the-art performance in both synthetic dataset and in real-world dataset, with real-time prediction speed.
  arXiv  Detail & Related papers  (2021-12-07T14:34:52Z)
• Parameter Decoupling Strategy for Semi-supervised 3D Left Atrium Segmentation [0.0]
  We present a novel semi-supervised segmentation model based on parameter decoupling strategy to encourage consistent predictions from diverse views. Our method has achieved a competitive result over the state-of-the-art semisupervised methods on the Atrial Challenge dataset.
  arXiv  Detail & Related papers  (2021-09-20T14:51:42Z)
• Complex Event Forecasting with Prediction Suffix Trees: Extended Technical Report [70.7321040534471]
  Complex Event Recognition (CER) systems have become popular in the past two decades due to their ability to "instantly" detect patterns on real-time streams of events. There is a lack of methods for forecasting when a pattern might occur before such an occurrence is actually detected by a CER engine. We present a formal framework that attempts to address the issue of Complex Event Forecasting.
  arXiv  Detail & Related papers  (2021-09-01T09:52:31Z)
• Modeling Sequences as Distributions with Uncertainty for Sequential Recommendation [63.77513071533095]
  Most existing sequential methods assume users are deterministic. Item-item transitions might fluctuate significantly in several item aspects and exhibit randomness of user interests. We propose a Distribution-based Transformer Sequential Recommendation (DT4SR) which injects uncertainties into sequential modeling.
  arXiv  Detail & Related papers  (2021-06-11T04:35:21Z)
• Finding Geometric Models by Clustering in the Consensus Space [61.65661010039768]
  We propose a new algorithm for finding an unknown number of geometric models, e.g., homographies. We present a number of applications where the use of multiple geometric models improves accuracy. These include pose estimation from multiple generalized homographies; trajectory estimation of fast-moving objects.
  arXiv  Detail & Related papers  (2021-03-25T14:35:07Z)

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.