research-article

Performance improvement on legal model checking

Authors:

Carlos Faciano,

Fernando Schapachnik,

Ana Haydée Di Iorio,

Bibiana Luz Clara,

Verónica Uriarte,

María Fernanda Giaccaglia,

María Belén Ruffa,

Cristian MarcosAuthors Info & Claims

ICAIL '17: Proceedings of the 16th edition of the International Conference on Articial Intelligence and Law

Pages 59 - 68

https://doi.org/10.1145/3086512.3086518

Published: 12 June 2017 Publication History

Abstract

This article describes several performance improvements that allowed FormaLex, a tool developed to model check legal documents to find coherence problems, to process a real case study of the Argentinian Customer Protection Act. The described truth-preserving techniques reduce the model checking state space by improving the representation of actions and filtering language constructs that are used to encode the law.

References

[1]

Thomas Ball, Vladimir Levin, and Sriram K. Rajamani. 2011. A Decade of Software Model Checking with SLAM. Commun. ACM 54, 7 (July 2011), 68--76.

Digital Library

[2]

Juan Pablo Benedetti. 2014. Improving F<scp>orma</scp>L<scp>ex</scp>, a tool for normative analysis and automatic flaw detection. Master's thesis. Depto de Computación, Facultad de Ciencias Exactas y Naturales, UBA. http://www.dc.uba.ar/inv/tesis/licenciatura/2014/benedetti.pdf

[3]

A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. 2000. NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer (STTT) 2, 4 (2000), 410--425.

[4]

Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. 2002. Integrating BDD-Based and SAT-Based Symbolic Model Checking. Springer Berlin Heidelberg, Berlin, Heidelberg, 49--56.

Digital Library

[5]

Silvano Colombo Tosatto, Guido Governatori, and Pierre Kelsen. 2015. Business Process Regulatory Compliance is Hard. IEEE Trans. Services Computing 8, 6 (2015), 958--970.

[6]

Carlos Faciano. 2016. Optimizing the peformance of the FormaLex legal coherence checker. Master's thesis. Depto de Computación, Facultad de Ciencias Exactas y Naturales, UBA. http://www.dc.uba.ar/inv/tesis/licenciatura/2016/faciano.pdf

[7]

Stephen Fenech, Gordon J. Pace, and Gerardo Schneider. 2009. CLAN: A Tool for Contract Analysis and Conflict Discovery. In ATVA (Lecture Notes in Computer Science), Zhiming Liu and Anders P. Ravn (Eds.), Vol. 5799. Springer, 90--96.

Digital Library

[8]

Ulrich Furbach, Claudia Schon, and Frieder Stolzenburg. 2014. Automated Reasoning in Deontic Logic. In Multi-disciplinary Trends in Artificial Intelligence - 8th International Workshop, MIWAI 2014, Bangalore, India, December 8--10, 2014. Proceedings (Lecture Notes in Computer Science), M. Narasimha Murty, Xiangjian He, Chillarige Raghavendra Rao, and Paul Weng (Eds.), Vol. 8875. Springer, 57--68.

Digital Library

[9]

D. Giannakopoulou and J. Magee. 2003. Fluent model checking for event-based systems. ACM SIGSOFT Software Engineering Notes 28, 5 (2003), 266.

Digital Library

[10]

Daniel Gorín, Sergio Mera, and Fernando Schapachnik. 2010. Model Checking Legal Documents. In Proceedings of the 2010 conference on Legal Knowledge and Information Systems: JURIX 2010. 111--115.

Digital Library

[11]

Daniel Gorín, Sergio Mera, and Fernando Schapachnik. 2011. A Software Tool for Legal Drafting. In FLACOS 2011: Fifth Workshop on Formal Languages and Analysis of Contract-Oriented Software. Elsevier, 1--15.

[12]

Guido Governatori. 2015. Thou shalt is not you will. In Proceedings of the 15th International Conference on Artificial Intelligence and Law, ICAIL 2015, San Diego, CA, USA, June 8--12, 2015, Ted Sichelman and Katie Atkinson (Eds.). ACM, 63--68.

Digital Library

[13]

Guido Governatori and Duy Hoang Pham. 2009. DR-CONTRACT: an architecture for e-contracts in defeasible logic. IJBPIM 4 (2009), 187--199.

[14]

Guido Governatori and Sidney Shek. 2013. Regorous: A Business Process Compliance Checker. In Proceedings of the Fourteenth International Conference on Artificial Intelligence and Law (ICAIL '13). ACM, New York, NY, USA, 245--246.

Digital Library

[15]

Orna Grumberg and Helmut Veith. 2008. 25 years of model checking: history, achievements, perspectives. Vol. 5000. Springer.

Digital Library

[16]

María Celeste Gunski and Melisa Gabriela Raiczyk. 2016. FormaLex: improving expressive power of the FL language for the detection of normative flaws. Master's thesis. Depto de Computación, Facultad de Ciencias Exactas y Naturales, UBA. http://www.dc.uba.ar/inv/tesis/licenciatura/2016/gunski.pdf

[17]

Antonín Kučera and Jan Strejček. 2005. The stuttering principle revisited. Acta Informatica 41, 7 (2005), 415--434.

Digital Library

[18]

Ho-Pun Lam and Guido Governatori. 2009. The Making of SPINdle. In RuleML 2009. Springer, 315--322.

Digital Library

[19]

G. Pace, C. Prisacariu, and G. Schneider. 2007. Model Checking Contracts - A Case Study. Automated Technology for Verification and Analysis (2007), 82--97.

Digital Library

[20]

Gordon J. Pace, Fernando Schapachnik, and Gerardo Schneider. 2015. Conditional Permissions in Contracts. In Legal Knowledge and Information Systems - JURIX 2015: The Twenty-Eighth Annual Conference, Braga, Portual, December 10--11, 2015 (Frontiers in Artificial Intelligence and Applications), Vol. 279. IOS Press, 61--70.

[21]

Ellis Solaiman, Carlos Molina-jimenez, and Santosh Shrivastava. 2003. Model Checking Correctness Properties of Electronic Contracts. In Proceedings of the International conference on Service Oriented Computing (ICSOC03). Springer-Verlag, 303--318.

[22]

Sebastián Sznur, Juan Martín Brun, María Belén Ruffa, Máximo Martínez, and Fernando Schapachnik. 2014. Análisis de consistencia de la legislación de defensa al consumidor mediante métodos formales. In CIIDDI 2014, Tercer Congreso Iberoamericano de Investigadores y Docentes de Derecho e Informática.

[23]

Willem Visser, Matthew B Dwyer, and Michael Whalen. 2012. The hidden models of model checking. Software & Systems Modeling 11, 4 (2012), 541--555.

Digital Library

[24]

Bozena Woźna, Alessio Lomuscio, and Wojciech Penczek. 2005. Bounded Model Checking for Deontic Interpreted Systems. Electronic Notes in Theoretical Computer Science 126 (2005), 93 -- 114. Proceedings of the 2nd International Workshop on Logic and Communication in Multi-Agent Systems (2004). Logic and Communication in Multi-Agent Systems 2004.

Cited By

Khoja AKölbl MLeue SWilhelmi R(2022)Automated Consistency Analysis for Legal ContractsModel Checking Software10.1007/978-3-031-15077-7_1(1-23)Online publication date: 23-Aug-2022
https://doi.org/10.1007/978-3-031-15077-7_1
Lauritsen MSteenhuis Q(2019)Substantive Legal Software QualityProceedings of the Seventeenth International Conference on Artificial Intelligence and Law10.1145/3322640.3326706(52-62)Online publication date: 17-Jun-2019
https://dl.acm.org/doi/10.1145/3322640.3326706

Index Terms

Performance improvement on legal model checking
1. Applied computing
  1. Law, social and behavioral sciences
    1. Law
2. Theory of computation
  1. Logic
    1. Automated reasoning
    2. Verification by model checking

Recommendations

DocLog: An Electronic Contract Representation Language
DEXA '00: Proceedings of the 11th International Workshop on Database and Expert Systems Applications

The legal aspects of electronic commerce have attracted widespread attention. Many organisations have expressed their concern regarding the legal framework of the Internet and electronic commerce in particular. For small and medium sized enterprises (...
A logical model of directed obligations and permissions to support electronic contracting
Special issue: Formal aspects of digital commerce

In electronic commerce paper-based trade documents are replaced by electronic messages that can be processed automatically by computer applications. Electronic contracting and negotiating is an advanced type of automated processing of electronic ...
Towards model checking interpreted systems
AAMAS '03: Proceedings of the second international joint conference on Autonomous agents and multiagent systems

We show how it is possible to pair the NuSMV model checker with Akka, a software platform used to check validity of propositional modal formulas, to verify static properties of multi-agent systems formalised on interpreted systems semantics.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICAIL '17: Proceedings of the 16th edition of the International Conference on Articial Intelligence and Law

June 2017

299 pages

ISBN:9781450348911

DOI:10.1145/3086512

Conference Chair:
Jeroen Keppens
King's College London, United Kingdom
,
Program Chair:
Guido Governatori
Data61, CSIRO, Australia

Copyright © 2017 ACM.

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].

Sponsors

SIGAI: ACM Special Interest Group on Artificial Intelligence

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 June 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

UBACyT

Conference

ICAIL '17

Sponsor:

SIGAI

ICAIL '17: Sixteenth International Conference on Artificial Intelligence and Law

June 12 - 16, 2017

London, United Kingdom

Acceptance Rates

Overall Acceptance Rate 69 of 169 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
92
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Khoja AKölbl MLeue SWilhelmi R(2022)Automated Consistency Analysis for Legal ContractsModel Checking Software10.1007/978-3-031-15077-7_1(1-23)Online publication date: 23-Aug-2022
https://doi.org/10.1007/978-3-031-15077-7_1
Lauritsen MSteenhuis Q(2019)Substantive Legal Software QualityProceedings of the Seventeenth International Conference on Artificial Intelligence and Law10.1145/3322640.3326706(52-62)Online publication date: 17-Jun-2019
https://dl.acm.org/doi/10.1145/3322640.3326706

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten