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