SMT-based Safety Verification of Parameterised Multi-Agent Systems
- URL: http://arxiv.org/abs/2008.04774v2
- Date: Fri, 14 Aug 2020 17:06:25 GMT
- Title: SMT-based Safety Verification of Parameterised Multi-Agent Systems
- Authors: Paolo Felli and Alessandro Gianola and Marco Montali
- Abstract summary: We study the verification of parameterised multi-agent systems (MASs)
In particular, we study whether unwanted states, characterised as a given state formula, are reachable in a given MAS.
- Score: 78.04236259129524
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In this paper we study the verification of parameterised multi-agent systems
(MASs), and in particular the task of verifying whether unwanted states,
characterised as a given state formula, are reachable in a given MAS, i.e.,
whether the MAS is unsafe. The MAS is parameterised and the model only
describes the finite set of possible agent templates, while the actual number
of concrete agent instances for each template is unbounded and cannot be
foreseen. This makes the state-space infinite. As safety may of course depend
on the number of agent instances in the system, the verification result must be
correct irrespective of such number. We solve this problem via infinite-state
model checking based on satisfiability modulo theories (SMT), relying on the
theory of array-based systems: we present parameterised MASs as particular
array-based systems, under two execution semantics for the MAS, which we call
concurrent and interleaved. We prove our decidability results under these
assumptions and illustrate our implementation approach, called SAFE: the Swarm
Safety Detector, based on the third-party model checker MCMT, which we evaluate
experimentally. Finally, we discuss how this approach lends itself to richer
parameterised and data-aware MAS settings beyond the state-of-the-art solutions
in the literature, which we leave as future work.
Related papers
- Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions.
In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates.
We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
arXiv Detail & Related papers (2024-03-15T17:32:02Z) - Scope Compliance Uncertainty Estimate [0.4262974002462632]
SafeML is a model-agnostic approach for performing such monitoring.
This work addresses these limitations by changing the binary decision to a continuous metric.
arXiv Detail & Related papers (2023-12-17T19:44:20Z) - Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal
Abstractions [59.605246463200736]
We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions.
First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states.
We use state-of-the-art verification techniques to provide guarantees on the interval Markov decision process and compute a controller for which these guarantees carry over to the original control system.
arXiv Detail & Related papers (2023-01-04T10:40:30Z) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
We propose a method for synthesising controllers for Markov jump linear systems.
Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS.
We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
arXiv Detail & Related papers (2022-12-01T17:36:30Z) - Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic
Dynamical Models with Epistemic Uncertainty [68.00748155945047]
Capturing uncertainty in models of complex dynamical systems is crucial to designing safe controllers.
Several approaches use formal abstractions to synthesize policies that satisfy temporal specifications related to safety and reachability.
Our contribution is a novel abstraction-based controller method for continuous-state models with noise, uncertain parameters, and external disturbances.
arXiv Detail & Related papers (2022-10-12T07:57:03Z) - 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) - Adversarial Robustness Verification and Attack Synthesis in Stochastic
Systems [8.833548357664606]
We develop a formal framework for adversarial robustness in systems defined as discrete time Markov chains (DTMCs)
We outline a class of threat models under which adversaries can perturb system transitions, constrained by an $varepsilon$ ball around the original transition probabilities.
arXiv Detail & Related papers (2021-10-05T15:52:47Z) - SMT-Based Safety Verification of Data-Aware Processes under Ontologies
(Extended Version) [71.12474112166767]
We introduce a variant of one of the most investigated models in this spectrum, namely simple artifact systems (SASs)
This DL, enjoying suitable model-theoretic properties, allows us to define SASs to which backward reachability can still be applied, leading to decidability in PSPACE of the corresponding safety problems.
arXiv Detail & Related papers (2021-08-27T15:04:11Z)
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.