Early Verification of Legal Compliance via Bounded Satisfiability Checking

• URL: http://arxiv.org/abs/2209.04052v3
• Date: Sun, 28 May 2023 02:29:19 GMT
• Title: Early Verification of Legal Compliance via Bounded Satisfiability Checking
• Authors: Nick Feng, Lina Marsso, Mehrdad Sabetzadeh, Marsha Chechik
• Abstract summary: 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.
• Score: 4.304202636346692
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Legal properties involve reasoning about data values and time. Metric first-order temporal logic (MFOTL) provides a rich formalism for specifying legal properties. While MFOTL has been successfully used for verifying legal properties over operational systems via runtime monitoring, no solution exists for MFOTL-based verification in early-stage system development captured by requirements. Given a legal property and system requirements, both formalized in MFOTL, the compliance of the property can be verified on the requirements via satisfiability checking. In this paper, we propose a practical, sound, and complete (within a given bound) satisfiability checking approach for MFOTL. The approach, based on satisfiability modulo theories (SMT), employs a counterexample-guided strategy to incrementally search for a satisfying solution. We implemented our approach using the Z3 SMT solver and evaluated it on five case studies spanning the healthcare, business administration, banking and aviation domains. Our results indicate that our approach can efficiently determine whether legal properties of interest are met, or generate counterexamples that lead to compliance violations.

Related papers

• Step-by-Step Reasoning for Math Problems via Twisted Sequential Monte Carlo [55.452453947359736]
  We introduce a novel verification method based on Twisted Sequential Monte Carlo (TSMC) We apply TSMC to Large Language Models by estimating the expected future rewards at partial solutions. This approach results in a more straightforward training target that eliminates the need for step-wise human annotations.
  arXiv  Detail & Related papers  (2024-10-02T18:17:54Z)
• Optimizing Numerical Estimation and Operational Efficiency in the Legal Domain through Large Language Models [13.067312163677933]
  We propose a novel approach integrating Large Language Models with specially designed prompts to address precision requirements in legal Artificial Intelligence (LegalAI) applications. To validate this method, we introduce a curated dataset tailored to precision-oriented LegalAI tasks.
  arXiv  Detail & Related papers  (2024-07-26T18:46:39Z)
• Rethinking Legal Compliance Automation: Opportunities with Large Language Models [2.9088208525097365]
  We argue that the examination of (textual) legal artifacts should, first employ broader context than sentences. We present a compliance analysis approach designed to address these limitations.
  arXiv  Detail & Related papers  (2024-04-22T17:10:27Z)
• Auditing large language models: a three-layered approach [0.0]
  Large language models (LLMs) represent a major advance in artificial intelligence (AI) research. LLMs are also coupled with significant ethical and social challenges. Previous research has pointed towards auditing as a promising governance mechanism.
  arXiv  Detail & Related papers  (2023-02-16T18:55:21Z)
• 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)
• Conformance Checking with Uncertainty via SMT (Extended Version) [66.58864135810981]
  We show how to solve the problem of checking conformance of uncertain logs against data-aware reference processes. Our approach is modular, in that it homogeneously accommodates for different types of uncertainty. We show the correctness of our approach and witness feasibility through a proof-of-concept implementation.
  arXiv  Detail & Related papers  (2022-06-15T11:39:45Z)
• 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)
• Stateless and Rule-Based Verification For Compliance Checking Applications [1.7403133838762452]
  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.
  arXiv  Detail & Related papers  (2022-04-14T17:31:33Z)
• 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)
• 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.