94 (1) 2009

1. Timed P Automata
   Roberto Barbuti,  Andrea Maggiolo-Schettini,  Paolo Milazzo,  Luca Tesei 1-19
   To study systems whose dynamics changes with time, an extension of timed P systems is introduced in which evolution rules may vary with time. The proposed model is a timed automaton with a discrete time domain and in which each state is a timed P system. A result on expressive power and on features of the formalism sufficient for full expressiveness is proved and, as an application example, the model of an ecological system is given.
2. Clausal Tableaux for Multimodal Logics of Belief
   Rajeev Goré,  Linh Anh Nguyen 21-40
   We develop clausal tableau calculi for six multimodal logics variously designed for reasoning about multi-degree belief, reasoning about distributed systems of belief and for reasoning about epistemic states of agents in multi-agent systems. Our tableau calculi are sound, complete, cut-free and have the analytic superformula property, thereby giving decision procedures for all of these logics. We also use our calculi to obtain complexity results for five of these logics. The complexity of the remaining logic was known.
3. Algebraic Properties of Generalized Rough Sets
   Michiro Kondo 41-48
   In this paper we consider the problem whether for a map j: A(B) ® B there is a relation R on A(B) such that properties of a map j^* : B® B are reflected to R. This is a converse problem that J.Järvinen proved in [5]. We give an affirmative answer to the problem. Moreover we give equational bases which characterize properties of the map j. This means that the classes of some types of algebras form varieties. Hence, there are full correspondence between properties of relations and varieties of modal algebras.
4. First-order Generalization of the MPMA Belief Update Operator
   Ewa Madalińska-Bugaj, Witold Łukaszewicz 49-61
   In this paper we generalize the MPMA belief update operator by admitting first-order knowledge bases and restricted first-order update formulae. This allows us to consider scenarios which cannot be properly formalized either in the original MPMA or in other existing approaches to belief update.
5. The Injectivity of the Global Function of a Cellular Automaton in the Hyperbolic Plane is Undecidable
   Maurice Margenstern 63-99
   In this paper, we look at the following question. We consider cellular automata in the hyperbolic plane, see [6,22,9,12] and we consider the global function defined on all possible configurations. Is the injectivity of this function undecidable? The problem was answered positively in the case of the Euclidean plane by Jarkko Kari, in 1994, see [4]. In the present paper, we show that the answer is also positive for the hyperbolic plane: the problem is undecidable.
6. Greedy Algorithms with Weights for Construction of Partial Association Rules
   Mikhail Ju. Moshkov,  Marcin Piliszczuk,  Beata Zielosko 101-120
   This paper is devoted to the study of approximate algorithms for minimization of the total weight of attributes occurring in partial association rules. We consider mainly greedy algorithms with weights for construction of rules. The paper contains bounds on precision of these algorithms and bounds on the minimal weight of partial association rules based on an information obtained during the greedy algorithm run.

94 (2) 2009

1. Fundamentals of Knowledge Technology - Preface i-i
2. An Extended Comparison of Six Approaches to Discretization - A Rough Set Approach
   Piotr Blajdo, Jerzy W. Grzymała-Busse,  Zdzisław S. Hippe,   Maksymilian Knap,  Teresa Mroczek,  Łukasz Piątek 121-131
   We present results of extensive experiments performed on nine data sets with numerical attributes using six promising discretization methods. For every method and every data set 30 experiments of ten-fold cross validation were conducted and then means and sample standard deviations were computed. Our results show that for a specific data set it is essential to choose an appropriate discretization method since performance of discretization methods differ significantly. However, in general, among all of these discretization methods there is no statistically significant worst or best method. Thus, in practice, for a given data set the best discretization method should be selected individually.
3. Dominance-Based Rough Sets Using Indexed Blocks as Granules
   Chien-Chung Chan, Gwo-Hshiung Tzeng 133-146
   Dominance-based rough set introduced by Greco et al. is an extension of Pawlak's classical rough set theory by using dominance relations in place of equivalence relations for approximating sets of preference ordered decision classes satisfying upward and downward union properties. This paper introduces the concept of indexed blocks for representing dominance-based approximation spaces. Indexed blocks are sets of objects indexed by pairs of decision values. In our study, inconsistent information is represented by exclusive neighborhoods of indexed blocks. They are used to define approximations of decision classes. It turns out that a set of indexed blocks with exclusive neighborhoods forms a partition on the universe of objects. Sequential rules for updating indexed blocks incrementally are considered and illustrated with examples.
4. Approximation Algebra and Framework
   Davide Ciucci 147-161
   Generalized approximation algebras and approximation algebras are defined as a theoretical counterpart of all the situations where a "lower" and an "upper" mapping are used. Some models of these structures are discusse, among them rough sets, fuzzy rough sets and possibility theory. Generalized approximation framework and approximation framework are also introduced as an abstraction of all those cases where several approximations are possibile on the same element. Also in this case some examples are given.
5. Learning Rule Ensembles for Ordinal Classification with Monotonicity Constraints
   Krzysztof Dembczyński,  Wojciech Kotowski,  Roman Słowiński 163-178
   Ordinal classification problems with monotonicity constraints (also referred to as multicriteria classification problems) often appear in real-life applications, however, they are considered relatively less frequently in theoretical studies than regular classification problems. We introduce a rule induction algorithm based on the statistical learning approach that is tailored for this type of problems. The algorithm first monotonizes the dataset (excludes strongly inconsistent objects), using Stochastic Dominance-based Rough Set Approach, and then uses forward stagewise additive modeling framework for generating a monotone rule ensemble. Experimental results indicate that taking into account knowledge about order and monotonicity constraints in the classifier can improve the prediction accuracy.
6. Single 2D Image-based 3D Face Reconstruction and Its Application in Pose Estimation
   Xun Gong,  Guoyin Wang,  Lili Xiong 179-195
   Human beings are born with a natural capacity of recovering shape from merely one image. However, it is still a challenging mission for current techniques to make a computer have such an ability. To simulate the modeling procedure of human visual system, a Ternary Deformation Framework (TDF) is proposed to reconstruct a realistic 3D face from one 2D frontal facial image, with prior knowledge regarding facial shape learnt from a 3D face data set. Based upon the reconstructed 3D face, a novel method via linear regression is then proposed to estimate that person's pose on another image with pose variations. Simulation results show that TDF outperforms the conventional methods with respect to the modeling precision and that reconstructions on real photographs have achieved favorable visual effects. Moreover, the comparison results validated the effectiveness of using the 3D face in the proposed pose estimation method.
7. Pairwise Comparisons Based Non-Numerical Ranking
   Ryszard Janicki 197-217
   A systematic procedure for deriving weakly ordered non-numerical rankings from given sets of data is proposed and analysed. The data are assumed to be collected using the Pairwise Comparisons paradigm. The concept of a partially ordered approximation of an arbitrary binary relation is formally defined and some solutions are proposed. The problem of testing and the importance of indifference and the power of weak order extensions are also discussed.
8. A Two-Phase Model for Learning Rules from Incomplete Data
   Huaxiong Li,  Yiyu Yao,  Xianzhong Zhou,  Bing Huang 219-232
   A two-phase learning strategy for rule induction from incomplete data is proposed, and a new form of rules is introduced so that a user can easily identify attributes with or without missing values in a rule. Two levels of measurement are assigned to a rule. An algorithm for two-phase rule induction is presented. Instead of filling in missing attribute values before or during the process of rule induction, we divide rule induction into two phases. In the first phase, rules and partial rules are induced based on non-missing values. In the second phase, partial rules are modified and refined by the imputation of some missing values. Such rules truthfully reflect the knowledge embedded in the incomplete data. The study not only presents a new view of rule induction from incomplete data, but also provides a practical solution. Experiments validate the effectiveness of the proposed method.
9. Semi-supervised Rough Cost/Benefit Decisions
   Pawan Lingras,  Min Chen,  Duoqian Miao 233-244
   Most of the business decisions are based on cost and benefit considerations. Data mining techniques that make it possible for the businesses to incorporate financial considerations will be more meaningful to the decision makers. Decision theoretic framework has been helpful in providing a better understanding of classification models. This study describes a semi-supervised decision theoretic rough set model. The model is based on an extension of decision theoretic model proposed by Yao. The proposal is used to model financial cost/benefit scenarios for a promotional campaign in a real-world retail store.
10. An Incremental Approach for Inducing Knowledge from Dynamic Information Systems
    Dun Liu, Tianrui Li, Da Ruan,  Weili Zou 245-260
    Knowledge in an information system evolves with its dynamical environment. A new concept of interesting knowledge based on both accuracy and coverage is defined in this paper for dynamic information systems. An incremental model and approach as well as its algorithm for inducing interesting knowledge are proposed when the object set varies over time. A case study validates the feasibility of the proposed method.
11. An Integration of Cloud Transform and Rough Set Theory to Induction of Decision Trees
    Jing Song,  Tianrui Li,  Da Ruan 261-273
    Decision trees are one of the most popular data-mining techniques for knowledge discovery. Many approaches for induction of decision trees often deal with the continuous data and missing values in information systems. However, they do not perform well in real situations. This paper presents a new algorithm, decision tree construction based on the Cloud transform and Rough set theory under the characteristic relation (CR), for mining classification knowledge from a given data set. The continuous data is transformed into discrete qualitative concepts via the cloud transformation and then the attribute with the smallest weighted mean roughness under the characteristic relation is selected as the current splitting node. Experimental evaluation shows the decision trees constructed by the CR algorithm tend to have a simpler structure, much higher classification accuracy and more understandable rules than those by C5.0 in most cases.

94 (3-4) 2009

1. Fundamenta Informaticae (2009) Petri Nets 2008 - Preface i-ii
2. Synthesis of Nets with Step Firing Policies
   Philippe Darondeau, Maciej Koutny,  Marta Pietkiewicz-Koutny,  Alex Yakovlev 275-303
   The unconstrained step semantics of Petri nets is impractical for simulating and modelling applications. In the past, this inadequacy has been alleviated by introducing various flavours of maximally concurrent semantics, as well as priority orders. In this paper, we introduce a general way of controlling step semantics of Petri nets through step firing policies that restrict the concurrent behaviour of Petri nets and so improve their execution and modelling features. In a nutshell, a step firing policy disables at each marking a subset of enabled steps which could otherwise be executed. We discuss various examples of step firing policies and then investigate the synthesis problem for Petri nets controlled by such policies. Using generalised regions of step transition systems, we provide an axiomatic characterisation of those transition systems which can be realised as reachability graphs of Petri nets controlled by a given step firing policy. We also provide two different decision and synthesis algorithms for PT-nets and step firing policies based on linear rewards of steps, where the reward for firing a single transition is either fixed or it depends on the current net marking. The simplicity of the algorithms supports our claim that the proposed approach is practical.
3. A Net-based Approach to Web Services Publication and Replaceability
   Filippo Bonchi,  Antonio Brogi,  Sara Corfini,  Fabio Gadducci 305-330
   Web services represent a promising technology for the development of distributed heterogeneous software systems. In this setting, a major issue is to establish whether two services can be used interchangeably in any context. To this aim, our paper first briefly reviews the results contained in a recent article by the same authors, where a suitable notion of behavioural equivalence for Web services was introduced. Our work then extends those results, in order to account for ontology-based service specifications. Next, a concrete example scenario - a car rental system - is presented, and it is then used to illustrate how the equivalence between services can be fruitfully employed for correctly addressing two prominent, modularity-related problems: the publication of correct service specifications and the replaceability of (sub)services.
4. Unfolding Semantics of Petri Nets Based on Token Flows
   Robin Bergenthum,  Sebastian Mauser,  Robert Lorenz,  Gabriel Juhas 331-360
   In this paper we propose two new unfolding semantics for general Petri nets combining the concept of prime event structures with the idea of token flows developed in [13]. In contrast to the standard unfolding based on branching processes, one of the presented unfolding models avoids to represent isomorphic processes while the other additionally reduces the number of (possibly non-isomorphic) processes with isomorphic underlying runs. We show that both the proposed unfolding models still represent the complete partial order behavior. Moreover, in both cases it is possible to construct complete finite prefixes for bounded nets through applying the known theory of cut-off events. In particular, canonical prefixes w.r.t. a given cutting context can be defined and computed for bounded nets. We present implementations of construction algorithms for complete finite prefixes of both the unfolding models. Experimental results show that the computed prefixes are much smaller and can be constructed significantly faster than in the case of the standard unfolding.
5. Modelling and Validation of Secure Connection Establishment in a Generic Access Network Scenario
   Lars M. Kristensen, Paul Fleischer 361-386
   The Generic Access Network (GAN) architecture is defined by the 3rd Generation Partnership Project (3GPP) and allows telephone services, such as SMS and voice-calls, to be accessed via Internet Protocol (IP) networks. The main usage of this is to allow mobile phones to use WiFi in addition to the usual GSM network. The GAN specification relies on the Internet Protocol Security layer (IPSec) and the Internet Key Exchange protocol (IKEv2) to provide encryption across IP networks, and thus avoid compromising the security of the telephone networks. The detailed usage of these two Internet protocols (IPSec and IKEv2) is not fully described in the GAN specification. As part of the process to develop solutions to support the GAN architecture, TietoEnator Denmark has developed a detailed GAN scenario which describes how IPSec and IKEv2 are to be used during the connection establishment procedure. This paper presents an industrial project where Coloured Petri Nets (CPNs) were used to specify and validate the detailed GAN scenario considered by TietoEnator.
6. Process Discovery using Integer Linear Programming
   J.M.E.M. van der Werf,  B.F. van Dongen,  C.A.J. Hurkens,  A. Serebrenik 387-412
   The research domain of process discovery aims at constructing a process model (e.g. a Petri net) which is an abstract representation of an execution log. Such a model should (1) be able to reproduce the log under consideration and (2) be independent of the number of cases in the log. In this paper, we present a process discovery algorithm where we use concepts taken from the language-based theory of regions, a well-known Petri net research area. We identify a number of shortcomings of this theory from the process discovery perspective, and we provide solutions based on integer linear programming.
7. Building Efficient Model Checkers using Hierarchical Set Decision Diagrams and Automatic Saturation
   Alexandre Hamez,  Yann Thierry-Mieg,  Fabrice Kordon 413-437
   Shared decision diagram representations of a state-space provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is tricky, as the construction procedure is liable to produce intractable intermediate structures (a.k.a peak effect). The definition of the so-called saturation method has empirically been shown to mostly avoid this peak effect, and allows verification of much larger systems. However, applying this algorithm currently requires deep knowledge of the decision diagram data structures.
   Hierarchical Set Decision Diagrams (SDD) are decision diagrams in which arcs of the structure are labeled with sets, themselves stored as SDD. This data structure offers an elegant and very efficient way of encoding structured specifications using decision diagram technology. It also offers, through the concept of inductive homomorphisms, flexibility to a user defining a symbolic transition relation. We show in this paper how, with very limited user input, the SDD library is able to optimize evaluation of a transition relation to produce a saturation effect at runtime.
   We build as an example an SDD model-checker for a compositional formalism: Instantiable Petri Nets (IPN). IPN define a type as an abstract contract. Labeled P/T nets are used as an elementary type. A composite type is defined to hierarchically contain instances (of elementary or composite type). To compose behaviors, IPN use classic label synchronization semantics from process calculi.
   With a particular recursive folding SDD are able to offer solutions for symmetric systems in logarithmic complexity with respect to other DD. Even in less regular cases, the use of hierarchy in the specification is shown to be well supported by SDD. Experimentations and performances are reported on some well known examples.
8. A Practical Approach to Verification of Mobile Systems Using Net Unfoldings
   Roland Meyer,  Victor Khomenko, Tim Strazny 439-471
   We propose a technique for verification of mobile systems. We translate finite control processes, a well-known subset of p-Calculus, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe processes, a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime. We also demonstrate the applicability of our method on a realistic model of an automated manufacturing system.