122 (1-2) 2013
- Applications and Theory of Petri Nets and Other Models of Concurrency, 2011 Preface i-ii
- Minimal Coverability Set for Petri Nets:
Karp and Miller Algorithm with Pruning
Pierre-Alain Reynier, Frédéric Servais 1-30
This paper presents the Monotone-Pruning algorithm () for
computing the minimal coverability set of Petri nets. The original
Karp and Miller algorithm () unfolds the reachability graph of a
Petri net and uses acceleration on branches to ensure
termination. The algorithm improves the algorithm by adding
pruning between branches of the tree. This idea was first
introduced in the Minimal Coverability Tree algorithm (),
however it was recently shown to be incomplete. The
algorithm can be viewed as the algorithm with a slightly more
aggressive pruning strategy which ensures completeness. Experimental
results show that this algorithm is a strong improvement over the
algorithm as it dramatically reduces the exploration tree.
- Branching Processes of General Petri Nets
Jean-Michel Couvreur, Denis Poitrenaud, Pascal Weil 31-58
We propose a new model of branching processes, suitable for
describing the behavior of general Petri nets, without any
finiteness or safeness assumption. In this framework, we define a
new class of branching processes and unfoldings of a net N, which
we call faithful. These coincide with the safe branching processes and
unfoldings if N is safe, or weakly safe as in [Engelfriet 1991],
but not in general. However, faithful branching processes and processes
satisfy the good order-theoretic properties which make the safe
processes of safe nets so useful in practice, and which are known not to
hold for the safe processes of a general net. Faithful processes
represent therefore good candidates to generalize the theory of safe
nets to the general case.
- Refinement of Synchronizable Places with Multi-workflow Nets
Kees M. van Hee, Natalia Sidorova, Jan Martijn van der Werf 59-83
Stepwise refinement is a well-known strategy in system modeling. The refinement rules should preserve essential behavioral properties, such as deadlock freedom, boundedness and weak termination.
A well-known example is the refinement rule that replaces a safe place of a Petri net with a sound workflow net.
In this case a token on the refined place undergoes a procedure that is modeled in detail by the refining workflow net.
We generalize this rule to component-based systems, where in the first, high-level, refinement iterations we often encounter in different components places that represent in fact the counterparts of the same procedure "simultaneously" executed by the components. The procedure involves communication between these components.
We model such a procedure as a multi-workflow net, which is actually a composition of communicating workflows. Behaviorally correct multi-workflow nets have the weak termination property. The weak termination requirement is also applied to the system being refined. We want to refine selected places in different components with a multi-workflow net in such a way that the weak termination property is preserved through refinements. We introduce the notion of synchronizable places and show that weak termination is preserved under the refinement of places with multiworks if and only if the refined places are synchronizable. We give a method to decide if a given set of places is synchronizable.
- A Petri Net Interpretation of Open Reconfigurable Systems
Frédéric Peschanski, Hanna Klaudel, Raymond Devillers 85-117
We present a Petri net interpretation of the pi-graphs - a graphical variant of the pi-calculus where recursion and replication are replaced by iteration.
The concise and syntax-driven translation can be used to reason in Petri net terms about open reconfigurable systems. We demonstrate that the pi-graphs and their translated high-level Petri nets agree at the semantic level. In consequence, existing results on pi-graphs naturally extend to the translated Petri nets, most notably a guarantee of finiteness by construction.
- Mutex Causality in Processes and Traces of General Elementary Nets
Jetty Kleijn, Maciej Koutny 119-146
A concurrent history represented by a
causality structure that captures the intrinsic, invariant
dependencies between its actions,
can be interpreted as defining a set of closely related
observations (e.g., step sequences).
Depending on the relationships observed in the
histories of a system, the concurrency paradigm to which it adheres
may be identified, with different concurrency paradigms
underpinned by different kinds of causality structures.
Elementary net systems with inhibitor arcs and mutex arcs
( ENIM-systems)
are a system model that
through its process semantics
and associated causality structures
fits the least restrictive concurrency paradigm.
One can also investigate the abstract behaviour of
an ENIM-system
by grouping together step sequences in equivalence classes
(generalised comtraces)
using the structural relations between its transitions.
The resulting concurrent histories
of the ENIM-system are consistent
with the generalised stratified order structures
underlying its processes.
The paper establishes a link between
ENIM-systems and trace theory
allowing one to discuss
different observations of concurrent behaviour
in a way that is consistent with the causality semantics defined
by the operationally defined processes.
- Synthesis and Analysis of Product-form Petri Nets
Serge Haddad, Jean Mairesse, Hoang-Thach Nguyen 147-172
For a large Markovian model, a "product form" is an
explicit description of the steady-state behaviour which is
otherwise generally untractable. Being first introduced in queueing networks,
it has been adapted to Markovian Petri nets. Here we address three relevant
issues for product-form Petri nets which were left fully or partially open: (1) we provide
a sound and complete set of rules for the synthesis; (2) we characterise
the exact complexity of classical problems like reachability; (3) we introduce a new subclass
for which the normalising constant (a crucial value for product-form expression) can be efficiently
computed.
122 (3) 2013
- Stochastic Populations, Power Law and Fitness Aggregation in Genetic Algorithms
Zhanshan (Sam) Ma 173-206
Natural populations are dynamic in both time and space. In biological populations such as insects, spatial distribution patterns are often studied as the first step to characterize population dynamics. In nature, the spatial distribution patterns of insect populations are considered as the emergent expression (property) of individual behaviors at population levels and are fine-tuned or optimized by natural selection. This inspiration prompts us to investigate the possibly similar mechanisms in Genetic Algorithms (GA) populations. In this study, we introduce the mathematical models for the spatial distribution patterns of insect populations to GA with the conjecture that the emulation of biological populations in nature may lead to computational improvement. In particular, we introduce three modeling approaches from the research of spatial distribution patterns of insect populations: (i) probability distribution modeling approach, (ii) aggregation index approach, and (iii) Taylor's (1961, 1977) Power Law, Iwao's (1968, 1976) Mean Crowding Model and Ma's (1991c) population aggregation critical density (PACD), to characterize populations in GA. With these three approaches, we investigate four mappings from the research field of insect spatial distribution patterns to GA populations in order to search for possible counterpart mechanisms or features in GA. They are: (i) mapping insect spatial distribution patterns to GA populations or allowing GA populations to be controlled by stochastic distribution models that describe insect spatial distributions; (ii) mapping insect population distribution to GA population fitness distribution via Power Law andPACD modeling; (iii) mapping population aggregation dynamics to GA fitness progression across generations (or
fitness aggregation dynamics in GA) via insect population aggregation index; (iv) mapping insect population sampling model to optimal GA population sizing. With regard to the mapping (i), the experiment results show the significant improvements in GA computational efficiency in terms of the reduced fitness evaluations and associated costs. This prompts us to suggest using probability distribution models, or what we call stochastic GA populations, to replace the fixed-size population settings. We also found the counterpart for the second mapping, the wide applicability of Power Law and Mean Crowding model to the fitness distribution in GA populations. The testing of the third and fourth mappings is very preliminary; we use example cases to suggest two further research problems: the potential to use fitness aggregation dynamics for controlling the number of generations iterated in GA searches, and the possibility to use fitness aggregation distribution parameters [(obtained in mapping (ii)] in determining the optimum population size in GA. A third interesting research problem is to investigate the relationship between mapping (i) and (iii), i.e., the controlling of both population sizes and population generations.
- Crisp and Fuzzy Topological Interior and Closure Operators with Inclusion Degree. Theory and Applications
Homa Fashandi, James F. Peters 207-225
This article introduces interior and closure operators with inclusion
degree considered within a crisp or fuzzy topological framework. First, inclusion degree is introduced in an extension of the interior and closure operators in crisp topology. This idea is then introduced in fuzzy topology by
incorporating a relaxed version of fuzzy subsethood. The introduction of inclusion degree leads to a means of dealing with imperfections and small errors, especially in cases such as digital images where boundaries of subsets of an image are not crisp. The properties of the new operators are presented. Applications of the proposed operators are given in terms of rough sets and mathematical morphology.
- Some Methodological Remarks Inspired by the Paper "On inner classes" by A. Igarashi and B. Pierce
Hans Langmaack, Andrzej Salwicki 227-274
In [14] an axiomatic approach towards the semantics of FJI, Featherweight Java with Inner classes, essentially a subset of the Java-programming language, is presented. In this way the authors contribute to an ambitious project:
to give an axiomatic definition of the semantics of programming language
Java.
At a first glance the approach of reducing Java's semantics to that of FJI seems promising. We are going to show that several questions have been left unanswered. It turns out that the theory how to elaborate or bind types and thus to determine direct superclasses as proposed in [14] has different models. Therefore the suggestion that the formal system of [14] defines the (exactly one) semantics of Java is not justified.
We present our contribution to the project showing that it must be
attacked from another starting point.
Quite frequently one encounters a set of inference rules and a claim that a semantics is defined by the rules. Such a claim should be proved. One should present arguments: 1^{0} that the system has a model and hence it is a consistent system, and 2^{0} that all models are isomorphic. Sometimes such a proposed system contains a rule with a premise which reads: there is no proof of something. One should notice that this is a metatheoretic property. It seems strange to accept a metatheorem as a premise, especially if such a system does not offer any other inference rules which would enable a proof of the premise. We are going to study the system in [14]. We shall show that it has many non-isomorphic models. We present a repair of Igarashi's and Pierce's calculus such that their ideas are preserved as close as possible.
122 (4) 2013
- Neighbourhood of Constant Order in the Interval Graph of a Random Boolean Function
Jakub Daubner, Eduard Toman 275-295
In the present paper we estimate the size of a neighbourhood of constant order in the interval graph of a random Boolean function. So far, no bound of this parameter has been known.
- Modeling Group Scheduling Problems in Space and Time by Timed Petri Nets
Daniel Graff, Jan Richling, Matthias Werner 297-313
Dealing with cyber-physical systems (CPS) puts a strong emphasis on the
interaction between computing and non-computing elements. Since the physical
world is characterized by being strongly distributed and concurrent, this is
also reflected in the computational world making the design of such systems a
challenging task. If a number of tasks shall be executed on a CPS which are
bound to time and space, may have dependencies to other tasks and requires a
specific amount of computing devices, a solution requires a four-dimensional
space-time schedule which includes positioning of the devices resulting in an
NP-hard problem.
In this paper, we address the problem of spatial-temporal group scheduling
using Timed Petri nets. We use Timed Petri nets in order to model the spatial,
temporal, ordered and concurrent character of our mobile, distributed system.
Our model is based on a discrete topology in which devices can change their
location by moving from cell to cell. Using the time property of Petri nets,
we model movement in a heterogeneous terrain as well as task execution or
access to other resources of the devices. Given the modeling, we show how to
find an optimal schedule by translating the problem into a shortest path
problem, which is solvable with the known method of dynamic programming.
- On the Trade-off Between Ambiguity and Complexity in Contextual Languages
Lakshmanan Kuppusamy, Anand Mahendran, Kamala Krithivasan 315-326
Contextual grammars are introduced by Solomon Marcus in 1969 based on the fundamental concept of descriptive linguistics of
insertion of strings in given contexts. Internal contextual grammars are introduced by Paun and Nguyen in 1980. For contextual grammars several descriptional complexity measures and levels of ambiguity have been defined. In this paper, we analyze the trade-off between ambiguity and complexity of languages generated by internal contextual grammars. The notion of a pseudo inherently ambiguous language with respect to two
complexity measures is introduced and investigated. These languages can be generated by unambiguous grammars which are minimal with respect to one measure and ambiguous if they are minimal with respect to the other measure. An open problem from [15] is solved in this framework.
- Application of Reduction of the Set of Conditional Attributes in the Process of Global Decision-making
Małgorzata Przybyła-Kasperek, Alicja Wakulicz-Deja 327-355
The paper includes a discussion of issues related to the process of global decision-making on the basis of information stored in several local knowledge bases. The local knowledge bases contain information on the same subject, but are defined on different sets of conditional attributes that are not necessarily disjoint. A decision-making system, which uses a number of knowledge bases, makes global decisions on the basis of a set of conditional attributes specified for all of the local knowledge bases used.
The paper contains a description of a multi-agent decision-making system with a hierarchical structure. Additionally, it briefly overviews methods of inference that enable global decision-making in this system and that were proposed in our earlier works.
The paper also describes the application of the conditional attributes reduction technique to local knowledge bases. Our main aim was to investigate the effect of attribute reduction on the efficiency of inference in such a system. For a measure of the efficiency of inference, we mean mainly an error rate of classification, for which a definition is given later in this paper. Therefore, our goal was to reduce the error rate of classification.
- Interactive Exploration of Multi-Dimensional and Hierarchical Information Spaces with
Real-Time Preference Elicitation
Yannis Tzitzikas, Panagiotis Papadakos 357-399
Current proposals for preference-based information access seem to
ignore that users should be acquainted with the information space
and the available choices for describing effectively their
preferences. Furthermore users rarely formulate complex (preference or
plain) queries. The interaction paradigm of
Faceted Dynamic Taxonomies (FDT) allows users to explore an information space and
to restrict their focus without having to formulate queries. Instead
the users can restrict their focus (object set, or set of choices in general)
gradually through a simple set
of actions, each corresponding to a more refined query (formulated
on-the-fly) which can be enacted by a simple click.
In this paper we extend this interaction paradigm with actions that allow
users to dynamically express their preferences.
The proposed model supports progressive preference elicitation,
inherited preferences and scope-based resolution of conflicts
over single or multi-valued attributes with hierarchically organized values.
Finally we elaborate on the algorithmic perspective and
the applicability of the model over large information bases.
- A Translation of the Existential Model Checking Problem from MITL to HLTL
Bożena Woźna-Szcześniak, Andrzej Zbrzezny 401-420
In the paper we propose a translation of the existential model checking problem
for timed automata and properties expressible in MITL to the existential model checking problem for HLTL.
Such a translation, for example, allows to adopt LTL bounded model checking
method for verification of the MITL properties.