Cited By
View all- Cristiá MRossi G(2024)A Practical Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted QuantifiersJournal of Automated Reasoning10.1007/s10817-024-09713-668:4Online publication date: 24-Oct-2024
A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
Article No.: 3, Pages 1 - 34
Abstract
In this paper we extend a decision procedure for the Boolean algebra of finite sets with cardinality constraints (ℒ|⋅|) to a decision procedure for ℒ|⋅| extended with set terms denoting finite integer intervals (ℒ[]). In ℒ[] interval limits can be integer linear terms including unbounded variables. These intervals are a useful extension because they allow to express non-trivial set operators such as the minimum and maximum of a set, still in a quantifier-free logic. Hence, by providing a decision procedure for ℒ[] it is possible to automatically reason about a new class of quantifier-free formulas. The decision procedure is implemented as part of the {log} (‘setlog’) tool. The paper includes a case study based on the elevator algorithm showing that {log} can automatically discharge all its invariance lemmas, some of which involve intervals.
References
[1]
J.-R. Abrial. 1996. The B-book: Assigning Programs to Meanings. Cambridge University Press, New York, NY, USA.
[2]
M. Leuschel and M. Butler. 2003. ProB: A model checker for B. In FME, Vol. 2805 of Lecture Notes in Computer Science. A. Keijiro, S. Gnesi, D. Mandrioli (Eds.), Springer-Verlag, 855–874.
[3]
Clearsy, Atelier B home page, http://www.atelierb.eu/
[4]
C. G. Zarba. 2002. Combining sets with integers. In Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8–10, 2002, Proceedings, A. Armando (Ed.), Vol. 2309 of Lecture Notes in Computer Science, Springer, 103–116. DOI:
[5]
V. Kuncak, H. H. Nguyen, and M. C. Rinard. 2006. Deciding Boolean algebra with Presburger arithmetic. J. Autom. Reason. 36, 3 (2006), 213–239. DOI:
[6]
K. Bansal, C. W. Barrett, A. Reynolds, and C. Tinelli. 2018. Reasoning with finite sets and cardinality constraints in SMT, Log. Methods Comput. Sci. 14, 4 (2018). DOI:
[7]
M. Cristiá and G. Rossi. 2023. Integrating cardinality constraints into constraint logic programming with sets. Theory Pract. Log. Program. 23, 2 (2023), 468–502. DOI:
[8]
A. R. Bradley, Z. Manna, and H. B. Sipma. 2006. What’s decidable about arrays?. In Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8–10, 2006, E. A. Emerson, K. S. Namjoshi (Eds.), Proceedings, Vol. 3855 of Lecture Notes in Computer Science, Springer, 427–442. DOI:
[9]
Z. Su and D. A. Wagner. 2005. A class of polynomially solvable range constraints for interval analysis without widenings, Theor. Comput. Sci. 345, 1 (2005), 122–138. DOI:
[10]
A. Dovier, C. Piazza, E. Pontelli, and G. Rossi. 2000. Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22, 5 (2000), 861–931.
[11]
M. Cristiá and G. Rossi. 2020. Solving quantifier-free first-order constraints over finite sets and binary relations. J. Autom. Reason. 64, 2 (2020), 295–330. DOI:
[12]
M. Cristiá and G. Rossi. 2021. Automated reasoning with restricted intensional sets. J. Autom. Reason. 65, 6 (2021), 809–890. DOI:
[13]
A. Dovier, E. G. Omodeo, E. Pontelli, and G. Rossi. 1996. A language for programming in logic with finite sets. J. Log. Program. 28, 1 (1996), 1–44. DOI:
[14]
G. Rossi. 2008. \(\lbrace log\rbrace\), http://www.clpset.unipr.it/setlog.Home.html, last access 2022 (2008).
[15]
M. Cristiá and G. Rossi. 2021. Automated proof of Bell-LaPadula security properties. J. Autom. Reason. 65, 4 (2021), 463–478. DOI:
[16]
M. Cristiá and G. Rossi. 2021. An automatically verified prototype of the Tokeneer ID station specification. J. Autom. Reason. 65, 8 (2021), 1125–1151. DOI:
[17]
A. Dovier, E. Pontelli, and G. Rossi. 2006. Set unification. Theory Pract. Log. Program. 6, 6 (2006), 645–701. DOI:
[18]
J. Eriksson and M. Parsa. 2020. A DSL for integer range reasoning: Partition, interval and mapping diagrams, In Practical Aspects of Declarative Languages - 22nd International Symposium, PADL 2020, New Orleans, LA, USA, January 20–21, 2020, E. Komendantskaya, Y. A. Liu (Eds.), Proceedings, Vol. 12007 of Lecture Notes in Computer Science, Springer, 196–212. DOI:
[19]
C. Holzbaur. 1995. OFAI CLP(Q,R) manual, Tech. rep., edition 1.3.3. Technical Report TR-95-09, Austrian Research Institute for Artificial Intelligence. http://www.ofai.at/cgi-bin/tr-online?number+95-09
[20]
J. M. Howe and A. King. 2012. A pearl on SAT and SMT solving in Prolog. Theor. Comput. Sci. 435, (2012) 43–55. DOI:
[21]
M. Cristiá and G. Rossi. 2019. Rewrite rules for a solver for sets, binary relations and partial functions. Tech. rep.https://www.clpset.unipr.it/SETLOG/calculus.pdf
[22]
M. Cristiá and G. Rossi. 2018. A set solver for finite set relation algebra. In Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 - November 1, 2018, J. Desharnais, W. Guttmann, S. Joosten (Eds.), Proceedings, Vol. 11194 of Lecture Notes in Computer Science, Springer, 333–349. DOI:
[23]
M. Cristiá, G. Rossi, and C. S. Frydman. 2013. \(\lbrace log\rbrace\) as a test case generator for the Test Template Framework. In SEFM, R. M. Hierons, M. G. Merayo, M. Bravetti (Eds.), Vol. 8137 of Lecture Notes in Computer Science, Springer, 229–243.
[24]
J. F. Allen. 1983. Maintaining knowledge about temporal intervals. Commun. ACM 26, 11 (1983), 832–843. DOI:
[25]
D. Mentré, C. Marché, J.-C. Filliâtre, and M. Asuka. 2012. Discharging proof obligations from Atelier B using multiple automated provers. In ABZ, J. Derrick, J. A. Fitzgerald, S. Gnesi, S. Khurshid, M. Leuschel, S. Reeves, E. Riccobene (Eds.), Vol. 7316 of Lecture Notes in Computer Science, Springer, 238–251.
[26]
W. Harvey and P. J. Stuckey. 2003. Improving linear constraint propagation by changing constraint representation. Constraints an Int. J. 8, 2 (2003), 173–207. DOI:
[27]
K. R. Apt and P. Zoeteweij. 2007. An analysis of arithmetic constraints on integer intervals. Constraints an Int. J. 12, 4 (2007), 429–468. DOI:
[28]
L. Bozzelli, A. Molinari, A. Montanari, and A. Peron. 2020. Model checking interval temporal logics with regular expressions. Inf. Comput. 272, (2020), 104498. DOI:
[29]
A. A. Krokhin, P. Jeavons, and P. Jonsson. 2003. Reasoning about temporal relations: The tractable subalgebras of Allen’s interval algebra. J. ACM 50, 5 (2003), 591–640. DOI:
[30]
P. B. Ladkin. 1987. The completeness of a natural system for reasoning with time intervals. In Proceedings of the 10th International Joint Conference on Artificial Intelligence. Milan, Italy, August 23-28, 1987, Morgan Kaufmann, J. P. McDermott (Ed.), 462–465. DOI:http://ijcai.org/Proceedings/87-1/Papers/091.pdf
[31]
T. Janhunen and M. Sioutis. 2019. Allen’s interval algebra makes the difference. In Declarative Programming and Knowledge Management - Conference on Declarative Programming, DECLARE 2019, Unifying INAP, WLP, and WFLP, Cottbus, Germany, September 9-12, 2019, P. Hofstedt, S. Abreu, U. John, H. Kuchen, D. Seipel (Eds.), Revised Selected Papers, Vol. 12057 of Lecture Notes in Computer Science, Springer, 89–98. DOI:
Index Terms
- A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
Recommendations
Finite-Memory Systems
Let K be a field, k and n positive integers and let A_1, \ldots ,A_k be n \times n- matrices with coefficients in K . For any function \[ g\colon \Gamma:= \{ t:=(t_1, ldots ,t_k) in N^k \vert t_1 t_2 \ldots t_k = 0 \} \ \to \ K^n \] there exists a ...
Well quasi orders and the shuffle closure of finite sets
DLT'06: Proceedings of the 10th international conference on Developments in Language TheoryGiven a set I of words, the set L$_{\rm \vdash}^{\epsilon}~_{\rm I}$ of all words obtained by the shuffle of (copies of) words of I is naturally provided with a partial order: for u, v in L$_{\rm \vdash}^{\epsilon}~_{\rm I}$, u$\vdash^{\rm *}_{I}$v if ...
Comments
Information & Contributors
Information
Published In
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 18 November 2023
Online AM: 22 September 2023
Accepted: 29 August 2023
Received: 03 November 2022
Published in TOCL Volume 25, Issue 1
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 102Total Downloads
- Downloads (Last 12 months)94
- Downloads (Last 6 weeks)5
Reflects downloads up to 22 Oct 2024
Other Metrics
Citations
Cited By
View all- Cristiá MRossi G(2024)A Practical Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted QuantifiersJournal of Automated Reasoning10.1007/s10817-024-09713-668:4Online publication date: 24-Oct-2024
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in