Stateless and Rule-Based Verification For Compliance Checking
Applications
- URL: http://arxiv.org/abs/2204.07430v1
- Date: Thu, 14 Apr 2022 17:31:33 GMT
- Title: Stateless and Rule-Based Verification For Compliance Checking
Applications
- Authors: Mohammad Reza Besharati, Mohammad Izadi, Ehsaneddin Asgari
- Abstract summary: We present a formal logic-based framework for creating intelligent compliance checking systems.
SARV is a verification framework designed to simplify the overall process of verification for stateless and rule-based verification problems.
Based on 300 data experiments, the SARV-based compliance solution outperforms machine learning methods on a 3125-records software quality dataset.
- Score: 1.7403133838762452
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Underlying computational model has an important role in any computation. The
state and transition (such as in automata) and rule and value (such as in Lisp
and logic programming) are two comparable and counterpart computational models.
Both of deductive and model checking verification techniques are relying on a
notion of state and as a result, their underlying computational models are
state dependent. Some verification problems (such as compliance checking by
which an under compliance system is verified against some regulations and
rules) have not a strong notion of state nor transition. Behalf of it, these
systems have a strong notion of value symbols and declarative rules defined on
them. SARV (Stateless And Rule-Based Verification) is a verification framework
that designed to simplify the overall process of verification for stateless and
rule-based verification problems (e.g. compliance checking). In this paper, a
formal logic-based framework for creating intelligent compliance checking
systems is presented. We define and introduce this framework, report a case
study and present results of an experiment on it. The case study is about
protocol compliance checking for smart cities. Using this solution, a Rescue
Scenario use case and its compliance checking are sketched and modeled. An
automation engine for and a compliance solution with SARV are introduced. Based
on 300 data experiments, the SARV-based compliance solution outperforms famous
machine learning methods on a 3125-records software quality dataset.
Related papers
- Neural Model Checking [10.376573742987917]
We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification.
Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic.
We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.
arXiv Detail & Related papers (2024-10-31T10:17:04Z) - Automatically Adaptive Conformal Risk Control [49.95190019041905]
We propose a methodology for achieving approximate conditional control of statistical risks by adapting to the difficulty of test samples.
Our framework goes beyond traditional conditional risk control based on user-provided conditioning events to the algorithmic, data-driven determination of appropriate function classes for conditioning.
arXiv Detail & Related papers (2024-06-25T08:29:32Z) - 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) - 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) - Early Verification of Legal Compliance via Bounded Satisfiability
Checking [4.304202636346692]
Metric first-order temporal logic (MFOTL) provides a rich formalism for specifying legal properties.
No solution exists for MFOTL-based verification in early-stage system development captured by requirements.
We propose a practical, sound, and complete satisfiability checking approach for MFOTL.
arXiv Detail & Related papers (2022-09-08T22:41:40Z) - 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) - Value-Consistent Representation Learning for Data-Efficient
Reinforcement Learning [105.70602423944148]
We propose a novel method, called value-consistent representation learning (VCR), to learn representations that are directly related to decision-making.
Instead of aligning this imagined state with a real state returned by the environment, VCR applies a $Q$-value head on both states and obtains two distributions of action values.
It has been demonstrated that our methods achieve new state-of-the-art performance for search-free RL algorithms.
arXiv Detail & Related papers (2022-06-25T03:02:25Z) - Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations.
We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety.
We then formulate an optimization problem to learn ROCBFs from expert demonstrations that exhibit safe system behavior.
arXiv Detail & Related papers (2021-11-18T23:21:00Z) - Complete Agent-driven Model-based System Testing for Autonomous Systems [0.0]
A novel approach to testing complex autonomous transportation systems is described.
It is intended to mitigate some of the most critical problems regarding verification and validation.
arXiv Detail & Related papers (2021-10-25T01:55:24Z) - Compliance checking in reified IO logic via SHACL [0.0]
Reified Input/Output (I/O) logic[21] has been recently proposed to model real-world norms in terms of the logic in [11]
This paper presents a methodology to carry out compliance checking on reified I/O logic formulae.
arXiv Detail & Related papers (2021-10-13T21:09:47Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework.
First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case.
Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
arXiv Detail & Related papers (2021-03-18T20:22:50Z)
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.