113(1) 2011

  1. Latin American Workshop on Logic Languages, Algorithms and New Methods of Reasoning (LANMR). Preface i-ii
  2. Solving the International Timetabling Competition: a Deterministic Approach
    Oscar Chávez-Bosquez,  Pilar Pozos-Parra,  Florian Lengyel 1-18
    The Course Timetabling Problem consists of the weekly scheduling of lectures of a collection of university courses, subject to certain constraints. The International Timetabling Competitions, ITC-2002 and ITC-2007, have been organized with the aim of creating a common formulation for comparison of solution proposals. This paper discusses the design and implementation of an extendable family of sorting-based mechanisms, called Sort Then Fix (STF) algorithms. ITC-2002 and ITC-2007 Post Enrolment based Course Timetabling problem instances were used in this study. The STF approach is deterministic, and does not require swapping or backtracking. Almost all solutions run in less than 10% of the ITC-2002 and less than 2% of the ITC-2007 benchmark times, respectively.
  3. Nested Preferences in Answer Set Programming
    Roberto Confalonieri,  Juan Carlos Nieves 19-39
    In this paper, we define a class of nested logic programs, called Nested Logic Programs with Ordered Disjunction (LPODs+), which makes it possible to specify conditional (qualitative) preferences by means of nested preference statements. To this end, we augment the syntax of Logic Programs with Ordered Disjunction (LPODs) to capture more general expressions. We define the LPODs+ semantics in a simple way and we extend most of the results of LPODs showing how our approach generalizes the LPODs framework in a proper way. We also show how the LPODs+ semantics can be computed in terms of a translation procedure that maps a nested ordered disjunction program (OD+-program) into a disjunctive logic program.
  4. A Possibilistic Argumentation Decision Making Framework with Default Reasoning
    Juan Carlos Nieves,  Roberto Confalonieri 41-61
    In this paper, we introduce a possibilistic argumentation-based decision making framework which is able to capture uncertain information and exceptions/defaults. In particular, we define the concept of a possibilistic decision making framework which is based on a possibilistic default theory, a set of decisions and a set of prioritized goals. This set of goals captures user preferences related to the achievement of a particular state in a decision making problem. By considering the inference of the possibilistic well-founded semantics, the concept of argument with respect to a decision is defined. This argument captures the feasibility of reaching a goal by applying a decision in a given context. The inference in the argumentation decision making framework is based on basic argumentation semantics. Since some basic argumentation semantics can infer more than one possible scenario of a possibilistic decision making problem, we define some criteria for selecting potential solutions of the problem.
  5. A Threshold for a Polynomial Solution of #2SAT
    Guillermo De Ita,  J. Raymundo Marcial-Romero,  José Antonio Hernández 63-77
    The #SAT problem is a classical #P-complete problem even for monotone, Horn and two conjunctive formulas (the last known as #2SAT). We present a novel branch and bound algorithm to solve the #2SAT problem exactly.
    Our procedure establishes a new threshold where #2SAT can be computed in polynomial time. We show that for any 2-CF formula F with n variables where #2SAT(F) £ p(n), for some polynomial p, #2SAT(F) is computed in polynomial time. This is a new way to measure the degree of difficulty for solving #2SAT and, according to such measure our algorithm allows to determine a boundary between `hard' and `easy' instances of the #2SAT problem.
  6. Armin: Automatic Trance Music Composition using Answer Set Programming
    Flavio Omar Everardo Pérez,  Fernando Antonio Aguilera Ramírez 79-96
    The Artificial Intelligence (AI) has taken a leading role in many activities which used to be made "by hand"; one of them is the musical composition. Such task now has another alternative implementation, through the support of software that can compose different musical genres to the point where a computer can compose pieces with some autonomy. This paper proposes Armin, a system dedicated to the electronic trance music composition. Armin’s aim is to provide a trance music composition to serve as a template or a base audio file, ready to add more instruments in a mastering (remastering) production – Additionally, it seeks to enable greater collaboration between a machine and a human, both seen as musical composers.

113(2) 2011

  1. Machine Learning in Bioinformatics. Preface. i-ii
  2. Uncovering Bivariate Interactions in High Dimensional Data Using Random Forests with Data Augmentation
    Jorge M Arevalillo,  Hilario Navarro 97-115
    Random Forests (RF) is an ensemble technology for classification and regression which has become widely accepted in the bioinformatics community in the last few years. Its predictive strength, along with some of the utilities, rich in information, provided by the output, has made RF an efficient data mining tool for discovering patterns in high dimensional data.
    In this paper we propose a search strategy that explores a subset of the input space in an exhaustive way using RF as the search engine. Our procedure begins by taking the variables previously rejected by a sequential search procedure and uses the out of bag error rate of the ensemble, obtained when trained over an augmented data set, as criterion to capture difficult to uncover bivariate patterns associated with an outcome variable. We will show the performance of the procedure in some synthetic scenarios and will give an application to a real microarray experiment in order to illustrate how it works for gene expression data.
  3. Efficient Search Methods for Statistical Dependency Rules
    Wilhelmiina Hämäläinen 117-150
    Dependency analysis is one of the central problems in bioinformatics and all empirical science. In genetics, for example, an important problem is to find which gene alleles are mutually dependent or which alleles and diseases are dependent. In ecology, a similar problem is to find dependencies between different species or groups of species. In both cases a classical solution is to consider all pairwise dependencies between single attributes and evaluate the relationships with some statistical measure like the c2-measure. It is known that the actual dependency structures can involve more attributes, but the existing computational methods are too inefficient for such an exhaustive search.
    In this paper, we introduce efficient search methods for positive dependencies of the form X ® A with typical statistical measures. The efficiency is achieved by a special kind of a branch-and-bound search which also prunes out redundant rules. Redundant attributes are especially harmful in dependency analysis, because they can blur the actual dependencies and even lead to erroneous conclusions.
    We consider two alternative definitions of redundancy: the classical one and a stricter one. We improve our previous algorithm for searching for the best strictly non-redundant dependency rules and introduce a totally new algorithm for searching for the best classically non-redundant rules. According to our experiments, both algorithms can prune the search space very efficiently, and in practice no minimum frequency thresholds are needed. This is an important benefit, because biological data sets are typically dense, and the alternative search methods would require too large minimum frequency thresholds for any practical purpose.
  4. Relational Feature Mining with Hierarchical Multitask kFOIL
    Elisa Cilia,  Niels Landwehr,  Andrea Passerini 151-177
    We introduce hierarchical kFOIL as a simple extension of the multitask kFOIL learning algorithm. The algorithm first learns a core logic representation common to all tasks, and then refines it by specialization on a per-task basis. The approach can be easily generalized to a deeper hierarchy of tasks. A task clustering algorithm is also proposed in order to automatically generate the task hierarchy. The approach is validated on problems of drug-resistance mutation prediction and protein structural classification. Experimental results show the advantage of the hierarchical version over both single and multi task alternatives and its potential usefulness in providing explanatory features for the domain. Task clustering allows to further improve performance when a deeper hierarchy is considered.

113(3-4) 2011

  1. Applications and Theory of Petri Nets and Other Models of Concurrency, 2010. Preface i-ii
  2. Separability in Persistent Petri Nets
    Eike Best,  Philippe Darondeau 179-203
    Separability in Petri nets means the property for a net k·N with an initial marking k·M to behave in the same way as k parallel instances of the same net N with an initial marking M, thus divided by k. We prove the separability of plain, bounded, reversible and persistent Petri nets, a class of nets that extends the well-known live and bounded marked graphs. We establish first a weak form of separability, already known to hold for marked graphs, in which every firing sequence of k·N is simulated by a firing sequence of k parallel instances of N with an identical firing count. We establish on top of this a strong form of separability, in which every firing sequence of k·N is simulated by an identical firing sequence of k parallel instances of N.
  3. Learning Workflow Petri Nets
    Javier Esparza,  Martin Leucker,  Maximilian Schlund 205-228
    Workflow mining is the task of automatically producing a workflow model from a set of event logs recording sequences of workflow events; each sequence corresponds to a use case or workflow instance. Formal approaches to workflow mining assume that the event log is complete (contains enough information to infer the workflow) which is often not the case. We present a learning approach that relaxes this assumption: if the event log is incomplete, our learning algorithm automatically derives queries about the executability of some event sequences. If a teacher answers these queries, the algorithm is guaranteed to terminate with a correct model. We provide matching upper and lower bounds on the number of queries required by the algorithm, and report on the application of an implementation to some examples.
  4. High-Level Petri Net Model Checking with AlPiNA
    Steve Hostettler,  Alexis Marechal,  Alban Linard,  Matteo Risoldi,  Didier Buchs 229-264
    Although model checking is heavily used in the hardware domain, it did not take off in software engineering yet. One of the possible reasons is that software models are very complex. They integrate many dimensions such as data types and concurrency, leading to the infamous state space explosion problem. This article introduces the Algebraic Petri Nets Analyzer (AlPiNA), a symbolic model checker for High-level Petri net. It is comprised of two independent modules: a GUI plug-in for Eclipse and an underlying model checking engine. AlPiNA is a step towards performing efficient and user-friendly model checking of large software systems. This is achieved by separating the model and its properties from the optimisation artifacts. This article describes the features that AlPiNA provides to the user for designing models and verifying properties. It also presents the techniques and artifacts used for tuning verification performance, along with some theoretical background.
  5. On Three Alternative Characterizations of Combined Traces
    Dai Tri Man Lê 265-293
    The combined trace (i.e., comtrace) notion was introduced by Janicki and Koutny in 1995 as a generalization of the Mazurkiewicz trace notion. Comtraces are congruence classes of step sequences, where the congruence relation is defined from two relations simultaneity and serializability on events. They also showed that comtraces correspond to some class of labeled stratified order structures, but left open the question of what class of labeled stratified orders represents comtraces. In this work, we proposed a class of labeled stratified order structures that captures exactly the comtrace notion. Our main technical contributions are representation theorems showing that comtrace quotient monoid, combined dependency graph (Kleijn and Koutny 2008) and our labeled stratified order structure characterization are three different and yet equivalent ways to represent comtraces. This paper is a revised and expanded version of Lê (in Proceedings of PETRI NETS 2010, LNCS 6128, pp. 104-124).
  6. Wendy: A Tool to Synthesize Partners for Services
    Niels Lohmann,  Daniela Weinberg 295-311
    Service-oriented computing proposes services as building blocks which can be composed to complex systems. To reason about the correctness of a service, its communication protocol needs to be analyzed. A fundamental correctness criterion for a service is the existence of a partner service, formalized in the notion of controllability.
    In this paper, we introduce Wendy, a Petri net-based tool to synthesize partner services. These partners are valuable artifacts to support the design, validation, verification, and adaptation of services. Furthermore, Wendy can calculate an operating guideline, a characterization of the set of all partners of a service. Operating guidelines can be used in many application scenarios from service brokerage to test case generation. Case studies show that Wendy efficiently performs on industrial service models.
  7. Accelerations for the Coverability Set of Petri Nets with Names
    Fernando Rosa-Velardo,  María Martos-Salgado,   David de Frutos-Escrig 313-341
    Pure names are identifiers with no relation between them, except equality and inequality. In previous works we have extended P/T nets with the capability of creating and managing pure names, obtaining n-PNs and proved that they are strictly well structured (WSTS), so that coverability and boundedness are decidable. Here we use the framework recently developed by Finkel and Goubault-Larrecq for forward analysis for WSTS, in the case of n-PNs, to compute the cover, that gives a good over approximation of the set of reachable markings. We prove that the least complete domain containing the set of markings is effectively representable. Moreover, we prove that in the completion we can compute least upper bounds of simple loops. Therefore, a forward Karp-Miller procedure that computes the cover is applicable. However, we prove that in general the cover is not computable, so that the procedure is non-terminating in general. As a corollary, we obtain the analogous result for Transfer Data nets and Data Nets. Finally, we show that a slight modification of the forward analysis yields decidability of a weak form of boundedness called width-boundedness, and identify a subclass of n-PN that we call dw-bounded n-PN, for which the cover is computable.
  8. Light Region-based Techniques for Process Discovery
    Marc Solé,  Josep Carmona 343-376
    A central problem in the area of Process Mining is to obtain a formal model that represents selected behavior of a system. The theory of regions has been applied to address this problem, enabling the derivation of a Petri net whose language includes a set of traces. However, when dealing with real-life systems, the available tool support for performing such a task is unsatisfactory, due to the complex algorithms that are required. In this paper, the theory of regions is revisited to devise a novel technique that explores the space of regions by combining the elements of a region basis. Due to its light space requirements, the approach can represent an important step for bridging the gap between the theory of regions and its industrial application. Experimental results show that there is improvement in orders of magnitude in comparison with state-of-the-art tools for the same task.
  9. Can Stubborn Sets be Optimal?
    Antti Valmari,  Henri Hansen 377-397
    Literature on the stubborn set and similar state space reduction methods presents numerous seemingly ad-hoc conditions for selecting the transitions that are investigated in the current state. There are good reasons to believe that the choice between them has a significant effect on reduction results, but not much has been published on this topic. This article presents theoretical results and examples that aim at shedding light on the issue. Because the topic is extensive, we only consider the detection of deadlocks. We distinguish between different places where choices can be made and investigate their effects. It is usually impractical to aim at choices that are "best" in some sense. However, one non-trivial practical optimality result is proven.
  10. Causal Behavioural Profiles - Efficient Computation, Applications, and Evaluation
    Matthias Weidlich,  Artem Polyvyanyy,  Jan Mendling,   Mathias Weske 399-435
    Analysis of behavioural consistency is an important aspect of software engineering. In process and service management, consistency verification of behavioural models has manifold applications. For instance, a business process model used as system specification and a corresponding workflow model used as implementation have to be consistent. Another example would be the analysis to what degree a process log of executed business operations is consistent with the corresponding normative process model. Typically, existing notions of behaviour equivalence, such as bisimulation and trace equivalence, are applied as consistency notions. Still, these notions are exponential in computation and yield a Boolean result. In many cases, however, a quantification of behavioural deviation is needed along with concepts to isolate the source of deviation.
    In this article, we propose causal behavioural profiles as the basis for a consistency notion. These profiles capture essential behavioural information, such as order, exclusiveness, and causality between pairs of activities of a process model. Consistency based on these profiles is weaker than trace equivalence, but can be computed efficiently for a broad class of models. In this article, we introduce techniques for the computation of causal behavioural profiles using structural decomposition techniques for sound free-choice workflow systems if unstructured net fragments are acyclic or can be traced back to S- or T-nets. We also elaborate on the findings of applying our technique to three industry model collections.