1,721,011 research outputs found
Mining temporal networks: Results and open problems
Full text linkThe design of temporal networks typically follows a top-down approach where a designer handcrafts a temporal network to model some concrete plan of interest. Instead, the bottom-up approach of mining is the process of building a temporal network from a set of execution traces of some (typically unknown) underlying process. Recent research showed that, due to the structural properties of temporal networks, such a task can be done in polynomial time. In this paper, we give an overview of the current status of our research and highlight open problems concerning Formal Methods and Artificial Intelligence
Mining CSTNUDs significant for a set of traces is polynomial
No full textA Conditional Simple Temporal Network with Uncertainty and Decisions (CSTNUD) is a formalism for temporal plans that models controllable and uncontrollable durations as well as controllable and uncontrollable choices simultaneously. In the classic top-down model-based engineering approach, a designer builds CSTNUDs to model, validate and execute some temporal plans of interest. In this paper, we investigate a bottom-up approach by providing a deterministic polynomial time algorithm to mine a CSTNUD from a set of execution traces (i.e., a log). We provide a prototype implementation and we test it with a set of artificial data. Finally, we elaborate on consistency and controllability of mined networks
A tableau-based system for spatial reasoning about directional relations
No full textThe management of qualitative spatial information is an important research area in computer science and AI. Modal logic provides a natural framework for the formalization and implementation of qualitative spatial reasoning. Unfortunately, when directional relations are considered, modal logic systems for spatial reasoning usually turn out to be undecidable (often even not recursively enumerable). In this paper, we give a first example of a decidable modal logic for spatial reasoning with directional relations, called Weak Spatial Propositional Neighborhood Logic (WSpPNL for short). WSpPNL features two modalities, respectively an east modality and a north modality, to deal with non-empty rectangles over NxN. We first show the NEXPTIME-completeness of WSpPNL, then we develop an optimal tableau method for it
The light side of interval temporal logic: The Bernays-Schönfinkel fragment of CDT
No full textDecidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the recent years. Even though most interval logics turn out to be undecidable, meaningful exceptions exist, such as the logics of temporal neighborhood and (some of) the logics of the subinterval relation. In this paper, we explore a different path to decidability: instead of restricting the set of modalities or imposing severe semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema's CDT, and we suitably limit the negation depth of modalities. The decidability of the satisfiability problem for the resulting fragment, called CDT_BS, over the class of all linear orders, is proved by embedding it into a well-known decidable quantifier prefix class of first-order logic, namely, Bernays-Schönfinkel class. In addition, we show that CDT_BS is in fact NP-complete (Bernays-Schönfinkel class is NEXPTIME-complete), and we prove its expressive completeness with respect to a suitable fragment of Bernays-Schönfinkel class. Finally, we show that any increase in the negation depth of CDT_BS modalities immediately yields undecidability
A Tractable Formalism for Combining Rectangular Cardinal Relations with Metric Constraints
No full textKnowledge representation and reasoning in real-world applications often require to integrate multiple aspects of space. In this paper, we focus our attention on the so-called Rectangular Cardinal Direction calculus for qualitative spatial reasoning on cardinal relations between rectangles whose sides are aligned to the axes of the plane. We first show how to extend a tractable fragment of such a calculus with metric constraints preserving tractability. Then, we illustrate how the resulting formalism makes it possible to represent available knowledge on directional relations between rectangles and to derive additional information about them, as well as to deal with metric constraints on the height/width of a rectangle or on the vertical/horizontal distance between rectangles
A note on ultimately-periodic finite interval temporal logic model checking
No full textIn this paper, we deal with the ultimately-periodic finite interval temporal logic model checking problem. The problem has been shown to be in PTIME for full Halpern and Shoham's interval temporal logic (HS for short) over finite models, as well as for the HS fragment featuring a modality for Allen relation meets and metric constraints over non-sparse ultimately-periodic (finite) models, that is, over ultimately-periodic models whose representation is polynomial in their size. Here, we generalize the latter result to the case of sparse ultimately-periodic models
A model checker for interval temporal logic over finite structures?
No full textModel checking is the process of establishing whether a certain
formula is satisfied by a given structure, and it is usually associated
with point-based temporal logics. Recently, the question of how to correctly
define and study the model checking problem for interval-based
temporal logics has been raised. In this paper, we focus on a very natural
finite version of the model checking problem for Halpern and Shoham's
modal logic of time intervals, a.k.a. HS, for which an algorithm that behaves
in a very effcient way (under certain conditions) can be designed.
We present an implementation of such an algorithm and analyse its performance
through a systematic series of tests.Model checking is the process of establishing whether a certain formula is satis-ed by a given structure, and it is usually associated with point-based temporal logics. Recently, the question of how to correctly define and study the model checking problem for interval-based temporal logics has been raised. In this paper, we focus on a very natural finite version of the model checking problem for Halpern and Shoham's modal logic of time intervals, a.k.a. HS, for which an algorithm that behaves in a very eficient way (under certain conditions) can be designed. We present an implementation of such an algorithm and analyse its performance through a systematic series of tests
Three-objective constrained evolutionary instance selection for classification: Wrapper and filter approaches
No full textThe large amount of data that is produced today with new technologies is an impediment for machine learning algorithms to work correctly, both due to the memory requirements and the necessary execution times. That is why the processes of reducing both the quantity and the size of the data are increasingly important. One of these processes is the so-called instance selection. In this paper we propose three-objective constrained optimization models to formulate instance selection wrapper and filter methods (separately) for classification problems, which are solved with multi-objective evolutionary algorithms and multi-objective differential evolution. In the proposed instance selection wrapper method, an objective is added to the usual ones to minimize the generalization error of the classifier. The proposed instance selection filter method simultaneously optimizes the correlation, redundancy and consistency of the datasets. Instance retention constraints are imposed on optimization models to retain a maximum percentage of samples, established by the decision maker, in big data scenarios. The experiments have been designed to compare (1) the NSGA-II and MODE algorithms, (2) two- and three-objective optimization models, (3) two different constraint handling techniques, and (4) the proposed evolutionary approaches and other 12 non-evolutionary approaches used in literature. The proposed wrapper and filter instance selection methods have been used in a real-world business engineering application, and have also been validated using three public datasets to facilitate the replicability of the research results. The results of the experiments show the superiority of the three-objective constrained evolutionary techniques proposed in this paper over the non-evolutionary techniques and over the two-objective evolutionary approaches used in the literature
Branching interval algebra: An almost complete picture
No full textBranching Algebra is the natural branching-time generalization of Allen's Interval Algebra. As in the linear case, the consistency problem for Branching Algebra is NP-HARD. Branching Algebra has many potential applications in different areas of Artificial Intelligence; therefore, being able to efficiently solve classical problems expressed in Branching Algebra is very important. This can be achieved in two steps: first, by identifying expressive enough, yet tractable fragments of the whole algebra, and, second, by using such fragments to boost the performances of a backtracking algorithm for the whole language. In this paper we study the properties of several such fragments, both from the algebraic and the computational point of view, and we give an almost complete picture of tractable and non-tractable fragments of the Branching Algebra
- …
