Showing 1–49 of 49 results for author: Arias, J

Modeling (Deontic) Modal Operators With the s(CASP) Goal-directed Predicated Answer Set Programming System

Authors: Gopal Gupta, Abhiramon Rajasekharan, Alexis R. Tudor, Elmer Salazar, Joaquín Arias

Abstract: We consider the problem of implementing deontic modal logic. We show how (deontic) modal operators can be expressed elegantly using default negation (negation-as-failure) and strong negation present in answer set programming (ASP). We propose using global constraints of ASP to represent obligations and impermissibilities of deontic modal logic. We show that our proposed representation results in t… ▽ More We consider the problem of implementing deontic modal logic. We show how (deontic) modal operators can be expressed elegantly using default negation (negation-as-failure) and strong negation present in answer set programming (ASP). We propose using global constraints of ASP to represent obligations and impermissibilities of deontic modal logic. We show that our proposed representation results in the various paradoxes of deontic modal logic being elegantly resolved. △ Less

Submitted 7 July, 2025; originally announced July 2025.

Building Trustworthy AI by Addressing its 16+2 Desiderata with Goal-Directed Commonsense Reasoning

Authors: Alexis R. Tudor, Yankai Zeng, Huaduo Wang, Joaquin Arias, Gopal Gupta

Abstract: Current advances in AI and its applicability have highlighted the need to ensure its trustworthiness for legal, ethical, and even commercial reasons. Sub-symbolic machine learning algorithms, such as the LLMs, simulate reasoning but hallucinate and their decisions cannot be explained or audited (crucial aspects for trustworthiness). On the other hand, rule-based reasoners, such as Cyc, are able to… ▽ More Current advances in AI and its applicability have highlighted the need to ensure its trustworthiness for legal, ethical, and even commercial reasons. Sub-symbolic machine learning algorithms, such as the LLMs, simulate reasoning but hallucinate and their decisions cannot be explained or audited (crucial aspects for trustworthiness). On the other hand, rule-based reasoners, such as Cyc, are able to provide the chain of reasoning steps but are complex and use a large number of reasoners. We propose a middle ground using s(CASP), a goal-directed constraint-based answer set programming reasoner that employs a small number of mechanisms to emulate reliable and explainable human-style commonsense reasoning. In this paper, we explain how s(CASP) supports the 16 desiderata for trustworthy AI introduced by Doug Lenat and Gary Marcus (2023), and two additional ones: inconsistency detection and the assumption of alternative worlds. To illustrate the feasibility and synergies of s(CASP), we present a range of diverse applications, including a conversational chatbot and a virtually embodied reasoner. △ Less

Submitted 14 June, 2025; originally announced June 2025.

VECSR: Virtually Embodied Common Sense Reasoning System

Authors: Alexis R. Tudor, Joaquín Arias, Gopal Gupta

Abstract: The development of autonomous agents has seen a revival of enthusiasm due to the emergence of LLMs, such as GPT-4o. Deploying these agents in environments where they coexist with humans (e.g., as domestic assistants) requires special attention to trustworthiness and explainability. However, the use of LLMs and other deep learning models still does not resolve these key issues. Deep learning system… ▽ More The development of autonomous agents has seen a revival of enthusiasm due to the emergence of LLMs, such as GPT-4o. Deploying these agents in environments where they coexist with humans (e.g., as domestic assistants) requires special attention to trustworthiness and explainability. However, the use of LLMs and other deep learning models still does not resolve these key issues. Deep learning systems may hallucinate, be unable to justify their decisions as black boxes, or perform badly on unseen scenarios. In this work, we propose the use of s(CASP), a goal-directed common sense reasoner based on Answer Set Programming, to break down the high-level tasks of an autonomous agent into mid-level instructions while justifying the selection of these instructions. To validate its use in real applications we present a framework that integrates the reasoner into the VirtualHome simulator and compares its accuracy with GPT-4o, running some of the real use cases available in the domestic environments of VirtualHome. Additionally, since experiments with VirtualHome have shown the need to reduce the response time (which increases as the agent's decision space grows), we have proposed and evaluated a series of optimizations based on program analysis that exploit the advantages of the top-down execution of s(CASP). △ Less

Submitted 4 May, 2025; originally announced May 2025.

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study

Authors: Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias, Marc Lelarge

Abstract: In this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources: a natural language description, the Lean formalization, and the Isabelle formalization. We conducted our experiment in 3 stages of increasing complexity, from basic one-shot prompting to multi-turn conversations that in… ▽ More In this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources: a natural language description, the Lean formalization, and the Isabelle formalization. We conducted our experiment in 3 stages of increasing complexity, from basic one-shot prompting to multi-turn conversations that incorporate feedback from unsuccessful attempts. At each stage, we perform multiple rounds of translation using increasingly advanced models: GPT-4o mini, Claude 3.5 Sonnet, o1 mini, and o1. We successfully translated 478 out of 488 theorems. The dataset is opensource: https://github.com/LLM4Rocq/miniF2F-rocq. △ Less

Submitted 11 February, 2025; originally announced March 2025.

CoGS: Model Agnostic Causality Constrained Counterfactual Explanations using goal-directed ASP

Authors: Sopam Dasgupta, Joaquín Arias, Elmer Salazar, Gopal Gupta

Abstract: Machine learning models are increasingly used in critical areas such as loan approvals and hiring, yet they often function as black boxes, obscuring their decision-making processes. Transparency is crucial, as individuals need explanations to understand decisions, primarily if the decisions result in an undesired outcome. Our work introduces CoGS (Counterfactual Generation with s(CASP)), a model-a… ▽ More Machine learning models are increasingly used in critical areas such as loan approvals and hiring, yet they often function as black boxes, obscuring their decision-making processes. Transparency is crucial, as individuals need explanations to understand decisions, primarily if the decisions result in an undesired outcome. Our work introduces CoGS (Counterfactual Generation with s(CASP)), a model-agnostic framework capable of generating counterfactual explanations for classification models. CoGS leverages the goal-directed Answer Set Programming system s(CASP) to compute realistic and causally consistent modifications to feature values, accounting for causal dependencies between them. By using rule-based machine learning algorithms (RBML), notably the FOLD-SE algorithm, CoGS extracts the underlying logic of a statistical model to generate counterfactual solutions. By tracing a step-by-step path from an undesired outcome to a desired one, CoGS offers interpretable and actionable explanations of the changes required to achieve the desired outcome. We present details of the CoGS framework along with its evaluation. △ Less

Submitted 29 October, 2024; originally announced October 2024.

Comments: arXiv admin note: substantial text overlap with arXiv:2407.08179

Automating Semantic Analysis of System Assurance Cases using Goal-directed ASP

Authors: Anitha Murugesan, Isaac Wong, Joaquín Arias, Robert Stroud, Srivatsan Varadarajan, Elmer Salazar, Gopal Gupta, Robin Bloomfield, John Rushby

Abstract: Assurance cases offer a structured way to present arguments and evidence for certification of systems where safety and security are critical. However, creating and evaluating these assurance cases can be complex and challenging, even for systems of moderate complexity. Therefore, there is a growing need to develop new automation methods for these tasks. While most existing assurance case tools foc… ▽ More Assurance cases offer a structured way to present arguments and evidence for certification of systems where safety and security are critical. However, creating and evaluating these assurance cases can be complex and challenging, even for systems of moderate complexity. Therefore, there is a growing need to develop new automation methods for these tasks. While most existing assurance case tools focus on automating structural aspects, they lack the ability to fully assess the semantic coherence and correctness of the assurance arguments. In prior work, we introduced the Assurance 2.0 framework that prioritizes the reasoning process, evidence utilization, and explicit delineation of counter-claims (defeaters) and counter-evidence. In this paper, we present our approach to enhancing Assurance 2.0 with semantic rule-based analysis capabilities using common-sense reasoning and answer set programming solvers, specifically s(CASP). By employing these analysis techniques, we examine the unique semantic aspects of assurance cases, such as logical consistency, adequacy, indefeasibility, etc. The application of these analyses provides both system developers and evaluators with increased confidence about the assurance case. △ Less

Submitted 1 October, 2024; v1 submitted 21 August, 2024; originally announced August 2024.

Journal ref: Theory and Practice of Logic Programming 24 (2024) 805-824

Early Validation of High-level System Requirements with Event Calculus and Answer Set Programming

Authors: Ondřej Vašíček, Joaquin Arias, Jan Fiedor, Gopal Gupta, Brendan Hall, Bohuslav Křena, Brian Larson, Sarat Chandra Varanasi, Tomáš Vojnar

Abstract: This paper proposes a new methodology for early validation of high-level requirements on cyber-physical systems with the aim of improving their quality and, thus, lowering chances of specification errors propagating into later stages of development where it is much more expensive to fix them. The paper presents a transformation of a real-world requirements specification of a medical device$-$a PCA… ▽ More This paper proposes a new methodology for early validation of high-level requirements on cyber-physical systems with the aim of improving their quality and, thus, lowering chances of specification errors propagating into later stages of development where it is much more expensive to fix them. The paper presents a transformation of a real-world requirements specification of a medical device$-$a PCA pump$-$into an Event Calculus model that is then evaluated using answer set programming and the s(CASP) system. The evaluation under s(CASP) allowed deductive as well as abductive reasoning about the specified functionality of the PCA pump on the conceptual level with minimal implementation or design dependent influences, and led to fully-automatically detected nuanced violations of critical safety properties. Further, the paper discusses scalability and non-termination challenges that had to be faced in the evaluation and techniques proposed to (partially) solve them. Finally, ideas for improving s(CASP) to overcome its evaluation limitations that still persist as well as to increase its expressiveness are presented. △ Less

Submitted 19 August, 2024; originally announced August 2024.

Comments: Accepted for ICLP 2024

A Reliable Common-Sense Reasoning Socialbot Built Using LLMs and Goal-Directed ASP

Authors: Yankai Zeng, Abhiramon Rajashekharan, Kinjal Basu, Huaduo Wang, Joaquín Arias, Gopal Gupta

Abstract: The development of large language models (LLMs), such as GPT, has enabled the construction of several socialbots, like ChatGPT, that are receiving a lot of attention for their ability to simulate a human conversation. However, the conversation is not guided by a goal and is hard to control. In addition, because LLMs rely more on pattern recognition than deductive reasoning, they can give confusing… ▽ More The development of large language models (LLMs), such as GPT, has enabled the construction of several socialbots, like ChatGPT, that are receiving a lot of attention for their ability to simulate a human conversation. However, the conversation is not guided by a goal and is hard to control. In addition, because LLMs rely more on pattern recognition than deductive reasoning, they can give confusing answers and have difficulty integrating multiple topics into a cohesive response. These limitations often lead the LLM to deviate from the main topic to keep the conversation interesting. We propose AutoCompanion, a socialbot that uses an LLM model to translate natural language into predicates (and vice versa) and employs commonsense reasoning based on Answer Set Programming (ASP) to hold a social conversation with a human. In particular, we rely on s(CASP), a goal-directed implementation of ASP as the backend. This paper presents the framework design and how an LLM is used to parse user messages and generate a response from the s(CASP) engine output. To validate our proposal, we describe (real) conversations in which the chatbot's goal is to keep the user entertained by talking about movies and books, and s(CASP) ensures (i) correctness of answers, (ii) coherence (and precision) during the conversation, which it dynamically regulates to achieve its specific purpose, and (iii) no deviation from the main topic. △ Less

Submitted 26 July, 2024; originally announced July 2024.

Journal ref: Theory and Practice of Logic Programming 24 (2024) 606-627

CoGS: Causality Constrained Counterfactual Explanations using goal-directed ASP

Authors: Sopam Dasgupta, Joaquín Arias, Elmer Salazar, Gopal Gupta

Abstract: Machine learning models are increasingly used in areas such as loan approvals and hiring, yet they often function as black boxes, obscuring their decision-making processes. Transparency is crucial, and individuals need explanations to understand decisions, especially for the ones not desired by the user. Ethical and legal considerations require informing individuals of changes in input attribute v… ▽ More Machine learning models are increasingly used in areas such as loan approvals and hiring, yet they often function as black boxes, obscuring their decision-making processes. Transparency is crucial, and individuals need explanations to understand decisions, especially for the ones not desired by the user. Ethical and legal considerations require informing individuals of changes in input attribute values (features) that could lead to a desired outcome for the user. Our work aims to generate counterfactual explanations by considering causal dependencies between features. We present the CoGS (Counterfactual Generation with s(CASP)) framework that utilizes the goal-directed Answer Set Programming system s(CASP) to generate counterfactuals from rule-based machine learning models, specifically the FOLD-SE algorithm. CoGS computes realistic and causally consistent changes to attribute values taking causal dependencies between them into account. It finds a path from an undesired outcome to a desired one using counterfactuals. We present details of the CoGS framework along with its evaluation. △ Less

Submitted 11 July, 2024; originally announced July 2024.

Algorithms for learning value-aligned policies considering admissibility relaxation

Authors: Andrés Holgado-Sánchez, Joaquín Arias, Holger Billhardt, Sascha Ossowski

Abstract: The emerging field of \emph{value awareness engineering} claims that software agents and systems should be value-aware, i.e. they must make decisions in accordance with human values. In this context, such agents must be capable of explicitly reasoning as to how far different courses of action are aligned with these values. For this purpose, values are often modelled as preferences over states or a… ▽ More The emerging field of \emph{value awareness engineering} claims that software agents and systems should be value-aware, i.e. they must make decisions in accordance with human values. In this context, such agents must be capable of explicitly reasoning as to how far different courses of action are aligned with these values. For this purpose, values are often modelled as preferences over states or actions, which are then aggregated to determine the sequences of actions that are maximally aligned with a certain value. Recently, additional value admissibility constraints at this level have been considered as well. However, often relaxed versions of these constraints are needed, and this increases considerably the complexity of computing value-aligned policies. To obtain efficient algorithms that make value-aligned decisions considering admissibility relaxation, we propose the use of learning techniques, in particular, we have used constrained reinforcement learning algorithms. In this paper, we present two algorithms, $ε\text{-}ADQL$ for strategies based on local alignment and its extension $ε\text{-}CADQL$ for a sequence of decisions. We have validated their efficiency in a water distribution problem in a drought scenario. △ Less

Submitted 7 June, 2024; originally announced June 2024.

CFGs: Causality Constrained Counterfactual Explanations using goal-directed ASP

Authors: Sopam Dasgupta, Joaquín Arias, Elmer Salazar, Gopal Gupta

Abstract: Machine learning models that automate decision-making are increasingly used in consequential areas such as loan approvals, pretrial bail approval, and hiring. Unfortunately, most of these models are black boxes, i.e., they are unable to reveal how they reach these prediction decisions. A need for transparency demands justification for such predictions. An affected individual might also desire expl… ▽ More Machine learning models that automate decision-making are increasingly used in consequential areas such as loan approvals, pretrial bail approval, and hiring. Unfortunately, most of these models are black boxes, i.e., they are unable to reveal how they reach these prediction decisions. A need for transparency demands justification for such predictions. An affected individual might also desire explanations to understand why a decision was made. Ethical and legal considerations require informing the individual of changes in the input attribute (s) that could be made to produce a desirable outcome. Our work focuses on the latter problem of generating counterfactual explanations by considering the causal dependencies between features. In this paper, we present the framework CFGs, CounterFactual Generation with s(CASP), which utilizes the goal-directed Answer Set Programming (ASP) system s(CASP) to automatically generate counterfactual explanations from models generated by rule-based machine learning algorithms in particular. We benchmark CFGs with the FOLD-SE model. Reaching the counterfactual state from the initial state is planned and achieved using a series of interventions. To validate our proposal, we show how counterfactual explanations are computed and justified by imagining worlds where some or all factual assumptions are altered/changed. More importantly, we show how CFGs navigates between these worlds, namely, go from our initial state where we obtain an undesired outcome to the imagined goal state where we obtain the desired decision, taking into account the causal relationships among features. △ Less

Submitted 24 May, 2024; originally announced May 2024.

Comments: arXiv admin note: substantial text overlap with arXiv:2402.04382

Counterfactual Generation with Answer Set Programming

Authors: Sopam Dasgupta, Farhad Shakerin, Joaquín Arias, Elmer Salazar, Gopal Gupta

Abstract: Machine learning models that automate decision-making are increasingly being used in consequential areas such as loan approvals, pretrial bail approval, hiring, and many more. Unfortunately, most of these models are black-boxes, i.e., they are unable to reveal how they reach these prediction decisions. A need for transparency demands justification for such predictions. An affected individual might… ▽ More Machine learning models that automate decision-making are increasingly being used in consequential areas such as loan approvals, pretrial bail approval, hiring, and many more. Unfortunately, most of these models are black-boxes, i.e., they are unable to reveal how they reach these prediction decisions. A need for transparency demands justification for such predictions. An affected individual might also desire explanations to understand why a decision was made. Ethical and legal considerations may further require informing the individual of changes in the input attribute that could be made to produce a desirable outcome. This paper focuses on the latter problem of automatically generating counterfactual explanations. We propose a framework Counterfactual Generation with s(CASP) (CFGS) that utilizes answer set programming (ASP) and the s(CASP) goal-directed ASP system to automatically generate counterfactual explanations from rules generated by rule-based machine learning (RBML) algorithms. In our framework, we show how counterfactual explanations are computed and justified by imagining worlds where some or all factual assumptions are altered/changed. More importantly, we show how we can navigate between these worlds, namely, go from our original world/scenario where we obtain an undesired outcome to the imagined world/scenario where we obtain a desired/favourable outcome. △ Less

Submitted 6 February, 2024; originally announced February 2024.

Comments: 16 Pages

Del Visual al Auditivo: Sonorización de Escenas Guiada por Imagen

Authors: María Sánchez, Laura Fernández, Julián Arias, Mateo Cámara, Giulia Comini, Adam Gabrys, José Luis Blanco, Juan Ignacio Godino, Luis Alfonso Hernández

Abstract: Recent advances in image, video, text and audio generative techniques, and their use by the general public, are leading to new forms of content generation. Usually, each modality was approached separately, which poses limitations. The automatic sound recording of visual sequences is one of the greatest challenges for the automatic generation of multimodal content. We present a processing flow that… ▽ More Recent advances in image, video, text and audio generative techniques, and their use by the general public, are leading to new forms of content generation. Usually, each modality was approached separately, which poses limitations. The automatic sound recording of visual sequences is one of the greatest challenges for the automatic generation of multimodal content. We present a processing flow that, starting from images extracted from videos, is able to sound them. We work with pre-trained models that employ complex encoders, contrastive learning, and multiple modalities, allowing complex representations of the sequences for their sonorization. The proposed scheme proposes different possibilities for audio mapping and text guidance. We evaluated the scheme on a dataset of frames extracted from a commercial video game and sounds extracted from the Freesound platform. Subjective tests have evidenced that the proposed scheme is able to generate and assign audios automatically and conveniently to images. Moreover, it adapts well to user preferences, and the proposed objective metrics show a high correlation with the subjective ratings. △ Less

Submitted 2 February, 2024; originally announced February 2024.

Comments: 10 pages, in Spanish, Tecniacústica

Automated legal reasoning with discretion to act using s(LAW)

Authors: Joaquín Arias, Mar Moreno-Rebato, José A. Rodríguez-García, Sascha Ossowski

Abstract: Automated legal reasoning and its application in smart contracts and automated decisions are increasingly attracting interest. In this context, ethical and legal concerns make it necessary for automated reasoners to justify in human-understandable terms the advice given. Logic Programming, specially Answer Set Programming, has a rich semantics and has been used to very concisely express complex kn… ▽ More Automated legal reasoning and its application in smart contracts and automated decisions are increasingly attracting interest. In this context, ethical and legal concerns make it necessary for automated reasoners to justify in human-understandable terms the advice given. Logic Programming, specially Answer Set Programming, has a rich semantics and has been used to very concisely express complex knowledge. However, modelling discretionality to act and other vague concepts such as ambiguity cannot be expressed in top-down execution models based on Prolog, and in bottom-up execution models based on ASP the justifications are incomplete and/or not scalable. We propose to use s(CASP), a top-down execution model for predicate ASP, to model vague concepts following a set of patterns. We have implemented a framework, called s(LAW), to model, reason, and justify the applicable legislation and validate it by translating (and benchmarking) a representative use case, the criteria for the admission of students in the "Comunidad de Madrid". △ Less

Submitted 25 January, 2024; originally announced January 2024.

ACM Class: I.2.1

Journal ref: Artificial Intelligence and Law (2023)

A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets

Authors: Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, Laure Petrucci

Abstract: This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the "standard" semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and comp… ▽ More This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the "standard" semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude -- including full LTL model checking, analysis with user-defined analysis strategies, and even statistical model checking -- for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Romeo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Romeo in many cases. △ Less

Submitted 12 September, 2024; v1 submitted 3 January, 2024; originally announced January 2024.

Comments: arXiv admin note: substantial text overlap with arXiv:2303.08929

Journal ref: Fundamenta Informaticae, Volume 192, Issues 3-4: Petri Nets 2023 (November 10, 2024) fi:12781

Counterfactual Explanation Generation with s(CASP)

Authors: Sopam Dasgupta, Farhad Shakerin, Joaquín Arias, Elmer Salazar, Gopal Gupta

Abstract: Machine learning models that automate decision-making are increasingly being used in consequential areas such as loan approvals, pretrial bail, hiring, and many more. Unfortunately, most of these models are black-boxes, i.e., they are unable to reveal how they reach these prediction decisions. A need for transparency demands justification for such predictions. An affected individual might desire e… ▽ More Machine learning models that automate decision-making are increasingly being used in consequential areas such as loan approvals, pretrial bail, hiring, and many more. Unfortunately, most of these models are black-boxes, i.e., they are unable to reveal how they reach these prediction decisions. A need for transparency demands justification for such predictions. An affected individual might desire explanations to understand why a decision was made. Ethical and legal considerations may further require informing the individual of changes in the input attribute that could be made to produce a desirable outcome. This paper focuses on the latter problem of automatically generating counterfactual explanations. Our approach utilizes answer set programming and the s(CASP) goal-directed ASP system. Answer Set Programming (ASP) is a well-known knowledge representation and reasoning paradigm. s(CASP) is a goal-directed ASP system that executes answer-set programs top-down without grounding them. The query-driven nature of s(CASP) allows us to provide justifications as proof trees, which makes it possible to analyze the generated counterfactual explanations. We show how counterfactual explanations are computed and justified by imagining multiple possible worlds where some or all factual assumptions are untrue and, more importantly, how we can navigate between these worlds. We also show how our algorithm can be used to find the Craig Interpolant for a class of answer set programs for a failing query. △ Less

Submitted 22 October, 2023; originally announced October 2023.

Comments: 18 Pages

Optimal Scheduling of Agents in ADTrees: Specialised Algorithm and Declarative Models

Authors: Jaime Arias, Carlos Olarte, Laure Petrucci, Łukasz Maśko, Wojciech Penczek, Teofil Sidoruk

Abstract: Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that syn… ▽ More Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using the minimal number of agents for a given attack-defence tree. We also investigate an alternative approach for the same problem using Rewriting Logic, starting with a simple and elegant declarative model, whose correctness (in terms of schedule's optimality) is self-evident. We then refine this specification, inspired by the design of our specialised algorithm, to obtain an efficient system that can be used as a playground to explore various aspects of attack-defence trees. We compare the two approaches on different benchmarks. △ Less

Submitted 19 October, 2023; v1 submitted 8 May, 2023; originally announced May 2023.

Comments: arXiv admin note: text overlap with arXiv:2101.06838

Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs

Authors: Yankai Zeng, Abhiramon Rajasekharan, Parth Padalkar, Kinjal Basu, Joaquín Arias, Gopal Gupta

Abstract: Achieving human-like communication with machines remains a classic, challenging topic in the field of Knowledge Representation and Reasoning and Natural Language Processing. These Large Language Models (LLMs) rely on pattern-matching rather than a true understanding of the semantic meaning of a sentence. As a result, they may generate incorrect responses. To generate an assuredly correct response,… ▽ More Achieving human-like communication with machines remains a classic, challenging topic in the field of Knowledge Representation and Reasoning and Natural Language Processing. These Large Language Models (LLMs) rely on pattern-matching rather than a true understanding of the semantic meaning of a sentence. As a result, they may generate incorrect responses. To generate an assuredly correct response, one has to "understand" the semantics of a sentence. To achieve this "understanding", logic-based (commonsense) reasoning methods such as Answer Set Programming (ASP) are arguably needed. In this paper, we describe the AutoConcierge system that leverages LLMs and ASP to develop a conversational agent that can truly "understand" human dialogs in restricted domains. AutoConcierge is focused on a specific domain-advising users about restaurants in their local area based on their preferences. AutoConcierge will interactively understand a user's utterances, identify the missing information in them, and request the user via a natural language sentence to provide it. Once AutoConcierge has determined that all the information has been received, it computes a restaurant recommendation based on the user-preferences it has acquired from the human user. AutoConcierge is based on our STAR framework developed earlier, which uses GPT-3 to convert human dialogs into predicates that capture the deep structure of the dialog's sentence. These predicates are then input into the goal-directed s(CASP) ASP system for performing commonsense reasoning. To the best of our knowledge, AutoConcierge is the first automated conversational agent that can realistically converse like a human and provide help to humans based on truly understanding human utterances. △ Less

Submitted 17 March, 2023; v1 submitted 15 March, 2023; originally announced March 2023.

Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving

Authors: Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, Laure Petrucci, Fredrik Rømming

Abstract: Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding a… ▽ More Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding approach for symbolic reachability that terminates whenever the parametric state-class graph of the PITPN is finite. We explain how almost all formal analysis and parameter synthesis supported by the state-of-the-art PITPN tool Roméo can be done in Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments on three benchmarks show that our methods outperform Roméo in many cases. △ Less

Submitted 15 March, 2023; originally announced March 2023.

Strategic (Timed) Computation Tree Logic

Authors: Jaime Arias, Wojciech Jamroga, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk

Abstract: We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, i.e., STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding inform… ▽ More We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, i.e., STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding information: imperfect (i) and perfect (I), and recall: imperfect (r) and perfect (R). We prove that SCTL is more expressive than ATL for all semantics, and this holds for the timed versions as well. Moreover, the model checking problem for SCTL[ir] is of the same complexity as for ATL[ir], the model checking problem for STCTL[ir] is of the same complexity as for TCTL, while for STCTL[iR] it is undecidable as for ATL[iR]. The above results suggest to use SCTL[ir] and STCTL[ir] in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTL[ir]. △ Less

Submitted 19 October, 2023; v1 submitted 26 February, 2023; originally announced February 2023.

Building Information Modeling Using Constraint Logic Programming

Authors: Joaquín Arias, Seppo Törmä, Manuel Carro, Gopal Gupta

Abstract: Building Information Modeling (BIM) produces three-dimensional models of buildings combining the geometrical information with a wide range of properties. BIM is slowly but inevitably revolutionizing the architecture, engineering, and construction (AEC) industry. Buildings need to be compliant with regulations about stability, safety, and environmental impact. Manual compliance checking is tedious… ▽ More Building Information Modeling (BIM) produces three-dimensional models of buildings combining the geometrical information with a wide range of properties. BIM is slowly but inevitably revolutionizing the architecture, engineering, and construction (AEC) industry. Buildings need to be compliant with regulations about stability, safety, and environmental impact. Manual compliance checking is tedious and error-prone, and amending flaws discovered only at construction time causes huge additional costs and delays. Several tools can check BIM models for conformance with rules/guidelines. For example, Singapore's CORENET e-Submission System checks fire safety. But since the current BIM exchange format only contains basic information of building objects, a separate, ad-hoc model pre-processing is required to determine, e.g., evacuation routes. Moreover, they face difficulties in adapting existing built-in rules and/or adding new ones (to cater for building regulations, that can vary not only among countries but also among parts of the same city), if at all possible. We propose the use of logic-based executable formalisms (CLP and Constraint ASP) to couple BIM models with advanced knowledge representation and reasoning capabilities. Previous experience shows that such formalisms can be used to uniformly capture and reason with knowledge (including ambiguity) in a large variety of domains. Additionally, incorporating checking within design tools makes it possible to ensure that models are rule-compliant at every step. This also prevents erroneous designs from having to be (partially) redone, which is also costly and burdensome. To validate our proposal, we implemented a preliminary reasoner under CLP(Q/R) and ASP with constraints and evaluated it with several BIM models. Under consideration for acceptance in Theory and Practice of Logic Programming (TPLP). △ Less

Submitted 17 May, 2022; originally announced May 2022.

Comments: Paper presented at the 38th International Conference on Logic Programming (ICLP 2022), 16 pages

Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming

Authors: Joaquín Arias, Manuel Carro, Gopal Gupta

Abstract: Goal-directed evaluation of Answer Set Programs is gaining traction thanks to its amenability to create AI systems that can, due to the evaluation mechanism used, generate explanations and justifications. s(CASP) is one of these systems and has been already used to write reasoning systems in several fields. It provides enhanced expressiveness w.r.t. other ASP systems due to its ability to use cons… ▽ More Goal-directed evaluation of Answer Set Programs is gaining traction thanks to its amenability to create AI systems that can, due to the evaluation mechanism used, generate explanations and justifications. s(CASP) is one of these systems and has been already used to write reasoning systems in several fields. It provides enhanced expressiveness w.r.t. other ASP systems due to its ability to use constraints, data structures, and unbound variables natively. However, the performance of existing s(CASP) implementations is not on par with other ASP systems: model consistency is checked once models have been generated, in keeping with the generate-and-test paradigm. In this work, we present a variation of the top-down evaluation strategy, termed Dynamic Consistency Checking, which interleaves model generation and consistency checking. This makes it possible to determine when a literal is not compatible with the denials associated to the global constraints in the program, prune the current execution branch, and choose a different alternative. This strategy is specially (but not exclusively) relevant in problems with a high combinatorial component. We have experimentally observed speedups of up to 90x w.r.t. the standard versions of s(CASP). △ Less

Submitted 22 October, 2021; originally announced October 2021.

Comments: Submitted to PADL'22. arXiv admin note: text overlap with arXiv:2106.14566

Knowledge-Assisted Reasoning of Model-Augmented System Requirements with Event Calculus and Goal-Directed Answer Set Programming

Authors: Brendan Hall, Sarat Chandra Varanasi, Jan Fiedor, Joaquín Arias, Kinjal Basu, Fang Li, Devesh Bhatt, Kevin Driscoll, Elmer Salazar, Gopal Gupta

Abstract: We consider requirements for cyber-physical systems represented in constrained natural language. We present novel automated techniques for aiding in the development of these requirements so that they are consistent and can withstand perceived failures. We show how cyber-physical systems' requirements can be modeled using the event calculus (EC), a formalism used in AI for representing actions and… ▽ More We consider requirements for cyber-physical systems represented in constrained natural language. We present novel automated techniques for aiding in the development of these requirements so that they are consistent and can withstand perceived failures. We show how cyber-physical systems' requirements can be modeled using the event calculus (EC), a formalism used in AI for representing actions and change. We also show how answer set programming (ASP) and its query-driven implementation s(CASP) can be used to directly realize the event calculus model of the requirements. This event calculus model can be used to automatically validate the requirements. Since ASP is an expressive knowledge representation language, it can also be used to represent contextual knowledge about cyber-physical systems, which, in turn, can be used to find gaps in their requirements specifications. We illustrate our approach through an altitude alerting system from the avionics domain. △ Less

Submitted 9 September, 2021; originally announced September 2021.

Comments: In Proceedings HCVS 2021, arXiv:2109.03988

Journal ref: EPTCS 344, 2021, pp. 79-90

Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming

Authors: Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta

Abstract: Automated commonsense reasoning is essential for building human-like AI systems featuring, for example, explainable AI. Event Calculus (EC) is a family of formalisms that model commonsense reasoning with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in the treatment of the continuous change in dense domains (e.g., time and other physical quantities),… ▽ More Automated commonsense reasoning is essential for building human-like AI systems featuring, for example, explainable AI. Event Calculus (EC) is a family of formalisms that model commonsense reasoning with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in the treatment of the continuous change in dense domains (e.g., time and other physical quantities), constraints among variables, default negation, and the uniform application of different inference methods, among others. We propose the use of s(CASP), a query-driven, top-down execution model for Predicate Answer Set Programming with Constraints, to model and reason using EC. We show how EC scenarios can be naturally and directly encoded in s(CASP) and how it enables deductive and abductive reasoning tasks in domains featuring constraints involving both dense time and dense fluents. △ Less

Submitted 28 June, 2021; originally announced June 2021.

Comments: Under consideration in Theory and Practice of Logic Programming (TPLP)

Knowledge-driven Natural Language Understanding of English Text and its Applications

Authors: Kinjal Basu, Sarat Varanasi, Farhad Shakerin, Joaquin Arias, Gopal Gupta

Abstract: Understanding the meaning of a text is a fundamental challenge of natural language understanding (NLU) research. An ideal NLU system should process a language in a way that is not exclusive to a single task or a dataset. Keeping this in mind, we have introduced a novel knowledge driven semantic representation approach for English text. By leveraging the VerbNet lexicon, we are able to map syntax t… ▽ More Understanding the meaning of a text is a fundamental challenge of natural language understanding (NLU) research. An ideal NLU system should process a language in a way that is not exclusive to a single task or a dataset. Keeping this in mind, we have introduced a novel knowledge driven semantic representation approach for English text. By leveraging the VerbNet lexicon, we are able to map syntax tree of the text to its commonsense meaning represented using basic knowledge primitives. The general purpose knowledge represented from our approach can be used to build any reasoning based NLU system that can also provide justification. We applied this approach to construct two NLU applications that we present here: SQuARE (Semantic-based Question Answering and Reasoning Engine) and StaCACK (Stateful Conversational Agent using Commonsense Knowledge). Both these systems work by "truly understanding" the natural language text they process and both provide natural language explanations for their responses while maintaining high accuracy. △ Less

Submitted 27 January, 2021; originally announced January 2021.

Comments: Preprint. Accepted by the 35th AAAI Conference (AAAI-21) Main Tracks

Minimal Schedule with Minimal Number of Agents in Attack-Defence Trees

Authors: Jaime Arias, Łukasz Maśko, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk

Abstract: Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that syn… ▽ More Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using minimal number of agents for a given attack-defence tree. △ Less

Submitted 29 April, 2022; v1 submitted 17 January, 2021; originally announced January 2021.

A Theoretical Study of (Full) Tabled Constraint Logic Programming

Authors: Joaquín Arias, Manuel Carro

Abstract: Logic programming with tabling and constraints (TCLP, tabled constraint logic programming) has been shown to be more expressive and, in some cases, more efficient than LP, CLP, or LP with tabling. In this paper we provide insights regarding the semantics, correctness, completeness, and termination of top-down execution strategies for full TCLP, i.e., TCLP featuring entailment checking in the calls… ▽ More Logic programming with tabling and constraints (TCLP, tabled constraint logic programming) has been shown to be more expressive and, in some cases, more efficient than LP, CLP, or LP with tabling. In this paper we provide insights regarding the semantics, correctness, completeness, and termination of top-down execution strategies for full TCLP, i.e., TCLP featuring entailment checking in the calls and in the answers. We present a top-down semantics for TCLP and show that it is equivalent to a fixpoint semantics. We study how the constraints that a program generates can effectively impact termination, even for constraint classes that are not constraint compact, generalizing previous results. We also present how different variants of constraint projection impact the correctness and completeness of TCLP implementations. All of the presented characteristics are implemented (or can be experimented with) in Mod TCLP, a modular framework for Tabled Constraint Logic Programming, part of the Ciao Prolog logic programming system. △ Less

Submitted 28 September, 2020; originally announced September 2020.

Comments: arXiv admin note: text overlap with arXiv:1809.05771

Justifications for Goal-Directed Constraint Answer Set Programming

Authors: Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta

Abstract: Ethical and legal concerns make it necessary for programs that may directly influence the life of people (via, e.g., legal or health counseling) to justify in human-understandable terms the advice given. Answer Set Programming has a rich semantics that makes it possible to very concisely express complex knowledge. However, justifying why an answer is a consequence from an ASP program may be non-tr… ▽ More Ethical and legal concerns make it necessary for programs that may directly influence the life of people (via, e.g., legal or health counseling) to justify in human-understandable terms the advice given. Answer Set Programming has a rich semantics that makes it possible to very concisely express complex knowledge. However, justifying why an answer is a consequence from an ASP program may be non-trivial -- even more so when the user is an expert in a given domain, but not necessarily knowledgeable in ASP. Most ASP systems generate answers using SAT-solving procedures on ground rules that do not match how humans perceive reasoning. We propose using s(CASP), a query-driven, top-down execution model for predicate ASP with constraints to generate justification trees of (constrained) answer sets. The operational semantics of s(CASP) relies on backward chaining, which is intuitive to follow and lends itself to generating explanations that are easier to translate into natural language. We show how s(CASP) provides minimal justifications for, among others, relevant examples proposed in the literature, both as search trees but, more importantly, as explanations in natural language. We validate our design with real ASP applications and evaluate the cost of generating s(CASP) justification trees. △ Less

Submitted 21 September, 2020; originally announced September 2020.

Comments: In Proceedings ICLP 2020, arXiv:2009.09158

Journal ref: EPTCS 325, 2020, pp. 59-72

The Making of 5G: Building an End-to-End 5G-Enabled System

Authors: Idelkys Quintana-Ramirez, Anthony Tsiopoulos, Maria A Lema, Fragkiskos Sardis, Luis Sequeira, James Arias, Aravindh Raman, Ali Azam, Mischa Dohler

Abstract: This article documents one of the world's first standards-compliant pre-commercial end-to-end 5th generation (5G) systems. Focus is on a standardized 5G architecture which includes the underlying 3GPP components but also the ETSI Network Function Virtualization (NFV) management and orchestration capabilities. The truly innovative character of 5G enabling fundamental changes to architecture and imp… ▽ More This article documents one of the world's first standards-compliant pre-commercial end-to-end 5th generation (5G) systems. Focus is on a standardized 5G architecture which includes the underlying 3GPP components but also the ETSI Network Function Virtualization (NFV) management and orchestration capabilities. The truly innovative character of 5G enabling fundamental changes to architecture and implementation is discussed, and details of monitoring and orchestration approaches that are deemed instrumental in unlocking the full potential of 5G. Finally, it is important to us to share the lessons learned which we hope are of use to industry and academia alike when building, deploying and testing emerging 5G systems. △ Less

Submitted 30 July, 2020; originally announced July 2020.

Journal ref: IEEE Communications Standards Magazine. Vol. 2, Issue 4, pp. 88-96, Dec. 2018

Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP

Authors: Joaquin Arias, Manuel Carro

Abstract: CiaoPP is an analyzer and optimizer for logic programs, part of the Ciao Prolog system. It includes PLAI, a fixpoint algorithm for the abstract interpretation of logic programs which we adapt to use tabled constraint logic programming. In this adaptation, the tabling engine drives the fixpoint computation, while the constraint solver handles the LUB of the abstract substitutions of different claus… ▽ More CiaoPP is an analyzer and optimizer for logic programs, part of the Ciao Prolog system. It includes PLAI, a fixpoint algorithm for the abstract interpretation of logic programs which we adapt to use tabled constraint logic programming. In this adaptation, the tabling engine drives the fixpoint computation, while the constraint solver handles the LUB of the abstract substitutions of different clauses. That simplifies the code and improves performance, since termination, dependencies, and some crucial operations (e.g., branch switching and resumption) are directly handled by the tabling engine. Determining whether the fixpoint has been reached uses semantic equivalence, which can decide that two syntactically different abstract substitutions represent the same element in the abstract domain. Therefore, the tabling analyzer can reuse answers in more cases than an analyzer using syntactical equality. This helps achieve better performance, even taking into account the additional cost associated to these checks. Our implementation is based on the TCLP framework available in Ciao Prolog and is one-third the size of the initial fixpoint implementation in CiaoPP. Its performance has been evaluated by analyzing several programs using different abstract domains. This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP). △ Less

Submitted 31 July, 2019; originally announced August 2019.

Comments: Paper presented at the 35th International Conference on Logic Programming (ICLP 2019), Las Cruces, New Mexico, USA, 20-25 September 2019, 16 pages

Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-Agent Systems

Authors: Jaime Arias, Carlos E. Budde, Wojciech Penczek, Laure Petrucci, Mariëlle Stoelinga

Abstract: Attack-Defence Trees (ADTs) are well-suited to assess possible attacks to systems and the efficiency of counter-measures. In this paper, we first enrich the available constructs with reactive patterns that cover further security scenarios, and equip all constructs with attributes such as time and cost to allow quantitative analyses. Then, ADTs are modelled as (an extension of) Asynchronous Multi-A… ▽ More Attack-Defence Trees (ADTs) are well-suited to assess possible attacks to systems and the efficiency of counter-measures. In this paper, we first enrich the available constructs with reactive patterns that cover further security scenarios, and equip all constructs with attributes such as time and cost to allow quantitative analyses. Then, ADTs are modelled as (an extension of) Asynchronous Multi-Agents Systems--EAMAS. The ADT-EAMAS transformation is performed in a systematic manner that ensures correctness. The transformation allows us to quantify the impact of different agents configurations on metrics such as attack time. Using EAMAS also permits parametric verification: we derive constraints for property satisfaction. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools. △ Less

Submitted 12 June, 2019; originally announced June 2019.

Comments: This work was partially funded by the NWO project SEQUOIA (grant 15474), EU project SUCCESS (102112) and the PHC van Gogh PAMPAS. The work of Arias and Petrucci has been supported by the BQR project AMoJAS

Description, Implementation, and Evaluation of a Generic Design for Tabled CLP

Authors: Joaquín Arias, Manuel Carro

Abstract: Logic programming with tabling and constraints (TCLP, tabled constraint logic programming) has been shown to be more expressive and in some cases more efficient than LP, CLP or LP + tabling. Previous designs of TCLP systems did not fully use entailment to determine call / answer subsumption and did not provide a simple and well-documented interface to facilitate the integration of constraint solve… ▽ More Logic programming with tabling and constraints (TCLP, tabled constraint logic programming) has been shown to be more expressive and in some cases more efficient than LP, CLP or LP + tabling. Previous designs of TCLP systems did not fully use entailment to determine call / answer subsumption and did not provide a simple and well-documented interface to facilitate the integration of constraint solvers in existing tabling systems. We study the role of projection and entailment in the termination, soundness and completeness of TCLP systems, and present the design and an experimental evaluation of Mod TCLP, a framework that eases the integration of additional constraint solvers. Mod TCLP views constraint solvers as clients of the tabling system, which is generic w.r.t. the solver and only requires a clear interface from the latter. We validate our design by integrating four constraint solvers: a previously existing constraint solver for difference constraints, written in C; the standard versions of Holzbaur's CLP(Q) and CLP(R), written in Prolog; and a new constraint solver for equations over finite lattices. We evaluate the performance of our framework in several benchmarks using the aforementioned constraint solvers. Mod TCLP is developed in Ciao Prolog, a robust, mature, next-generation Prolog system. Under consideration in Theory and Practice of Logic Programming (TPLP). △ Less

Submitted 15 September, 2018; originally announced September 2018.

Comments: Under consideration in Theory and Practice of Logic Programming (TPLP)

Constraint Answer Set Programming without Grounding

Authors: Joaquín Arias, Manuel Carro, Elmer Salazar, Kyle Marple, Gopal Gupta

Abstract: Extending ASP with constraints (CASP) enhances its expressiveness and performance. This extension is not straightforward as the grounding phase, present in most ASP systems, removes variables and the links among them, and also causes a combinatorial explosion in the size of the program. Several methods to overcome this issue have been devised: restricting the constraint domains (e.g., discrete ins… ▽ More Extending ASP with constraints (CASP) enhances its expressiveness and performance. This extension is not straightforward as the grounding phase, present in most ASP systems, removes variables and the links among them, and also causes a combinatorial explosion in the size of the program. Several methods to overcome this issue have been devised: restricting the constraint domains (e.g., discrete instead of dense), or the type (or number) of models that can be returned. In this paper we propose to incorporate constraints into s(ASP), a goal-directed, top-down execution model which implements ASP while retaining logical variables both during execution and in the answer sets. The resulting model, s(CASP), can constrain variables that, as in CLP, are kept during the execution and in the answer sets. s(CASP) inherits and generalizes the execution model of s(ASP) and is parametric w.r.t. the constraint solver. We describe this novel execution model and show through several examples the enhanced expressiveness of s(CASP) w.r.t. ASP, CLP, and other CASP systems. We also report improved performance w.r.t. other very mature, highly optimized ASP systems in some benchmarks. This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP). △ Less

Submitted 31 May, 2018; v1 submitted 30 April, 2018; originally announced April 2018.

Comments: Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018 18 pages, LaTeX

Certified Graph View Maintenance with Regular Datalog

Authors: Angela Bonifati, Stefania Dumbrava, Emilio Jesus Gallego Arias

Abstract: We employ the Coq proof assistant to develop a mechanically-certified framework for evaluating graph queries and incrementally maintaining materialized graph instances, also called views. The language we use for defining queries and views is Regular Datalog (RD) -- a notable fragment of non-recursive Datalog that can express complex navigational queries, with transitive closure as native operator.… ▽ More We employ the Coq proof assistant to develop a mechanically-certified framework for evaluating graph queries and incrementally maintaining materialized graph instances, also called views. The language we use for defining queries and views is Regular Datalog (RD) -- a notable fragment of non-recursive Datalog that can express complex navigational queries, with transitive closure as native operator. We first design and encode the theory of RD and then mechanize a RD-specific evaluation algorithm capable of fine-grained, incremental graph view computation, which we prove sound with respect to the declarative RD semantics. By using the Coq extraction mechanism, we test an Ocaml version of the verified engine on a set of preliminary benchmarks. Our development is particularly focused on leveraging existing verification and notational techniques to: a) define mechanized properties that can be easily understood by logicians and database researchers and b) attain formal verification with limited effort. Our work is the first step towards a unified, machine-verified, formal framework for dynamic graph query languages and their evaluation engines. This paper is under consideration for acceptance in TPLP. △ Less

Submitted 27 April, 2018; originally announced April 2018.

Comments: Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018. 18 pages, LaTeX, (arXiv:YYMM.NNNNN)

jsCoq: Towards Hybrid Theorem Proving Interfaces

Authors: Emilio Jesús Gallego Arias, Benoît Pin, Pierre Jouvelot

Abstract: We describe jsCcoq, a new platform and user environment for the Coq interactive proof assistant. The jsCoq system targets the HTML5-ECMAScript 2015 specification, and it is typically run inside a standards-compliant browser, without the need of external servers or services. Targeting educational use, jsCoq allows the user to start interaction with proof scripts right away, thanks to its self-conta… ▽ More We describe jsCcoq, a new platform and user environment for the Coq interactive proof assistant. The jsCoq system targets the HTML5-ECMAScript 2015 specification, and it is typically run inside a standards-compliant browser, without the need of external servers or services. Targeting educational use, jsCoq allows the user to start interaction with proof scripts right away, thanks to its self-contained nature. Indeed, a full Coq environment is packed along the proof scripts, easing distribution and installation. Starting to use jsCoq is as easy as clicking on a link. The current release ships more than 10 popular Coq libraries, and supports popular books such as Software Foundations or Certified Programming with Dependent Types. The new target platform has opened up new interaction and display possibilities. It has also fostered the development of some new Coq-related technology. In particular, we have implemented a new serialization-based protocol for interaction with the proof assistant, as well as a new package format for library distribution. △ Less

Submitted 24 January, 2017; originally announced January 2017.

Comments: In Proceedings UITP 2016, arXiv:1701.06745

Journal ref: EPTCS 239, 2017, pp. 15-27

Measuring Economic Resilience to Natural Disasters with Big Economic Transaction Data

Authors: Elena Alfaro Martinez, Maria Hernandez Rubio, Roberto Maestre Martinez, Juan Murillo Arias, Dario Patane, Amanda Zerbe, Robert Kirkpatrick, Miguel Luengo-Oroz, Amanda Zerbe

Abstract: This research explores the potential to analyze bank card payments and ATM cash withdrawals in order to map and quantify how people are impacted by and recover from natural disasters. Our approach defines a disaster-affected community's economic recovery time as the time needed to return to baseline activity levels in terms of number of bank card payments and ATM cash withdrawals. For Hurricane Od… ▽ More This research explores the potential to analyze bank card payments and ATM cash withdrawals in order to map and quantify how people are impacted by and recover from natural disasters. Our approach defines a disaster-affected community's economic recovery time as the time needed to return to baseline activity levels in terms of number of bank card payments and ATM cash withdrawals. For Hurricane Odile, which hit the state of Baja California Sur (BCS) in Mexico between 15 and 17 September 2014, we measured and mapped communities' economic recovery time, which ranged from 2 to 40 days in different locations. We found that -- among individuals with a bank account -- the lower the income level, the shorter the time needed for economic activity to return to normal levels. Gender differences in recovery times were also detected and quantified. In addition, our approach evaluated how communities prepared for the disaster by quantifying expenditure growth in food or gasoline before the hurricane struck. We believe this approach opens a new frontier in measuring the economic impact of disasters with high temporal and spatial resolution, and in understanding how populations bounce back and adapt. △ Less

Submitted 27 September, 2016; originally announced September 2016.

Comments: Presented at the Data For Good Exchange 2016

Differentially Private Bayesian Programming

Authors: Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesùs Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub

Abstract: We present PrivInfer, an expressive framework for writing and verifying differentially private Bayesian machine learning algorithms. Programs in PrivInfer are written in a rich functional probabilistic programming language with constructs for performing Bayesian inference. Then, differential privacy of programs is established using a relational refinement type system, in which refinements on proba… ▽ More We present PrivInfer, an expressive framework for writing and verifying differentially private Bayesian machine learning algorithms. Programs in PrivInfer are written in a rich functional probabilistic programming language with constructs for performing Bayesian inference. Then, differential privacy of programs is established using a relational refinement type system, in which refinements on probability types are indexed by a metric on distributions. Our framework leverages recent developments in Bayesian inference, probabilistic programming languages, and in relational refinement types. We demonstrate the expressiveness of PrivInfer by verifying privacy for several examples of private Bayesian inference. △ Less

Submitted 17 August, 2016; v1 submitted 1 May, 2016; originally announced May 2016.

Crowdsourcing the Robin Hood effect in cities

Authors: Thomas Louail, Maxime Lenormand, Juan Murillo Arias, José J. Ramasco

Abstract: Socioeconomic inequalities in cities are embedded in space and result in neighborhood effects, whose harmful consequences have proved very hard to counterbalance efficiently by planning policies alone. Considering redistribution of money flows as a first step toward improved spatial equity, we study a bottom-up approach that would rely on a slight evolution of shopping mobility practices. Building… ▽ More Socioeconomic inequalities in cities are embedded in space and result in neighborhood effects, whose harmful consequences have proved very hard to counterbalance efficiently by planning policies alone. Considering redistribution of money flows as a first step toward improved spatial equity, we study a bottom-up approach that would rely on a slight evolution of shopping mobility practices. Building on a database of anonymized credit card transactions in Madrid and Barcelona, we quantify the mobility effort required to reach a reference situation where commercial income is evenly shared among neighborhoods. The redirections of shopping trips preserve key properties of human mobility, including travel distances. Surprisingly, for both cities only a small fraction ($\sim 5 \%$) of trips need to be altered to reach equity situations, improving even other sustainability indicators. The method could be implemented in mobile applications that would assist individuals in reshaping their shopping practices, to promote the spatial redistribution of opportunities in the city. △ Less

Submitted 9 June, 2017; v1 submitted 28 April, 2016; originally announced April 2016.

Comments: 9 pages, 4 figures + Appendix

Journal ref: Applied Network Science 2, 11 (2017)

Predicting Regional Economic Indices using Big Data of Individual Bank Card Transactions

Authors: Stanislav Sobolevsky, Emanuele Massaro, Iva Bojic, Juan Murillo Arias, Carlo Ratti

Abstract: For centuries quality of life was a subject of studies across different disciplines. However, only with the emergence of a digital era, it became possible to investigate this topic on a larger scale. Over time it became clear that quality of life not only depends on one, but on three relatively different parameters: social, economic and well-being measures. In this study we focus only on the first… ▽ More For centuries quality of life was a subject of studies across different disciplines. However, only with the emergence of a digital era, it became possible to investigate this topic on a larger scale. Over time it became clear that quality of life not only depends on one, but on three relatively different parameters: social, economic and well-being measures. In this study we focus only on the first two, since the last one is often very subjective and consequently hard to measure. Using a complete set of bank card transactions recorded by Banco Bilbao Vizcaya Argentaria (BBVA) during 2011 in Spain, we first create a feature space by defining various meaningful characteristics of a particular area performance through activity of its businesses, residents and visitors. We then evaluate those quantities by considering available official statistics for Spanish provinces (e.g., housing prices, unemployment rate, life expectancy) and investigate whether they can be predicted based on our feature space. For the purpose of prediction, our study proposes a supervised machine learning approach. Our finding is that there is a clear correlation between individual spending behavior and official socioeconomic indexes denoting quality of life. Moreover, we believe that this modus operandi is useful to understand, predict and analyze the impact of human activity on the wellness of our society on scales for which there is no consistent official statistics available (e.g., cities and towns, districts or smaller neighborhoods). △ Less

Submitted 11 July, 2015; v1 submitted 29 May, 2015; originally announced June 2015.

Comments: 12 pages, 6 figures

MSC Class: 91D30

Cities through the Prism of People's Spending Behavior

Authors: Stanislav Sobolevsky, Izabela Sitko, Remi Tachet des Combes, Bartosz Hawelka, Juan Murillo Arias, Carlo Ratti

Abstract: Scientific studies of society increasingly rely on digital traces produced by various aspects of human activity. In this paper, we use a relatively unexplored source of data, anonymized records of bank card transactions collected in Spain by a big European bank, in order to propose a new classification scheme of cities based on the economic behavior of their residents. First, we study how individu… ▽ More Scientific studies of society increasingly rely on digital traces produced by various aspects of human activity. In this paper, we use a relatively unexplored source of data, anonymized records of bank card transactions collected in Spain by a big European bank, in order to propose a new classification scheme of cities based on the economic behavior of their residents. First, we study how individual spending behavior is qualitatively and quantitatively affected by various factors such as customer's age, gender, and size of a home city. We show that, similar to other socioeconomic urban quantities, individual spending activity exhibits a statistically significant superlinear scaling with city size. With respect to the general trends, we quantify the distinctive signature of each city in terms of residents' spending behavior, independently from the effects of scale and demographic heterogeneity. Based on the comparison of city signatures, we build a novel classification of cities across Spain in three categories. That classification is, with few exceptions, stable over different ways of city definition and connects with a meaningful socioeconomic interpretation. Furthermore, it appears to be related with the ability of cities to attract foreign visitors, which is a particularly remarkable finding given that the classification was based exclusively on the behavioral patterns of city residents. This highlights the far-reaching applicability of the presented classification approach and its ability to discover patterns that go beyond the quantities directly involved in it. △ Less

Submitted 14 May, 2015; originally announced May 2015.

Scaling of city attractiveness for foreign visitors through big data of human economical and social media activity

Authors: Stanislav Sobolevsky, Iva Bojic, Alexander Belyi, Izabela Sitko, Bartosz Hawelka, Juan Murillo Arias, Carlo Ratti

Abstract: Scientific studies investigating laws and regularities of human behavior are nowadays increasingly relying on the wealth of widely available digital information produced by human social activity. In this paper we leverage big data created by three different aspects of human activity (i.e., bank card transactions, geotagged photographs and tweets) in Spain for quantifying city attractiveness for th… ▽ More Scientific studies investigating laws and regularities of human behavior are nowadays increasingly relying on the wealth of widely available digital information produced by human social activity. In this paper we leverage big data created by three different aspects of human activity (i.e., bank card transactions, geotagged photographs and tweets) in Spain for quantifying city attractiveness for the foreign visitors. An important finding of this papers is a strong superlinear scaling of city attractiveness with its population size. The observed scaling exponent stays nearly the same for different ways of defining cities and for different data sources, emphasizing the robustness of our finding. Temporal variation of the scaling exponent is also considered in order to reveal seasonal patterns in the attractiveness △ Less

Submitted 22 April, 2015; originally announced April 2015.

Comments: 8 pages, 3 figures, 1 table

MSC Class: 91D30

Really Natural Linear Indexed Type Checking

Authors: Arthur Azevedo de Amorim, Emilio Jesús Gallego Arias, Marco Gaboardi, Justin Hsu

Abstract: Recent works have shown the power of linear indexed type systems for enforcing complex program properties. These systems combine linear types with a language of type-level indices, allowing more fine-grained analyses. Such systems have been fruitfully applied in diverse domains, including implicit complexity and differential privacy. A natural way to enhance the expressiveness of this approach is… ▽ More Recent works have shown the power of linear indexed type systems for enforcing complex program properties. These systems combine linear types with a language of type-level indices, allowing more fine-grained analyses. Such systems have been fruitfully applied in diverse domains, including implicit complexity and differential privacy. A natural way to enhance the expressiveness of this approach is by allowing the indices to depend on runtime information, in the spirit of dependent types. This approach is used in DFuzz, a language for differential privacy. The DFuzz type system relies on an index language supporting real and natural number arithmetic over constants and variables. Moreover, DFuzz uses a subtyping mechanism to make types more flexible. By themselves, linearity, dependency, and subtyping each require delicate handling when performing type checking or type inference; their combination increases this challenge substantially, as the features can interact in non-trivial ways. In this paper, we study the type-checking problem for DFuzz. We show how we can reduce type checking for (a simple extension of) DFuzz to constraint solving over a first-order theory of naturals and real numbers which, although undecidable, can often be handled in practice by standard numeric solvers. △ Less

Submitted 16 March, 2015; originally announced March 2015.

Computer-aided verification in mechanism design

Authors: Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub

Abstract: In mechanism design, the gold standard solution concepts are dominant strategy incentive compatibility and Bayesian incentive compatibility. These solution concepts relieve the (possibly unsophisticated) bidders from the need to engage in complicated strategizing. While incentive properties are simple to state, their proofs are specific to the mechanism and can be quite complex. This raises two co… ▽ More In mechanism design, the gold standard solution concepts are dominant strategy incentive compatibility and Bayesian incentive compatibility. These solution concepts relieve the (possibly unsophisticated) bidders from the need to engage in complicated strategizing. While incentive properties are simple to state, their proofs are specific to the mechanism and can be quite complex. This raises two concerns. From a practical perspective, checking a complex proof can be a tedious process, often requiring experts knowledgeable in mechanism design. Furthermore, from a modeling perspective, if unsophisticated agents are unconvinced of incentive properties, they may strategize in unpredictable ways. To address both concerns, we explore techniques from computer-aided verification to construct formal proofs of incentive properties. Because formal proofs can be automatically checked, agents do not need to manually check the properties, or even understand the proof. To demonstrate, we present the verification of a sophisticated mechanism: the generic reduction from Bayesian incentive compatible mechanism design to algorithm design given by Hartline, Kleinberg, and Malekian. This mechanism presents new challenges for formal verification, including essential use of randomness from both the execution of the mechanism and from the prior type distributions. As an immediate consequence, our work also formalizes Bayesian incentive compatibility for the entire family of mechanisms derived via this reduction. Finally, as an intermediate step in our formalization, we provide the first formal verification of incentive compatibility for the celebrated Vickrey-Clarke-Groves mechanism. △ Less

Submitted 24 December, 2016; v1 submitted 13 February, 2015; originally announced February 2015.

Influence of sociodemographic characteristics on human mobility

Authors: Maxime Lenormand, Thomas Louail, Oliva G. Cantu-Ros, Miguel Picornell, Ricardo Herranz, Juan Murillo Arias, Marc Barthelemy, Maxi San Miguel, Jose J. Ramasco

Abstract: Human mobility has been traditionally studied using surveys that deliver snapshots of population displacement patterns. The growing accessibility to ICT information from portable digital media has recently opened the possibility of exploring human behavior at high spatio-temporal resolutions. Mobile phone records, geolocated tweets, check-ins from Foursquare or geotagged photos, have contributed t… ▽ More Human mobility has been traditionally studied using surveys that deliver snapshots of population displacement patterns. The growing accessibility to ICT information from portable digital media has recently opened the possibility of exploring human behavior at high spatio-temporal resolutions. Mobile phone records, geolocated tweets, check-ins from Foursquare or geotagged photos, have contributed to this purpose at different scales, from cities to countries, in different world areas. Many previous works lacked, however, details on the individuals' attributes such as age or gender. In this work, we analyze credit-card records from Barcelona and Madrid and by examining the geolocated credit-card transactions of individuals living in the two provinces, we find that the mobility patterns vary according to gender, age and occupation. Differences in distance traveled and travel purpose are observed between younger and older people, but, curiously, either between males and females of similar age. While mobility displays some generic features, here we show that sociodemographic characteristics play a relevant role and must be taken into account for mobility and epidemiological modelization. △ Less

Submitted 25 May, 2015; v1 submitted 28 November, 2014; originally announced November 2014.

Comments: 13 pages, 11 figures + Supplementary information

Journal ref: Scientific Reports 5:10075 (2015)

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy

Authors: Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub

Abstract: Mechanism design is the study of algorithm design in which the inputs to the algorithm are controlled by strategic agents, who must be incentivized to faithfully report them. Unlike typical programmatic properties, it is not sufficient for algorithms to merely satisfy the property---incentive properties are only useful if the strategic agents also believe this fact. Verification is an attractive… ▽ More Mechanism design is the study of algorithm design in which the inputs to the algorithm are controlled by strategic agents, who must be incentivized to faithfully report them. Unlike typical programmatic properties, it is not sufficient for algorithms to merely satisfy the property---incentive properties are only useful if the strategic agents also believe this fact. Verification is an attractive way to convince agents that the incentive properties actually hold, but mechanism design poses several unique challenges: interesting properties can be sophisticated relational properties of probabilistic computations involving expected values, and mechanisms may rely on other probabilistic properties, like differential privacy, to achieve their goals. We introduce a relational refinement type system, called $\mathsf{HOARe}^2$, for verifying mechanism design and differential privacy. We show that $\mathsf{HOARe}^2$ is sound w.r.t. a denotational semantics, and correctly models $(ε,δ)$-differential privacy; moreover, we show that it subsumes DFuzz, an existing linear dependent type system for differential privacy. Finally, we develop an SMT-based implementation of $\mathsf{HOARe}^2$ and use it to verify challenging examples of mechanism design, including auctions and aggregative games, and new proposed examples from differential privacy. △ Less

Submitted 29 October, 2014; v1 submitted 25 July, 2014; originally announced July 2014.

Proving differential privacy in Hoare logic

Authors: Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub

Abstract: Differential privacy is a rigorous, worst-case notion of privacy-preserving computation. Informally, a probabilistic program is differentially private if the participation of a single individual in the input database has a limited effect on the program's distribution on outputs. More technically, differential privacy is a quantitative 2-safety property that bounds the distance between the output d… ▽ More Differential privacy is a rigorous, worst-case notion of privacy-preserving computation. Informally, a probabilistic program is differentially private if the participation of a single individual in the input database has a limited effect on the program's distribution on outputs. More technically, differential privacy is a quantitative 2-safety property that bounds the distance between the output distributions of a probabilistic program on adjacent inputs. Like many 2-safety properties, differential privacy lies outside the scope of traditional verification techniques. Existing approaches to enforce privacy are based on intricate, non-conventional type systems, or customized relational logics. These approaches are difficult to implement and often cumbersome to use. We present an alternative approach that verifies differential privacy by standard, non-relational reasoning on non-probabilistic programs. Our approach transforms a probabilistic program into a non-probabilistic program which simulates two executions of the original program. We prove that if the target program is correct with respect to a Hoare specification, then the original probabilistic program is differentially private. We provide a variety of examples from the differential privacy literature to demonstrate the utility of our approach. Finally, we compare our approach with existing verification techniques for privacy. △ Less

Submitted 10 July, 2014; originally announced July 2014.

Comments: Published at the Computer Security Foundations Symposium (CSF), 2014

Mining Urban Performance: Scale-Independent Classification of Cities Based on Individual Economic Transactions

Authors: Stanislav Sobolevsky, Izabela Sitko, Sebastian Grauwin, Remi Tachet des Combes, Bartosz Hawelka, Juan Murillo Arias, Carlo Ratti

Abstract: Intensive development of urban systems creates a number of challenges for urban planners and policy makers in order to maintain sustainable growth. Running efficient urban policies requires meaningful urban metrics, which could quantify important urban characteristics including various aspects of an actual human behavior. Since a city size is known to have a major, yet often nonlinear, impact on t… ▽ More Intensive development of urban systems creates a number of challenges for urban planners and policy makers in order to maintain sustainable growth. Running efficient urban policies requires meaningful urban metrics, which could quantify important urban characteristics including various aspects of an actual human behavior. Since a city size is known to have a major, yet often nonlinear, impact on the human activity, it also becomes important to develop scale-free metrics that capture qualitative city properties, beyond the effects of scale. Recent availability of extensive datasets created by human activity involving digital technologies creates new opportunities in this area. In this paper we propose a novel approach of city scoring and classification based on quantitative scale-free metrics related to economic activity of city residents, as well as domestic and foreign visitors. It is demonstrated on the example of Spain, but the proposed methodology is of a general character. We employ a new source of large-scale ubiquitous data, which consists of anonymized countrywide records of bank card transactions collected by one of the largest Spanish banks. Different aspects of the classification reveal important properties of Spanish cities, which significantly complement the pattern that might be discovered with the official socioeconomic statistics. △ Less

Submitted 16 May, 2014; originally announced May 2014.

Comments: 10 pages, 7 figures, to be published in the proceedings of ASE BigDataScience 2014 conference

MSC Class: 62-07; 68U01 ACM Class: H.2.8; J.4

Dual Query: Practical Private Query Release for High Dimensional Data

Authors: Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Zhiwei Steven Wu

Abstract: We present a practical, differentially private algorithm for answering a large number of queries on high dimensional datasets. Like all algorithms for this task, ours necessarily has worst-case complexity exponential in the dimension of the data. However, our algorithm packages the computationally hard step into a concisely defined integer program, which can be solved non-privately using standard… ▽ More We present a practical, differentially private algorithm for answering a large number of queries on high dimensional datasets. Like all algorithms for this task, ours necessarily has worst-case complexity exponential in the dimension of the data. However, our algorithm packages the computationally hard step into a concisely defined integer program, which can be solved non-privately using standard solvers. We prove accuracy and privacy theorems for our algorithm, and then demonstrate experimentally that our algorithm performs well in practice. For example, our algorithm can efficiently and accurately answer millions of queries on the Netflix dataset, which has over 17,000 attributes; this is an improvement on the state of the art by multiple orders of magnitude. △ Less

Submitted 18 November, 2015; v1 submitted 6 February, 2014; originally announced February 2014.

Journal ref: Journal of Privacy and Confidentiality 7(2) 53--77 (2017)

The Ciao clp(FD) Library. A Modular CLP Extension for Prolog

Authors: Emilio Jesús Gallego Arias, Rémy Haemmerlé, Manuel V. Hermenegildo, José F. Morales

Abstract: We present a new free library for Constraint Logic Programming over Finite Domains, included with the Ciao Prolog system. The library is entirely written in Prolog, leveraging on Ciao's module system and code transformation capabilities in order to achieve a highly modular design without compromising performance. We describe the interface, implementation, and design rationale of each modular compo… ▽ More We present a new free library for Constraint Logic Programming over Finite Domains, included with the Ciao Prolog system. The library is entirely written in Prolog, leveraging on Ciao's module system and code transformation capabilities in order to achieve a highly modular design without compromising performance. We describe the interface, implementation, and design rationale of each modular component. The library meets several design goals: a high level of modularity, allowing the individual components to be replaced by different versions; high-efficiency, being competitive with other FD implementations; a glass-box approach, so the user can specify new constraints at different levels; and a Prolog implementation, in order to ease the integration with Ciao's code analysis components. The core is built upon two small libraries which implement integer ranges and closures. On top of that, a finite domain variable datatype is defined, taking care of constraint reexecution depending on range changes. These three libraries form what we call the FD kernel of the library. This FD kernel is used in turn to implement several higher-level finite domain constraints, specified using indexicals. Together with a labeling module this layer forms what we name \emph{the FD solver}. A final level integrates the clp(FD) paradigm with our FD solver. This is achieved using attributed variables and a compiler from the clp(FD) language to the set of constraints provided by the solver. It should be noted that the user of the library is encouraged to work in any of those levels as seen convenient: from writing a new range module to enriching the set of FD constraints by writing new indexicals. △ Less

Submitted 31 January, 2013; originally announced January 2013.

Comments: Appeared in CICLOPS 2012. 15 Pages, 5 Figures