Bisimulation Learning

• URL: http://arxiv.org/abs/2405.15723v1
• Date: Fri, 24 May 2024 17:11:27 GMT
• Title: Bisimulation Learning
• Authors: Alessandro Abate, Mirco Giacobbe, Yannik Schnitzer,
• Abstract summary: We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
• Score: 55.859538562698496
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce a data-driven approach to computing finite bisimulations for state transition systems with very large, possibly infinite state space. Our novel technique computes stutter-insensitive bisimulations of deterministic systems, which we characterize as the problem of learning a state classifier together with a ranking function for each class. Our procedure learns a candidate state classifier and candidate ranking functions from a finite dataset of sample states; then, it checks whether these generalise to the entire state space using satisfiability modulo theory solving. Upon the affirmative answer, the procedure concludes that the classifier constitutes a valid stutter-insensitive bisimulation of the system. Upon a negative answer, the solver produces a counterexample state for which the classifier violates the claim, adds it to the dataset, and repeats learning and checking in a counterexample-guided inductive synthesis loop until a valid bisimulation is found. We demonstrate on a range of benchmarks from reactive verification and software model checking that our method yields faster verification results than alternative state-of-the-art tools in practice. Our method produces succinct abstractions that enable an effective verification of linear temporal logic without next operator, and are interpretable for system diagnostics.

Related papers

• Improving Probabilistic Bisimulation for MDPs Using Machine Learning [0.0]
  We propose a new technique to partition the state space of a given model to its probabilistic bisimulation classes. The approach can decrease significantly the running time compared to state-of-the-art tools.
  arXiv  Detail & Related papers  (2023-07-30T12:58:12Z)
• Quick Adaptive Ternary Segmentation: An Efficient Decoding Procedure For Hidden Markov Models [70.26374282390401]
  Decoding the original signal (i.e., hidden chain) from the noisy observations is one of the main goals in nearly all HMM based data analyses. We present Quick Adaptive Ternary (QATS), a divide-and-conquer procedure which decodes the hidden sequence in polylogarithmic computational complexity.
  arXiv  Detail & Related papers  (2023-05-29T19:37:48Z)
• Structured model selection via $\ell_1-\ell_2$ optimization [1.933681537640272]
  We develop a learning approach for identifying structured dynamical systems. We show that if the set of candidate functions forms a bounded system, the recovery is stable and is bounded.
  arXiv  Detail & Related papers  (2023-05-27T12:51:26Z)
• Unified Functional Hashing in Automatic Machine Learning [58.77232199682271]
  We show that large efficiency gains can be obtained by employing a fast unified functional hash. Our hash is "functional" in that it identifies equivalent candidates even if they were represented or coded differently. We show dramatic improvements on multiple AutoML domains, including neural architecture search and algorithm discovery.
  arXiv  Detail & Related papers  (2023-02-10T18:50:37Z)
• Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes [0.0]
  We propose a data-driven algorithm for numerical invariant synthesis and verification. The algorithm is based on the ICE-DT schema for learning decision trees from samples of positive and negative states.
  arXiv  Detail & Related papers  (2022-05-30T09:18:37Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• An Automated Approach to Causal Inference in Discrete Settings [8.242194776558895]
  We show an algorithm to automatically bound causal effects using efficient dual relaxation and spatial branch-and-bound techniques. The algorithm searches over admissible data-generating processes and outputs the most precise possible range consistent with available information. It offers an additional guarantee we refer to as $epsilon$-sharpness, characterizing the incomplete bounds.
  arXiv  Detail & Related papers  (2021-09-28T03:55:32Z)
• Sparse PCA via $l_{2,p}$-Norm Regularization for Unsupervised Feature Selection [138.97647716793333]
  We propose a simple and efficient unsupervised feature selection method, by combining reconstruction error with $l_2,p$-norm regularization. We present an efficient optimization algorithm to solve the proposed unsupervised model, and analyse the convergence and computational complexity of the algorithm theoretically.
  arXiv  Detail & Related papers  (2020-12-29T04:08:38Z)
• Learning from Incomplete Features by Simultaneous Training of Neural Networks and Sparse Coding [24.3769047873156]
  This paper addresses the problem of training a classifier on a dataset with incomplete features. We assume that different subsets of features (random or structured) are available at each data instance. A new supervised learning method is developed to train a general classifier, using only a subset of features per sample.
  arXiv  Detail & Related papers  (2020-11-28T02:20:39Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)

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.