Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic

• URL: http://arxiv.org/abs/2203.07982v1
• Date: Tue, 15 Mar 2022 15:14:25 GMT
• Title: Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic
• Authors: Paolo Felli, Marco Montali, Sarah Winkler
• Abstract summary: We introduce a new semantic property of "finite summary", which guarantees the existence of a faithful finite-state abstraction. Several decidability conditions studied in formal methods and database theory can be seen as concrete, checkable instances of this property. Our results allow us to analyze systems that were out of reach in earlier approaches.
• Score: 8.914271888521652
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Combined modeling and verification of dynamic systems and the data they operate on has gained momentum in AI and in several application domains. We investigate the expressive yet concise framework of data-aware dynamic systems (DDS), extending it with linear arithmetic, and provide the following contributions. First, we introduce a new, semantic property of "finite summary", which guarantees the existence of a faithful finite-state abstraction. We rely on this to show that checking whether a witness exists for a linear-time, finite-trace property is decidable for DDSs with finite summary. Second, we demonstrate that several decidability conditions studied in formal methods and database theory can be seen as concrete, checkable instances of this property. This also gives rise to new decidability results. Third, we show how the abstract, uniform property of finite summary leads to modularity results: a system enjoys finite summary if it can be partitioned appropriately into smaller systems that possess the property. Our results allow us to analyze systems that were out of reach in earlier approaches. Finally, we demonstrate the feasibility of our approach in a prototype implementation.

Related papers

• Bisimulation Learning [55.859538562698496]
  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.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• Learning Latent Dynamics via Invariant Decomposition and (Spatio-)Temporal Transformers [0.6767885381740952]
  We propose a method for learning dynamical systems from high-dimensional empirical data. We focus on the setting in which data are available from multiple different instances of a system. We study behaviour through simple theoretical analyses and extensive experiments on synthetic and real-world datasets.
  arXiv  Detail & Related papers  (2023-06-21T07:52:07Z)
• Schema-aware Reference as Prompt Improves Data-Efficient Knowledge Graph Construction [57.854498238624366]
  We propose a retrieval-augmented approach, which retrieves schema-aware Reference As Prompt (RAP) for data-efficient knowledge graph construction. RAP can dynamically leverage schema and knowledge inherited from human-annotated and weak-supervised data as a prompt for each sample.
  arXiv  Detail & Related papers  (2022-10-19T16:40:28Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  We introduce the general framework of relational action bases (RABs) RABs generalize existing models by lifting both restrictions. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes.
  arXiv  Detail & Related papers  (2022-08-12T17:03:50Z)
• Combining Machine Learning and Agent-Based Modeling to Study Biomedical Systems [0.0]
  Agent-based modeling (ABM) is a well-established paradigm for simulating complex systems via interactions between constituent entities. Machine learning (ML) refers to approaches whereby statistical algorithms 'learn from data on their own, without imposing a priori theories of system behavior.
  arXiv  Detail & Related papers  (2022-06-02T15:19:09Z)
• MACE: An Efficient Model-Agnostic Framework for Counterfactual Explanation [132.77005365032468]
  We propose a novel framework of Model-Agnostic Counterfactual Explanation (MACE) In our MACE approach, we propose a novel RL-based method for finding good counterfactual examples and a gradient-less descent method for improving proximity. Experiments on public datasets validate the effectiveness with better validity, sparsity and proximity.
  arXiv  Detail & Related papers  (2022-05-31T04:57:06Z)
• Capturing Actionable Dynamics with Structured Latent Ordinary Differential Equations [68.62843292346813]
  We propose a structured latent ODE model that captures system input variations within its latent representation. Building on a static variable specification, our model learns factors of variation for each input to the system, thus separating the effects of the system inputs in the latent space.
  arXiv  Detail & Related papers  (2022-02-25T20:00:56Z)
• Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression [11.729744197698718]
  Leveraging autonomous systems in safety-critical scenarios requires verifying their behaviors in the presence of uncertainties. We develop a framework for verifying discrete-time dynamical systems with unmodelled dynamics and noisy measurements.
  arXiv  Detail & Related papers  (2021-12-31T05:10:05Z)
• Learning on Abstract Domains: A New Approach for Verifiable Guarantee in Reinforcement Learning [9.428825075908131]
  We propose an abstraction-based approach to train DRL systems on finite abstract domains. It yields neural networks whose input states are finite, making hosting DRL systems directly verifiable.
  arXiv  Detail & Related papers  (2021-06-13T06:28:40Z)
• Active Learning for Nonlinear System Identification with Guarantees [102.43355665393067]
  We study a class of nonlinear dynamical systems whose state transitions depend linearly on a known feature embedding of state-action pairs. We propose an active learning approach that achieves this by repeating three steps: trajectory planning, trajectory tracking, and re-estimation of the system from all available data. We show that our method estimates nonlinear dynamical systems at a parametric rate, similar to the statistical rate of standard linear regression.
  arXiv  Detail & Related papers  (2020-06-18T04:54:11Z)
• Data-Driven Verification under Signal Temporal Logic Constraints [0.0]
  We consider systems under uncertainty whose dynamics are partially unknown. Our aim is to study satisfaction of temporal logic properties by trajectories of such systems. We employ Bayesian inference techniques to associate a confidence value to the satisfaction of the property.
  arXiv  Detail & Related papers  (2020-05-08T08:32:30Z)

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.