Fundamenta Informaticae - Volume 135, issue 4

Authors: Penczek, Wojciech | Czaja, Ludwik

Article Type: Other

DOI: 10.3233/FI-2014-1126

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. i-i, 2014

Authors: Betts, Jack | Müller, Berndt

Article Type: Research Article

Abstract: We introduce a layered approach to multi-agent programming and motivate this with a perspective to smart home environments. Apart from the core layer, layer components can be updated at runtime to reflect, e.g., attributes like credibility and the addition of proprietary functionality. The Layered Agent Framework (LAF) is defined by interfaces and organised into layers. This approach minimises system fragmentation while allowing developers to create and maintain meaningful and effective agents. A Petri net model is provided to visualise and execute prototypes of the agents. Although fully functional, the Petri nets will later be translated into dedicated programs with a …smaller footprint and more efficient execution. Show more

Keywords: Multi-Agent Systems, Home Automation, Smart Home, Layered Architecture

DOI: 10.3233/FI-2014-1127

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 341-353, 2014

Authors: Castiglioni, Valentina | Lanotte, Ruggero | Tini, Simone

Article Type: Research Article

Abstract: Rule formats are sets of syntactical constraints over SOS rules ensuring semantical properties of the derived LTS. Given a rule format, our proposal is to relax the constraints imposed on each single rule and to introduce some constraints on the form of the whole set of rules, thus obtaining a new format ensuring the same semantical property and being less demanding than the original one. We apply our idea to a well known rule format for rooted branching bisimulation equivalence.

Keywords: Weak equivalence, rooted branching bisimulation, specification format

DOI: 10.3233/FI-2014-1128

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 355-369, 2014

Authors: Grabowski, Adam

Article Type: Research Article

Abstract: Theory exploration is a term describing the development of a formal approach to selected topic, usually within mathematics or computer science, with the help of an automated proof-assistant. This activity however usually doesn't reflect the view of science considered as a whole, not as separated islands of knowledge. Merging theories essentially has its primary aim of bridging these gaps between specific disciplines. As we provided formal apparatus for basic notions within rough set theory (as e.g. approximation operators and membership functions), we try to reuse the knowledge which is already contained in available repositories of computer-checked mathematical knowledge, or which …can be obtained in a relatively easy way. We can point out at least three topics here: topological aspects of rough sets – as approximation operators have properties of the topological interior and closure; possible connections with formal concept analysis; lattice-theoretic approach giving the algebraic viewpoint (e.g. Stone algebras). In the first case, we discovered semiautomatically some connections with Isomichi's classification of subsets of a topological space and with the problem of fourteen Kuratowski sets. This paper is also a brief description of the computer source code which is a feasible illustration of our approach – nearly two thousand lines containing all the formal proofs (essentially we omit them in the paper). In such a way we can give the formal characterization of rough sets in terms of topologies or orders. Although fully formal, still the approach can be revised to keep the uniformity all the time. Show more

Keywords: rough sets, rough concept analysis, knowledge management, formal topology

DOI: 10.3233/FI-2014-1129

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 371-385, 2014

Authors: Heitmann, Frank | Köhler-Bußmeier, Michael

Article Type: Research Article

Abstract: Elementary object systems (EOS for short) are Petri nets in which tokens may be Petri nets again. Originally proposed by Valk for a two levelled structure, the formalism was later generalised for arbitrary nesting structures. However, even if restricted to a nesting depth of two, EOS are Turing-complete and thus many problems like reachability and liveness are undecidable for them. Nonetheless, since they are useful to model many practical applications a natural question is how to restrict the formalism in such a way, that the resulting restricted formalism is still helpful in a modelling context, but so that important verification …problems like reachability become quickly decidable. In the last years several structural and dynamic restrictions for EOS have therefore been investigated. These investigations have been central to the first author's recent PhD thesis and have been published in past editions of this journal and on conferences. In this paper we add several new results and present them together with the old in a unified fashion highlighting the central message of these investigations. Show more

Keywords: high-level Petri net models, nets-within-nets, restrictions, reachability

DOI: 10.3233/FI-2014-1130

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 387-401, 2014

Authors: Kacprzak, Magdalena | Sawicka, Anna

Article Type: Research Article

Abstract: This paper is a continuation of the work [26] in which the LND dialogue system was proposed. LND reconstructs the dialogical logic introduced by Lorenzen using the terminology of persuasion dialogue games as specified by Prakken [18]. The aim of the LND system is to recognize formal fallacies in natural dialogues and remove them. Now we extend this system to include a new protocol enabling the reconstruction of natural dialogues in which parties can commit formal fallacies. We then present the implementation of the protocols applied.

DOI: 10.3233/FI-2014-1131

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 403-417, 2014

Authors: Karbowska-Chilinska, Joanna | Zabielski, Pawel

Article Type: Research Article

Abstract: The Orienteering Problem with Time Windows (OPTW) is an optimisation NP-hard problem. This paper proposes a hybrid genetic algorithm (GAPR) for approximating a solution to the OPTW. Instead of a crossover we use a path relinking (PR) strategy as a form of intensification solution. PR generates a new solution by exploring trajectories between two random solutions: genes not present in one solution are included in the other one. Experiments performed on popular benchmark instances show that the proposed GAPR gives good quality solutions using short computing times. Moreover, GAPR gives new best solutions for some test instances.

Keywords: orienteering problem with time windows, genetic algorithm, path relinking

DOI: 10.3233/FI-2014-1132

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 419-431, 2014

Authors: Nguyen, Linh Anh | Golińska-Pilarek, Joanna

Article Type: Research Article

Abstract: We present the first tableau method with an EXPTIME (optimal) complexity for checking satisfiability of a knowledge base in the description logic ${\cal{SHOQ}}$, which extends ${\cal{ALC}}$ with transitive roles, hierarchies of roles, nominals and qualified number restrictions. The complexity is measured using unary representation for numbers (in number restrictions). Our procedure is based on global caching and integer linear feasibility checking.

Keywords: automated reasoning, description logics, global state caching, integer linear feasibility

DOI: 10.3233/FI-2014-1133

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 433-449, 2014

Authors: Niewiadomski, Artur | Skaruz, Jaroslaw | Penczek, Wojciech | Szreter, Maciej | Jarocki, Mariusz

Article Type: Research Article

Abstract: The paper deals with the concrete planning problem (CPP) – a stage of the Web Service Composition (WSC) in the PlanICS framework. The complexity of the problem is discussed. A novel SMT-based approach to CPP is defined and its performance is compared to the standard Genetic Algorithm (GA) and the OpenOpt numerical toolset planner in the framework of the PlanICS system. The discussion of all the approaches is supported by extensive experimental results.

Keywords: Web Service Composition, SMT, GA, OpenOpt, Concrete Planning

DOI: 10.3233/FI-2014-1134

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 451-466, 2014

Authors: Półrola, Agata | Cybula, Piotr | Męski, Artur

Article Type: Research Article

Abstract: Time Petri nets by Merlin and Farber are a powerful modelling formalism. However, symbolic model checking methods for them consider in most cases the nets which are 1-safe, i.e., allow the places to contain at most one token. In our paper we present an approach which applies symbolic verification to testing reachability for time Petri nets without this restriction. We deal with the class of bounded nets restricted to disallow multiple enabledness of transitions, and present the method of reachability testing based on a translation into a satisfiability modulo theory (SMT).

DOI: 10.3233/FI-2014-1135

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 467-482, 2014

Authors: Przymus, Piotr | Kaczmarski, Krzysztof | Stencel, Krzysztof

Article Type: Research Article

Abstract: Graphics Processing Units (GPU) have significantly more applications than just rendering images. They are also used in general-purpose computing to solve problems that can benefit from massive parallel processing. However, there are tasks that either hardly suit GPU or fit GPU only partially. The latter class is the focus of this paper. We elaborate on hybrid CPU/GPU computation and build optimization methods that seek the equilibrium between these two computation platforms. The method is based on heuristic search for bi-objective Pareto optimal execution plans in presence of multiple concurrent queries. The underlying model mimics the commodity market where devices are …producers and queries are consumers. The value of resources of computing devices is controlled by supply-and-demand laws. Our model of the optimization criteria allows finding solutions of problems not yet addressed in heterogeneous query processing. Furthermore, it also offers lower time complexity and higher accuracy than other methods. Show more

Keywords: heterogeneous environment, GPU, CUDA, query processing

DOI: 10.3233/FI-2014-1136

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 483-501, 2014

Authors: Suraj, Zbigniew | Grochowalski, Piotr

Article Type: Research Article

Abstract: The aim of this paper is to present a new version of a bibliographic database system - Rough Set Database System (RSDS). The RSDS system, among others, includes bibliographic descriptions of publications on rough set theory and its applications. This system is also an experimental environment for research related to the processing of bibliographic data using the domain knowledge and the related information retrieval.

Keywords: rough sets, data mining, knowledge discovery, pattern recognition, database systems

DOI: 10.3233/FI-2014-1137

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 503-519, 2014

Authors: Wagler, Annegret K. | Wegener, Jan-Thierry

Article Type: Research Article

Abstract: The context of this work is the reconstruction of Petri net models for biological systems from experimental data. Such methods aim at generating all network alternatives fitting the given data. For a successful reconstruction, the data need to satisfy two properties: reproducibility and monotonicity. In this paper, we focus on a necessary preprocessing step for a recent reconstruction approach. We test the data for reproducibility, provide a feasibility test to detect cases where the reconstruction from the given data may fail, and provide a strategy to cope with the infeasible cases. After having performed the preprocessing step, it is guaranteed …that the (given or modified) data are appropriate as input for the main reconstruction algorithm. Show more

DOI: 10.3233/FI-2014-1138

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 521-535, 2014

Authors: Wiśniewski, Piotr | Stencel, Krzysztof

Article Type: Research Article

Abstract: Analytic database queries are exceptionally time consuming. Decision support systems employ various execution techniques in order to accelerate such queries and reduce their resource consumption. Probably the most important of them consists in materialization of partial results. However, any introduction of derived objects into the database schema increases the cost of software development, since programmers must take care of their usage and synchronization. In this article we consider using partial aggregations materialized in additional tables. The idea is based on the concept of metagranules that represent the information on grouping and used aggregations. Metagranules have a natural partial order that …guides the optimisation process. We present solutions to two problems. Firstly, we assume that a set of stored metagranules is given and we optimize a query. We present a novel query rewriting method to make analytic queries use the information stored in metagranules. We also describe our proof-of-concept implementation of this method and perform an extensive experimental evaluation using databases of the size up to 0:5 TiB and 6 billions rows. Secondly, we assume that a database workload is given and we want to select the optimal set of metagranules to materialize. Although each metagranule accelerates some queries, it also imposes a significant overhead on updates. Therefore, we propose a cost model that includes both benefits for queries and penalties for updates. We experiment with the complete search in the space of sets of metagranules to find the optimum. Finally, we empirically verify identified optimal sets against database instances up to 0:5 TiB with billions of rows and hundreds millions of aggregated rows. Show more

DOI: 10.3233/FI-2014-1139

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 537-551, 2014

Authors: Woźna-Szcześniak, Bożena | Zbrzezny, Andrzej

Article Type: Research Article

Abstract: We investigate a SAT-based bounded model checking (BMC) method for MTL (metric temporal logic) that is interpreted over linear discrete infinite time models generated by discrete timed automata. In particular, we translate the existential model checking problem for MTL to the existential model checking problem for a variant of linear temporal logic (called HLTL), and we provide a SAT-based BMC technique for HLTL. We show how to implement the BMC technique for HLTL and discrete timed automata, and as a case study we apply the technique in the analysis of GTPP, a Generic Timed Pipeline Paradigm modelled by a network …of discrete timed automata. Show more

DOI: 10.3233/FI-2014-1140

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 553-568, 2014

Article Type: Other

Citation: Fundamenta Informaticae, vol. 135, no. 4, pp. 569-570, 2014