检索结果-内蒙古大学图书馆

Extended High Utility Pattern Mining: An Answer Set programming Based Framework and Applications

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Cauteruccio, Francesco Terracina, Giorgio DII Polytechnic University of Marche Ancona Italy DEMACS University of Calabria Rende Italy

Detecting sets of relevant patterns from a given dataset is an important challenge in data mining. The relevance of a pattern, also called utility in the literature, is a subjective measure and can be actually assessed from very different points of view. Rule-based languages like Answer Set programming (ASP) seem well suited for specifying user-provided criteria to assess pattern utility in a form of constraints;moreover, declarativity of ASP allows for a very easy switch between several criteria in order to analyze the dataset from different points of view. In this paper, we make steps toward extending the notion of High Utility Pattern Mining (HUPM);in particular we introduce a new framework that allows for new classes of utility criteria not considered in the previous literature. We also show how recent extensions of ASP with external functions can support a fast and effective encoding and testing of the new framework. To demonstrate the potential of the proposed framework, we exploit it as a building block for the definition of an innovative method for predicting ICU admission for COVID-19 patients. Finally, an extensive experimental activity demonstrates both from a quantitative and a qualitative point of view the effectiveness of the proposed approach. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2023, The Authors. All rights reserved.

关键词： logic programming

Epistemic logic Programs: A study of some properties

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Costantini, Stefania Formisano, Andrea DISIM Università dell'Aquila via Vetoio L'Aquila Italy Gruppo Nazionale per il Calcolo Scientifico - INdAM Roma Italy DMIF Università di Udine via delle Scienze 206 Udine Italy

Epistemic logic Programs (ELPs), extend Answer Set programming (ASP) with epistemic operators. The semantics of such programs is provided in terms of world views, which are sets of belief sets, i.e., syntactically, sets of sets of atoms. Different semantic approaches propose different characterizations of world views. Recent work has introduced semantic properties that should be met by any semantics for ELPs, like the Epistemic Splitting Property, that, if satisfied, allows to modularly compute world views in a bottom-up fashion, analogously to "traditional" ASP. We analyze the possibility of changing the perspective, shifting from a bottom-up to a top-down approach to splitting. We propose a basic top-down approach, which we prove to be equivalent to the bottom-up one. We then propose an extended approach, where our new definition: (i) is provably applicable to many of the existing semantics;(ii) operates similarly to "traditional" ASP;(iii) provably coincides under any semantics with the bottom-up notion of splitting at least on the class of Epistemically Stratified Programs (which are, intuitively, those where the use of epistemic operators is stratified);(iv) better adheres to common ASP programming methodology. Under consideration in theory and practice of logic programming (TPLP). © 2023, CC BY.

关键词： Semantics

VeriFly: On-the-fly Assertion Checking via Incrementality

学校读者我要写书评

暂无评论

theory and practice of logic programming 2021年第6期21卷 768-784页

作者： Sanchez-Ordaz, Miguel A. Garcia-Contreras, Isabel Perez, Victor Morales, Jose F. Lopez-Garcia, Pedro Hermenegildo, Manuel V. IMDEA Software Inst Madrid Spain UPM Madrid Spain Spanish Council Sci Res CSIC Madrid Spain

Assertion checking is an invaluable programmer's tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers, this means being able to have relevant properties, such as modes, types, determinacy, nonfailure, sharing, constraints, and cost, checked and errors flagged without having to actually run the program. Such global static analysis tools are arguably most useful the earlier they are used in the software development cycle, and fast response times are essential for interactive use. Triggering a full and precise semantic analysis of a software project every time a change is made can be prohibitively expensive. This is specially the case when complex properties need to be inferred for large, realistic code bases. In our static analysis and verification framework, this challenge is addressed through a combination of modular and incremental (context- and path-sensitive) analysis that is responsive to program edits, at different levels of granularity. In this tool paper, we present how the combination of this framework within an integrated development environment (IDE) takes advantage of such incrementality to achieve a high level of reactivity when reflecting analysis and verification results back as colorings and tooltips directly on the program text - the tool's VeriFly mode. The concrete implementation that we describe is Emacs-based and reuses in part off-the- shelf "on-the-fly" syntax checking facilities (flycheck). We believe that similar extensions are also reproducible with low effort in other mature development environments. Our initial experience with the tool shows quite promising results, with low latency times that provide early, continuous, and precise assertion checking and other semantic feedback to programmers during the development process. The tool supports Prolog natively, as well as other languages by semantic transformation into Horn clauses.

关键词： On-the-fly assertion checking program development environments static analysis abstract interpretation incremental analysis logic and constraint programming

Explanation Generation for Multi-Modal Multi-Agent Path Finding with Optimal Resource Utilization using Answer Set programming

学校读者我要写书评

暂无评论

theory and practice of logic programming 2020年第6期20卷 974-989页

作者： BOGATARKAN, A. Y. S. U. ERDEM, E. S. R. A. Sabanci Univ Fac Engn & Nat Sci Istanbul Turkey

The multi-agent path finding (MAPF) problem is a combinatorial search problem that aims at finding paths for multiple agents (e.g., robots) in an environment (e.g., an autonomous warehouse) such that no two agents collide with each other, and subject to some constraints on the lengths of paths. We consider a general version of MAPF, called mMAPF, that involves multi-modal transportation modes (e.g., due to velocity constraints) and consumption of different types of resources (e.g., batteries). The real-world applications of mMAPF require flexibility (e.g., solving variations of mMAPF) as well as explainability. Our earlier studies on mMAPF have focused on the former challenge of flexibility. In this study, we focus on the latter challenge of explainability, and introduce a method for generating explanations for queries regarding the feasibility and optimality of solutions, the nonexistence of solutions, and the observations about solutions. Our method is based on answer set programming.

关键词： logic programming

Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Cristiá, Maximiliano Rossi, Gianfranco Universidad Nacional de Rosario CIFASIS Argentina Università di Parma Italy

This technical note shows how we have combined prescriptive type checking and constraint solving to increase automation during software verification. We do so by defining a type system and implementing a typechecker for {log} (read 'setlog'), a Constraint logic programming (CLP) language and satisfiability solver based on set theory. The constraint solver is proved to be safe w.r.t. the type system. Two industrial-strength case studies are presented where this combination is used with very good results. Under consideration in theory and practice of logic programming (TPLP). © 2022, CC BY.

关键词： Set theory

Exploiting Game theory for Analysing Justifications

学校读者我要写书评

暂无评论

theory and practice of logic programming 2020年第6期20卷 880-894页

作者： MARYNISSEN, S. I. M. O. N. BOGAERTS, B. A. R. T. DENECKER, M. A. R. C. Katholieke Univ Leuven Leuven Belgium Vrije Univ Brussel Brussels Belgium

Justification theory is a unifying semantic framework. While it has its roots in non-monotonic logics, it can be applied to various areas in computer science, especially in explainable reasoning;its most central concept is a justification: an explanation why a property holds (or does not hold) in a model. In this paper, we continue the study of justification theory by means of three major contributions. The first is studying the relation between justification theory and game theory. We show that justification frameworks can be seen as a special type of games. The established connection provides the theoretical foundations for our next two contributions. The second contribution is studying under which condition two different dialects of justification theory (graphs as explanations vs trees as explanations) coincide. The third contribution is establishing a precise criterion of when a semantics induced by justification theory yields consistent results. In the past proving that such semantics were consistent took cumbersome and elaborate proofs. We show that these criteria are indeed satisfied for all common semantics of logic programming.

关键词： justification theory positional games logic programming non-monotonic logic

A Multi-Objective Approach for Security Hardening and Probabilistic Vulnerability Assessment on Attack Graphs 46

学校读者我要写书评

暂无评论

A Multi-Objective Approach for Security Hardening and Probab...

46th Annual IEEE-Computer-Society International Computers, Software, and Applications Conference (COMPSAC) - Computers, Software, and Applications in an Uncertain World

作者： Bardhan, Shuvo Georgetown Univ Ctr Secur & Emerging Technol Washington DC 20057 USA

ISBN: (纸本)9781665488105

Assessing vulnerabilities of a network and mitigating them is a challenging task owing to the complexity and scale of the problem. Various probabilistic security metrics on attack graphs are presented in the literature to handle realistic attack scenarios involving large attack graphs. In our work, we propose a generalized path-enumeration based technique for computing attack probabilities on attack graphs that can handle repeated vulnerabilities as well as cyclic graphs. A multiplicative idempotency based approach is used for computation while aggregating the path probabilities. We employ the inclusion-exclusion principle to prove the soundness of our proposed technique. Also, in practice, we found that attackers retain experience and face reduced difficulty in exploiting a vulnerability in repeated attacks. In this paper, we extend the proposed probabilistic measure to incorporate such conditions leveraging possible decay functions. Our proposed metric is helpful in service management for network hardening. Network hardening is formulated as a multi-objective optimization problem that generates pareto-optimal solutions which trade off utility with vulnerability. Case studies are presented for complex attack graphs having interesting pareto-optimal solutions for service management.

关键词： Measurement Conferences Probabilistic logic Linear programming Software Complexity theory Security

Compositional verification in rewriting logic

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Martín, Óscar Verdejo, Alberto Martí-Oliet, Narciso Facultad de Informática Universidad Complutense de Madrid Madrid Spain

In previous work, summarized in this paper, we proposed an operation of parallel composition for rewriting-logic theories, allowing compositional specification of systems and reusability of components. The present paper focuses on compositional verification. We show how the assume/guarantee technique can be transposed to our setting, by giving appropriate definitions of satisfaction based on transition structures and path semantics. We also show that simulation and equational abstraction can be done componentwise. Appropriate concepts of fairness and deadlock for our composition operation are discussed, as they affect satisfaction of temporal formulas. We keep in parallel a distributed and a global view of composed systems. We show that these views are equivalent and interchangeable, which may help our intuition and also has practical uses as, for example, it allows global-style verification of a modularly specified system. Under consideration in theory and practice of logic programming (TPLP). © 2023, CC BY-NC-ND.

关键词： Reusability

Human Robot Collaborative Assembly Planning: An Answer Set programming Approach

学校读者我要写书评

暂无评论

theory and practice of logic programming 2020年第6期20卷 1006-1020页

作者： Rizwan, Momina Patoglu, Volkan Erdem, Esra Sabanci Univ Fac Engn & Nat Sci Istanbul Turkey

For planning an assembly of a product from a given set of parts, robots necessitate certain cognitive skills: high-level planning is needed to decide the order of actuation actions, while geometric reasoning is needed to check the feasibility of these actions. For collaborative assembly tasks with humans, robots require further cognitive capabilities, such as commonsense reasoning, sensing, and communication skills, not only to cope with the uncertainty caused by incomplete knowledge about the humans' behaviors but also to ensure safer collaborations. We propose a novel method for collaborative assembly planning under uncertainty, that utilizes hybrid conditional planning extended with commonsense reasoning and a rich set of communication actions for collaborative tasks. Our method is based on answer set programming. We show the applicability of our approach in a real-world assembly domain, where a bi-manual Baxter robot collaborates with a human teammate to assemble furniture.

关键词： Answer set programming cognitive robotics conditional planning assembly planning human-robot interaction hybrid reasoning robotic planning planning under uncertainty