<p>Software systems handling data are increasingly required to comply with legal properties (LPs) aimed at ensuring security and data privacy. Automated reasoning of LPs can be carried out by solving constraint satisfiability problems in first-order logic. However, the current logic-based reasoning approaches have limited support for capturing and reasoning about LPs with aggregation constraints, which are commonly found in financial and privacy policies. In this work, we extend first-order logic with quantifiers over relational objects (<InlineEquation ID="IEq3"> <EquationSource Format="TEX">$\hbox {FOL}^$</EquationSource> <EquationSource Format="MATHML"><math> <msup> <mtext>FOL</mtext> <mo>∗</mo> </msup> </math></EquationSource> </InlineEquation>) to support aggregation, resulting in a language <InlineEquation ID="IEq4"> <EquationSource Format="TEX">$\hbox {FOL}^{+}$</EquationSource> <EquationSource Format="MATHML"><math> <mmultiscripts> <mtext>FOL</mtext> <mrow /> <mrow> <mrow /> <mo>∗</mo> <mo>+</mo> </mrow> </mmultiscripts> </math></EquationSource> </InlineEquation>, and propose a satisfiability checking algorithm, <Emphasis FontCategory="SansSerif">LEGOS-A</Emphasis>, for <InlineEquation ID="IEq5"> <EquationSource Format="TEX">$\hbox {FOL}^{+}$</EquationSource> <EquationSource Format="MATHML"><math> <mmultiscripts> <mtext>FOL</mtext> <mrow /> <mrow> <mrow /> <mo>∗</mo> <mo>+</mo> </mrow> </mmultiscripts> </math></EquationSource> </InlineEquation> which supports reasoning about aggregation by over- and under-approximating the aggregated values and incrementally refining these approximations to derive the satisfiability result. Running <Emphasis FontCategory="SansSerif">LEGOS-A</Emphasis> on real world and academic examples with aggregation from various domains showed that <Emphasis FontCategory="SansSerif">LEGOS-A</Emphasis> was able to solve many previously intractable problems and provided substantial speed-ups compared to the state-of-the-art <InlineEquation ID="IEq6"> <EquationSource Format="TEX">$\hbox {FOL}^$</EquationSource> <EquationSource Format="MATHML"><math> <msup> <mtext>FOL</mtext> <mo>∗</mo> </msup> </math></EquationSource> </InlineEquation> satisfiability checker and other SMT-based alternatives.</p>

Bounded satisfiability checking of $\hbox {FOL}^*$ formulas with aggregations

期刊论文
发表日期：

2025年11月21日

查看全文

Nick Feng,
Lina Marsso,
Yuliia Kholodetska,
Marsha Chechik

摘要

Software systems handling data are increasingly required to comply with legal properties (LPs) aimed at ensuring security and data privacy. Automated reasoning of LPs can be carried out by solving constraint satisfiability problems in first-order logic. However, the current logic-based reasoning approaches have limited support for capturing and reasoning about LPs with aggregation constraints, which are commonly found in financial and privacy policies. In this work, we extend first-order logic with quantifiers over relational objects ( $\hbox {FOL}^*$ ${FOL}^{*}$ ) to support aggregation, resulting in a language $\hbox {FOL}^{*+}$ ${FOL}^{* +}$ , and propose a satisfiability checking algorithm, LEGOS-A, for $\hbox {FOL}^{*+}$ ${FOL}^{* +}$ which supports reasoning about aggregation by over- and under-approximating the aggregated values and incrementally refining these approximations to derive the satisfiability result. Running LEGOS-A on real world and academic examples with aggregation from various domains showed that LEGOS-A was able to solve many previously intractable problems and provided substantial speed-ups compared to the state-of-the-art $\hbox {FOL}^*$ ${FOL}^{*}$ satisfiability checker and other SMT-based alternatives.

Bounded satisfiability checking of \(\hbox {FOL}^*\) formulas with aggregations

摘要