94 (1) 2009
- 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.
- 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.
- 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.
- 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.
- 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.
- 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
- Fundamentals of Knowledge Technology - Preface i-i
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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
- Fundamenta Informaticae (2009) Petri Nets 2008 - Preface i-ii
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.