@techreport{A14,
author = {Marko Rauhamaa},
title = {A Comparative Study of the Methods for Efficient Reachability Analysis},
type = {Research Report},
number = {A14},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = sep,
year = {1990},
pages = {61},
keywords = {reachability analysis, distributed systems, Petrisystems},
abstract = {Six recently proposed methods for efficient reachability analysis
of distributed systems are studied and compared:
symmetry method (Huber et al.), parameterising method (Lindqvist),
stubborn set method (Valmari), reduction theory (Berthelot, Haddad),
symbolic model checking (Burch et al.), and incomplete state-space
generation (Holzmann).
Petri systems are used as
the main presentation formalism. The methods are evaluated by how well they
are suited for practical reachability graph generation by computer.
One can summarise in brief that the stubborn set method, reduction theory
and incomplete state-space generation are found very promising and they
provide useful aid to practical reachability analysis. The symmetry method
yields a significant reduction in memory space but hardly in generation time.
Symbolic model checking is a very general method and immense sample
state-spaces have been analysed with it but it is likely that for most
practical systems the method performs far worse than the conventional
methods. The parameterising method is impractical and also its theoretical
profits are questionable. Finally, it is observed that most of the methods
are mutually independent and it is considered how they can be combined
to complement each other. Indeed, the symmetry method, stubborn set method,
reduction theory and incomplete state-space generation can all be used
simultaneously to obtain better results than with any of them alone.},
file = {A14.ps.Z}}
@techreport{A16,
author = {Johan Lilius},
title = {On the Compositionality and Analysis of Algebraic High-Level Nets},
type = {Research Report},
number = {A16},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = oct,
year = {1991},
pages = {77},
keywords = {net theory, category theory, algebraic specification,linear logic, Petri nets, high-level nets, compositionality},
abstract = {This work discusses three aspects of net
theory: compositionality of nets, analysis of nets and high-level
nets.
Net theory has often been criticised for the difficulty of giving a
compositional semantics to a net. In this work we discuss this
problem form a category theoretic point of view. In category theory
compositionality is represented by colimits. We show how a
high-level net can be mapped into a low-level net that represents its
behaviour. This construction is functorial and preserves colimits,
giving a compositional semantics for these high-level nets. Using this
semantics we propose some proof rules for compositional reasoning with
high-level nets.
Linear logic is a recently discovered logic that has many interesting
properties. From a net theoretic point of view its interest lies in
the fact that it is able to express resources in an analogous manner
to nets. Several interpretations of Petri nets in terms of linear
logic exist. In this work we study a model theoretic interpretation
where the behaviour of the net gives a model of linear logic. This
construction is extended to cover the algebraic high-level nets
defined in this work.},
file = {A16.ps.Z}}
@techreport{A18,
author = {Patric R. J. Östergård},
title = {Constructions of Mixed Covering Codes},
type = {Research Report},
number = {A18},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = dec,
year = {1991},
pages = {44},
keywords = {Covering code, covering radius, football pool problem,mixed code, simulated annealing},
abstract = {In this work construction methods for so called
mixed covering codes are developed. There has been considerable
recent growth in the interest in covering codes.
They have the property that all words in the space
are within a given Hamming distance, called the covering radius,
from some codeword.
Traditionally, mainly spaces where all coordinates have the
same arity (usually 2 or 3, that is, they are binary or ternary)
have been discussed. In this work we consider mixed spaces
F_{q_1}^{n_1}F_{q_2}^{n_2}\cdots F_{q_m}^{n_m}, where the
coordinates can be of varying arities. The approach is very
general, no restrictions are set upon m and the arities
q_i.
The construction methods consist of generalizations of known
constructions for covering codes and some completely new
constructions. They are divided into three classes; direct
constructions, constructions of new codes from old, and
the matrix method.
Through these constructions upper bounds for
the minimal number of codewords in a code covering a certain
space with a certain covering radius
(K_{q_1,q_2, ... ,q_m}(n_1,n_2, ... ,n_m;R)) are
improved. The results include a new record-breaking binary
code, proving K_2(12,2) <= 78.},
file = {A18.ps.Z}}
@techreport{A20,
author = {Jussi Rintanen},
title = {Stratification and Tractability in Nonmonotonic Reasoning},
type = {Research Report},
number = {A20},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = nov,
year = {1992},
pages = {71},
keywords = {nonmonotonic reasoning, autoepistemic logic, tractability, stratification},
abstract = {Knowledge-based systems use forms of reasoning that do
not satisfy the monotonicity property of classical logical
reasoning.
Therefore, several nonmonotonic logics have been developed for
the investigation of theoretical foundations of knowledge-based systems.
This work investigates efficient inference procedures for knowledge
representation using the framework of nonmonotonic logics.
Recent results show that nonmonotonic reasoning cannot be brought to
tractable level by restricting merely the form of the formulae.
In this work the impact of the structural property of stratification
on the complexity of nonmonotonic reasoning is investigated.
Autoepistemic logic is used as the framework for establishing the
results, because several other nonmonotonic formalisms can be embedded in it.
The main result of the work is that in stratified cases
the complexity of nonmonotonic reasoning is approximately the same
as that of corresponding classical monotonic reasoning.
This is shown by giving a general decision procedure
for stratified autoepistemic theories and analyzing its complexity with
respect to the complexity of the classical theorem-proving required.
It turns out that for theories for which the classical theorem-proving
is polynomial time, also the decision procedure runs in polynomial time.
As an example of this, two tractable classes of autoepistemic theories
based on the Horn clause subset of propositional logic are presented.
Also the implications of these results on the complexity of reasoning
in default logic, truth-maintenance systems, and propositional logic
programs are discussed.},
file = {A20.ps.Z}}
@techreport{A21,
author = {Tomi Janhunen},
title = {Weakened Negative Introspection in Autoepistemic Reasoning},
type = {Research Report},
number = {A21},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = feb,
year = {1993},
pages = {82},
keywords = {autoepistemic logic, nonmonotonic reasoning, weakened negative introspection},
abstract = {A new weakened scheme for negative introspection in autoepistemic
reasoning is proposed. The scheme is formulated proof-theoretically in
terms of enumerations of formulae. The resulting sets of conclusions
based on this negative introspection principle, cautious autoepistemic
expansions, generalize Moore style stable expansions such that every
set of premises has a cautious expansion. A finitary characterization
is developed for cautious expansions. The elimination of weakly
grounded cautious expansions yields a subclass of cautious expansions:
the N-grounded cautious expansions. The least N-grounded cautious
expansion is shown to be unique and the intersection of all N-grounded
cautious expansions. This is in contrast with Moore style stable
expansions. The least N-grounded cautious expansion can be
constructed iteratively as the least fixed point of a monotonic
operator. Such a construction is exceptional, since autoepistemic
expansions are nonconstructive in general. It is also shown that
cautious autoepistemic logic is decidable. A comparison is made with
some other schemes of weakened negative introspection. The given set
of examples demonstrates that the proposed negative introspection
principle is stronger than, e.g., that of the well-founded semantics.},
file = {A21.ps.Z}}
@techreport{A22,
author = {Patric R. J. Östergård and Heikki O. Hämäläinen},
title = {New Upper Bounds for Binary/Ternary Mixed Covering Codes},
type = {Research Report},
number = {A22},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = mar,
year = {1993},
pages = {33},
keywords = {Code construction, covering code, covering radius, football pool problem, mixed code, simulated annealing},
abstract = {A table of upper bounds for K_{3,2}(n_1,n_2;R), the minimum number of
codewords in a covering code with n_1 ternary coordinates,
n_2 binary coordinates, and covering radius R, in
the range n = n_1+n_2 <= 13, R <= 3, is presented.
Explicit constructions
of codes are given to prove the new bounds and verify old bounds.
These binary/ternary covering codes can be used as systems
for the football pool game.
The results include a new upper bound for the football pool problem
for 9 matches, showing that K_3(9,1) <= 1356.},
file = {A22.ps.Z}}
@techreport{A23,
author = {Johan Lilius},
title = {A Sheaf Semantics for {P}etri Nets},
type = {Research Report},
number = {A23},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = jun,
year = {1993},
pages = {13},
abstract = {The semantics of Petri Nets are discussed within the "Objects are
sheaves" paradigm. Transitions and places are represented as sheaves
and nets are represented as diagrams of sheaves. Both an interleaving
semantics, and a non-interleaving semantics are shown to arise as the
limit of the sheaf diagram representing the net. },
file = {A23.ps.Z}}
@techreport{A24,
author = {Ilkka Niemelä},
title = {Autoepistemic Logic as a Unified Basis for Nonmonotonic Reasoning},
type = {Research Report},
number = {A24},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = aug,
year = {1994},
pages = {162},
keywords = {Nonmonotonic reasoning, autoepistemic logic,
computational complexity, automated theorem proving},
abstract = {Autoepistemic logic is investigated in a general setting where
autoepistemic reasoning based on a given classical logic is studied.
The possible sets of autoepistemic conclusions from a set of premises
are defined in terms of expansions of the premises. First Moore style
expansions defined by a fixed point equation are considered and a simple
finitary characterization of expansions is developed. An alternative
definition is proposed where autoepistemic reasoning is formalized as a
sequence of introspection steps using an enumeration of sentences. The
resulting enumeration-based expansions are a proper subclass of Moore
style expansions. An even more tightly grounded subclass is captured by
considering only L-hierarchic enumerations. Finitary characterizations
of enumeration-based and L-hierarchic expansions are developed. It is
shown that autoepistemic reasoning based on Moore style,
enumeration-based, and L-hierarchic expansions is decidable if the
monotonic consequence relation given by the underlying classical logic
is decidable. In the propositional case, decision problems related to
the three classes of expansions are shown to be complete problems with
respect to the second level of the polynomial time hierarchy. Default
logic, forms of circumscription, answer set semantics of logic programs
with classical negation, nonmonotonic truth maintenance systems, and
forms of abduction are shown to be special cases of autoepistemic logic
based on L-hierarchic expansions. Hence, this variant of autoepistemic
logic offers a promising unified basis for nonmonotonic reasoning. A
decision method for autoepistemic reasoning in the general setting is
developed. The method requires as a subroutine only a theorem prover for
the underlying monotonic consequence relation.},
file = {A24.ps.Z}}
@techreport{A25,
author = {Patric R. J. Östergård},
title = {Construction Methods for Covering Codes},
type = {Research Report},
number = {A25},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = sep,
year = {1993},
pages = {25},
abstract = {A covering code in a Hamming space is a set of codewords with
the property that any word in the space is within a specified Hamming distance,
the covering radius, from at least one codeword.
In this thesis, efficient construction methods for such codes are
considered.
The constructions work, with some exceptions, for codes over alphabets
consisting of any number of symbols.
Codes over mixed alphabets are also discussed.
Most of the methods are developed in order to determine
values of K_q(n,R), the minimum number of codewords
in a q-ary code of length n and covering radius R.
Codes obtained by the constructions prove upper bounds on this function.
In many of the constructions simulated annealing, a
probabilistic optimization method, has turned out to perform very well.
Simulated annealing cannot be used to prove optimality of codes found; in that case,
the problem is viewed and solved as a set covering problem.
For larger codes, a direct approach is not generally feasible; it is shown how
good such codes can be found by combining existing codes, or by imposing
some structure on the codes. A matrix method that is
presented follows the latter principle; a code constructed by this
method consists of cosets of a linear code.
To be able to combine existing codes efficiently, it is necessary that the
codes involved can be partitioned into subcodes with certain properties;
subnorm and norm are concepts that are introduced to describe
partitions of codes.
Finally, some families of combinatorial methods are presented.},
file = {A25.ps.Z}}
@techreport{A26,
author = {Kimmo Varpaaniemi},
title = {Efficient Detection of Deadlocks in {P}etri Nets},
type = {Research Report},
number = {A26},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = oct,
year = {1993},
pages = {56},
keywords = {reachability analysis, Petri nets, deadlocks,
stubborn set method, sleep set method},
abstract = {Reachability analysis is a powerful formal method for analysis of
concurrent and distributed finite state systems. It suffers from the
state space explosion problem, however: the state space of a system
can be far too large to be completely generated. This report
considers two promising methods, Valmari's stubborn set method and
Godefroid's sleep set method, to avoid generating all of the state
space when searching for undesirable reachable terminal states, also
called deadlocks. What makes deadlocks especially interesting is the
fact that the verification of a safety property can often be reduced
to deadlock detection. The considered methods utilize the
independence of transitions to cut down on the number of states
inspected during the search. These methods have been combined by
Godefroid, Pirottin, and Wolper to further reduce the number of
inspected states.
Petri nets are a widely used model for concurrent and distributed
systems. This report shows that the stubborn set method and the sleep
set method can be combined without any of the assumptions previously
placed on the stubborn sets as far as the detection of reachable
terminal states in place/transition nets, a class of Petri nets, is
concerned. The obtained result is actually more general and gives a
sufficient condition for a method to be compatible with the sleep set
method in the detection of reachable terminal states in
place/transition nets.
The number of enabled transitions in a stubborn set can drastically
affect the number of states inspected by the stubborn set method
during the search for reachable terminal states. This work presents
some heuristics for relieving the problem.
This report emphasizes the value of dynamically stubborn sets as a
useful generalization of stubborn sets and shows some results that
improve the understanding of the stubborn set method. SEE ALSO
http://saturn.hut.fi/pub/reports/A26errata.ps.Z.},
file = {A26.ps.Z}}
@techreport{A27,
author = {Kari J. Nurmela},
title = {Constructing Combinatorial Designs by Local Search},
type = {Research Report},
number = {A27},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = nov,
year = {1993},
pages = {76},
keywords = {Combinatorial designs, combinatorial optimization, great deluge algorithm, record-to-record travel},
abstract = {In this work probabilistic search heuristics are used in search for
covering designs, packing designs and t-designs. Each covering
design gives an upper bound for C_\lambda (v,m,k,t), the minimum
size of a t-(v,m,k,\lambda ) covering design, while each packing
design gives a lower bound for D_\lambda (v,m,k,t), the maximum size
of a t-(v,m,k,\lambda) packing design, and each t-design
establishes the existence of such a design. The designs are
constructed using probabilistic combinatorial optimization methods
including simulated annealing, tabu search, threshold accepting, great
deluge algorithm and record-to-record travel. Implementation issues
of these algorithms, such as cost functions and neighborhood
structures are discussed. Comparisons of the performance of these
algorithms on some designs is carried out. Some elementary search
methods including steepest descent algorithm and random walk are
included in the comparisons. Finally, the results of the searches are
tabulated. The object class hierarchy of the program (written in C++)
and brief class descriptions are presented in the appendix.},
file = {A27.ps.Z}}
@techreport{A28,
author = {Jussi Rintanen},
title = {Priorities and Nonmonotonic Reasoning},
type = {Research Report},
number = {A28},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = dec,
year = {1993},
pages = {90},
keywords = {Nonmonotonic logics, preferences, priorities, automated reasoning},
abstract = {Many knowledge-based systems use some kind of priorities
for controlling their reasoning.
In this work, autoepistemic logic is extended with priorities.
Priorities are formalized as partial orders of formulae
that express that some formulae are preferred to others.
Priorities increase the set of conclusions that can be inferred from
a set of formulae, because the number of cases where conflicts between
defaults are left unresolved decreases.
A decision procedure for prioritized autoepistemic logic is given
in terms of a decision procedure for a classical logic on which
the prioritized autoepistemic logic is based.
The complexity of the logic is analyzed with respect to the underlying
classical logic.
When the classical logic is the propositional logic,
the decision problems of prioritized autoepistemic logic are
located on the third level of the polynomial hierarchy.
The results of this work carry to other formalisms as well because
of the existence of translations of other formalisms to autoepistemic
logic.
Possible application areas are e.g. default logic, logic programs,
deductive databases, and theories of diagnosis.
It is shown that prioritized autoepistemic logic is in the propositional case
more general than other related formalisms like preferred subtheories of
Brewka, structured theories of Ryan, and a propositional version of
Lifschitz's prioritized circumscription.
Simple polynomial-time translations of these formalisms to prioritized
autoepistemic logic are given.
Finally, it is demonstrated how automated theorem-proving in prioritized
autoepistemic logic benefits from priorities.
An algorithm for automated reasoning is given and proved correct.},
file = {A28.ps.Z}}
@techreport{A29,
author = {Tino Pyssysalo},
title = {The Modelling and Analysis of a High Speed Data Bus with Predicate/Transition Nets},
type = {Research Report},
number = {A29},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = mar,
year = {1994},
pages = {73},
keywords = {concurrent and distributed systems, protocol
verification, predicate/transition nets,
reachability analysis tools, Frame Synchronized Ring},
abstract = {In this work predicate/transition nets (Pr/T-nets) are used in the
modelling and analysis of the medium access control algorithm of a
parallel high speed data bus, Frame Synchronized Ring (FSR-bus). Two
Pr/T-net models of the bus are presented. One models the basic
operation of the control algorithm. The other is an extended model, in
which nodes can send longer frames and the reception of a frame can
fail.
The analysis of the nets is based on the reachability analysis, which
is made by a highly advanced Pr/T-net reachability analysis tool,
PROD. The state space of the reachability graph grows very fast with
respect to the number of nodes in the ring. The state space explosion
is tried to be reduced with the stubborn set and symmetry methods. The
stubborn set method reduces the number of reachable states almost 70%.
Symmetry method is not so efficient. These results show, how effective
these methods can be.
Analytical models and simulations have been used in the analysis of
the FSR-bus. With these methods it has not been possible to prove,
whether the bus can deadlock or whether the bus is fair. In this work
these properties are successfully proved with PROD.
Other important results concern the performance of the FSR-bus in
terms of waiting times of the nodes. The longest waiting path and the
situation, in which the waiting occurs, are examined with PROD.
It is found that in some circumstances a node has to wait quite long
to get access to the bus, which is undesirable in real time
applications. },
file = {A29.ps.Z}}
@techreport{A30,
author = {Johan Lilius},
title = {On the folding of Algebraic Nets},
type = {Research Report},
number = {A30},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = aug,
year = {1994},
pages = {28},
keywords = {concurrency, net theory, high-level nets},
abstract = {A folding in General Net theory is morphism that is surjective on
places and transitions. Foldings can be used to relate CE-systems to
"high-level system". In this paper we study the problem of relating
Petri Nets to non-strict High-level Nets. We give a construction that
given a morphism of Petri Nets produces an Algebraic Net that
characterises the folding in a canonical way. We also prove that
the construction is functorial. Then we show how the construction can
be made to work on Algebraic Nets directly. Finally we discuss an
application of the construction.},
file = {A30.ps.Z}}
@techreport{A31,
author = {Tomi Janhunen},
title = {Investigations on Cautious Autoepistemic Reasoning},
type = {Research Report},
number = {A31},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = dec,
year = {1994},
pages = {77},
keywords = {nonmonotonic reasoning, autoepistemic logic,
computational complexity, logic programming,
well-founded semantics},
abstract = {In this work, a formal model of knowledge representation systems,
cautious autoepistemic logic, is investigated. This logic is a
variant of autoepistemic logic which is a leading formal approach to
knowledge representation systems. Cautious autoepistemic logic has
some attractive properties that are not present in its
ancestor. Firstly, every set of premises induces a unique set of
conclusions. Moreover, this set of conclusions can be characterized
iteratively. In this work, a proof theory is developed for cautious
autoepistemic logic. The cumulativity of cautious autoepistemic
reasoning is studied with the aid of the proof theory. It turns out
that cautious autoepistemic reasoning is cumulative in restricted
cases. Computational complexity of cautious autoepistemic logic is
analyzed. Negative introspection which is the major subtask is shown
to be a complete problem on the second level of the polynomial time
hierarchy. An upper bound for the computational complexity of cautious
autoepistemic reasoning is provided. This implies that such reasoning
is in the worst case only slightly more complex than corresponding
reasoning in the original autoepistemic logic. As an application, new
model theoretic semantics for logic programs is provided in terms of
cautious autoepistemic logic. The proposed cautious semantics is
compared with the well-founded semantics. Results indicate that the
cautious model is more accurate than the well-founded model. An
alternative approach is also studied. It leads to a different model
that also subsumes the well-founded model.},
file = {A31.ps.Z}}
@techreport{A32,
author = {Kari J. Nurmela},
title = {Constructing Spherical Codes by Global Optimization Methods},
type = {Research Report},
number = {A32},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = feb,
year = {1995},
pages = {136},
keywords = {spherical codes, spherical circle-packings, global
optimization, stochastic optimization, combinatorial optimization.},
abstract = {In this work we search for spherical codes in three to five dimensions
using different global optimization methods. In three dimensions
the problem of finding optimal spherical codes is the
Tammes problem, which asks, how to pack k circular caps on
the surface of a sphere so that the diameter of the caps is as large
as possible. The optimal codes are known only when k is
small. The problem of spherical codes has close connections to sphere
packings and kissing numbers.
A variable repulsion-force based approximation of the packing
problem is used. This method has been used previously in three
dimensions and it is generalized into n dimensions in
this work. The potential energy of the point configuration is
minimized by using ordinary local optimization algorithms and
stochastic global optimization algorithms. New methods that are
used employ problem-specific heuristics with simulated annealing and
tabu search. It is shown how to reduce the number of optimization
variables by restricting the solutions to have certain symmetries.
Three new 3-dimensional codes with 43, 77 and 80 code points
are given. Most of the 4- and 5-dimensional codes in this work are
better than the previously known codes.},
file = {A32.ps.Z}}
@techreport{A33,
author = {Johan Lilius},
title = {On the Structure of High-level Nets},
type = {Research Report},
number = {A33},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = mar,
year = {1995},
pages = {136},
keywords = {net theory, category theory, algebraic
specification, linear logic, petri nets, high-level nets},
abstract = { The structure of High-level nets is studied from an algebraic and a
logical point of view using Algebraic nets as an example. First the
category of Algebraic nets is defined and the semantics given
through an unfolding construction. Other kinds of High-level net
formalisms are then presented. It is shown that nets given in these
formalisms can be transformed into equivalent Algebraic nets. Then
the semantics of nets in terms of universal constructions is
discussed. A definition of Algebraic nets in terms of structured
transition systems is proposed. The semantics of the Algebraic net
is then given as a free completion of this structured transition
system to a category. As an alternative also a sheaf semantics of
nets is examined. Here the semantics of the net arises as a limit
of a diagram of sheaves. Next Algebraic nets are characterized as
encodings of special morphisms called foldings. Each algebraic net
gives rise to a surjective morphism between Petri nets and
conversely each surjective morphism between Petri nets gives
rise to an algebraic net. Finally it is shown how Algebraic nets can
be described as sets of formulae in a typed version of intuitionistic
predicate linear logic.},
file = {A33.ps.Z}}
@techreport{A34,
author = {Jari Juopperi},
title = {{P}r{T}-net Based Analysis of Information Flow Security Nets},
type = {Research Report},
number = {A34},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = mar,
year = {1995},
pages = {87},
keywords = {security model, information flow model, security
analysis, Information Flow Security Nets,
Predicate/Transition nets, Petri nets, reachability
analysis},
abstract = {Information Flow Security Nets (IFS-nets) provide a framework for the
definition of security models. IFS-nets employ a class of low-level
Petri nets as their model of computation while the notion of security
is based on the extension of Denning's information flow model. An
inconvenient property of IFS-nets is that the direct analysis of the
nets without specialized tools is difficult. The aim of this work is
to show how the security properties of an IFS-net can be inspected
indirectly by constructing a PrT-net and by examining the reachability
graph of the constructed PrT-net. The crux of this approach is the
mapping which defines how the PrT-net corresponding to an IFS-net can
be created. It is shown that there exists an one-to-one correspondence
between the reachable markings of the IFS-net and the reachable
markings of the corresponding PrT-net. It is also shown that there
exists an one-to-one correspondence between the firing sequences of an
IFS-net and the firing sequences of the corresponding PrT-net.
Several results linking the security properties of IFS-nets to the
properties of the reachability graphs of the corresponding PrT-nets
are provided. Finally, the use of the proposed approach is illustrated
in an example where the upgrading and downgrading of data must be
properly done. The IFS-net and the corresponding PrT-net of the
example system are created. After this the security properties of the
system are analysed with the reachability analysis tool PROD.},
file = {A34.ps.Z}}
@techreport{A35,
author = {Patrik Simons},
title = {Efficient Implementation of the Stable Model Semantics for Normal Logic Programs},
type = {Research Report},
number = {A35},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = sep,
year = {1995},
pages = {66},
keywords = {stable model semantics, well-founded semantics,
logic programming, nonmonotonic reasoning, automatic theorem proving},
abstract = {The aim of this work is to develop an efficient implementation
method of the stable model semantics of logic programs with negation
using as a basis a lately proposed decision procedure for Reiter's
default logic. The problem of finding a stable model of a logic
program is NP-complete. An algorithm for computing the stable model
semantics of propositional logic programs is presented. The time
complexity of the algorithm is examined and found to be exponential in
the size of the input in the worst case. The algorithm is shown to
compute the unique stable model of a logic program with a total
well-founded model in time roughly quadratic in the size of the
program. The algorithm is compared with three other advanced
algorithms for computing the stable models semantics. It is
found to be outperforming the other algorithms mainly due to a better
technique for pruning the search space. A method for implementing the
algorithm efficiently is presented and a prototype implementation is
developed. As examples of applications of stable model
semantics, model-based diagnosis of logic circuits and the problem of
finding Hamiltonian circuits and N-colorings in undirected graphs
are encoded as propositional logic programs. These encodings are then
used as test cases in a comparison between the prototype
implementation of the algorithm presented in this work and the SLG
system, a state-of-the-art implementation of the stable model
semantics. The performance of the prototype implementation compares
favorably to that of the SLG system.},
file = {A35.ps.Z}}
@techreport{A38,
author = {Tuomas Aura},
title = {Time Processes of Time {P}etri Nets},
type = {Research Report},
number = {A38},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
address = {Espoo, Finland},
month = aug,
year = {1996},
pages = {58},
keywords = {Time Petri nets, processes, timing analysis, partial order
semantics, causality, net theory},
abstract = {
The objective of this thesis is to give time Petri nets
a partial order semantics, like the nonsequential processes
of untimed net systems.
A time process of a time Petri net is defined
as a traditionally constructed causal process with a valid timing.
This means that the
events of the process are labeled with occurrence times which must
satisfy specific validness criteria.
An efficient algorithm for checking validness of known timings is presented.
Interleavings of the time processes are defined as linearizations
of the causal partial order of events
where also the time order of events is preserved.
The relationship between firing schedules of a time Petri net and
the interleavings of the time processes of the net is shown to be
bijective.
Also, a sufficient condition is given
for when the invalidity of timings for a process can be
inferred from its initial subprocess.
An alternative characterization for the validness of timings
results in an algorithm for constructing the set of all
valid timings for a process. The set of all valid timings is presented
as sets of alternative linear constraints, which can be used
in optimization problems.
The techniques developed can be used to compute, for example,
the maximum time separation of two events in a process.
The existence of a valid timing for a given process can be
decided in NP time.},
file = {A38.ps.Z}}
@TechReport{A39,
author = {Karsten Schmidt},
title = {How to Calculate Symbolically Siphons and Traps for
some Algebraic Petri nets},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1996},
type = {Research Report},
number = {A39},
address = {Espoo, Finland},
month = aug,
pages = {40},
keywords = {petri nets, structural analysis, symbolic analysis},
abstract = {We present a symbolic approach to the calculation of
siphons and traps
for algebraic Petri nets where the color domains are
specified without
equations and with at most unary operation symbols.},
file = {A39.ps.Z}
}
@TechReport{A41,
author = {Jussi Rintanen},
title = {Lexicographic Ordering as a Basis of Priorities in Default Reasoning},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1996},
type = {Research Report},
number = {A41},
address = {Espoo, Finland},
month = dec,
pages = {vi+187},
abstract = {Nonmonotonic reasoning with priorities is investigated.
First a version of default logic with priorities is defined.
This logic extends Reiter's default logic and uses a priority mechanism
that is based on lexicographic comparison.
Questions concerning the existence of extensions, monotonicity of default
reasoning with respect to priorities, alternative interpretations
of partiality in priorities, and computational complexity of prioritized
default logic are investigated.
An algorithm for automated reasoning in prioritized default logic is presented
and proved correct.
Two translational inheritance theories are presented.
The first is based on normal default theories
and the second is based on prerequisite-free normal default theories.
Results on the connection between these translational theories and
translational theories presented in earlier work are given.
Applicability of lexicographic ordering as a basis of priorities for
default reasoning in general is discussed.},
keywords = {nonmonotonic logics, default logic, preferences, priorities, lexicographic ordering, computational complexity, inheritance networks},
file = {A41.ps.Z}
}
@TechReport{A42,
author = {Eero Lassila},
title = {Towards Optimizing Code Generation by
Domain-Sensitive Macro Expansion},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1997},
type = {Research Report},
number = {A42},
address = {Espoo, Finland},
month = jan,
pages = {100},
abstract = {},
keywords = {},
file = {A42.ps.Z}
}
@TechReport{A43,
author = {Kari J. Nurmela},
title = {Minimum-Energy Point Charge Configurations on a
Circular Disk},
institution = {Helsinki University of Technology, Digital Systems
Laboratory},
year = {1997},
type = {Research Report},
number = {A43},
address = {Espoo, Finland},
month = feb,
keywords = {point charge configurations, potential energy minimization},
abstract = {Stochastic global optimization methods are used to find
configurations of n point charges on a circular disk such that the
potential energy is minimized. Previously such optimal or
conjecturally optimal configurations have been published for n <=
23 and n = 29, 30, 50. In this work configurations for n
<= 80 are presented.
}
}
@TechReport{A44,
author = {Karsten Schmidt},
title = {Applying Reduction Rules to Algebraic Petri nets},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1997},
type = {Research Report},
number = {A44},
address = {Espoo, Finland},
month = mar,
pages = {47},
keywords = {petri nets, structural analysis, net reductions.},
abstract = {We study the specific problems concerning the
application of reduction rules to algebraic Petri
nets. In particular we express the application
conditions for the rules by means of term operations
and discuss the validity of reduction rules in
different interpretations of an algebraic
net. Thereby the discussion is rather informal, that
is we do not add formal proofs of their
correctness. Nevertheless we demonstrate the
principle feasibility of the net reduction approach
for algebraic nets.},
file = {A44.ps.Z}
}
@TechReport{A45,
author = {Keijo Heljanko},
title = {Model Checking the Branching Time Temporal Logic CTL},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1997},
type = {Research Report},
number = {A45},
address = {Espoo, Finland},
month = may,
pages = {72},
keywords = {Model checking, temporal logic, CTL, verification,
reachability analysis, state-space exploration, PROD.},
abstract = {Reachability analysis is a method for analyzing the dynamic
behavior of a concurrent system.
One way of specifying the properties that the behaviors of the system
must fulfill is to use the branching time temporal
logic CTL (Computation tree logic).
The process of checking whether the behavior of the system fulfills
the specified property is called model checking.
In this work we analyze several algorithms for CTL model
checking.
The main contribution of this report is a new model checking
algorithm with
time complexity matching the best existing algorithms, and
memory requirements which are either equal or smaller than the
existing algorithms, depending on the structure of the system
under consideration.
The algorithm has a
counterexamples and witnesses facility, which is very valuable
when trying to find the cause of incorrect behavior of the system.
The presented algorithm is also straightforward to
implement efficiently, and we have implemented the
algorithm in the PROD tool set.},
file = {A45.ps.Z}
}
@TechReport{A46,
author = {Tuomas Aura},
title = {Stateless connections},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1997},
type = {Research Report},
number = {A46},
address = {Espoo, Finland},
month = may,
pages = {27},
keywords = {
stateless connections, denial of service, cryptographic protocols,
robust design, SYN-flooding attack
},
abstract = {
We describe a transformation of stateful connections or parts of
them into stateless ones by attaching the state information to the
messages. Message authentication codes are used for checking
integrity of the state data and the connections. The stateless
server protocols created in this way are more robust against denial
of service resulting from high loads and resource exhausting attacks
than their stateful counterparts. In particular, stateless
authentication resists attacks that leave connections in a half-open
state. Examples of problems related to statefulness and solutions to
them shown for the X.509, ISAKMP, TCP and HTTP protocols.
},
file = {A46.ps.Z}
}
@TechReport{A47,
author = {Patrik Simons},
title = {Towards Constraint Satisfaction through Logic Programs and the Stable Model Semantics},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1997},
type = {Research Report},
number = {A47},
address = {Espoo, Finland},
month = aug,
pages = {49},
keywords = {stable model semantics, logic programming,
nonmonotonic reasoning, automatic theorem proving
},
abstract = {
Logic programs with the stable model semantics can be
thought of as a new paradigm for constraint satisfaction, where the
rules of a program are seen as constraints on the stable models. In
this work the paradigm is realized by developing an efficient decision
procedure for the stable model semantics that computes the stable
models of a ground logic program. A strong pruning technique based on two
deductive closures is introduced. The technique is further
strengthened by the introduction of backjumping, which
is an improvement over chronological backtracking, and lookahead, a
new pruning rule. Moreover, a strong heuristic is derived.
The two deductive closures are given linear-time implementations
that provide a linear-space implementation method for the decision
procedure. A high lower bound on the least upper bound on the complexity
of the procedure is found. In order to generalize the procedure such
that it can handle programs with variables, an algorithm for grounding
a function-free range restricted logic program that avoids generating
the whole ground instantiation is presented. Finally, an implementation of
the decision procedure is compared with a state-of-the-art
satisfiability checker using hard satisfiability problems as a test
domain.
},
file = {A47.ps.gz}
}
@TechReport{A48,
author = {Tuomas Aura},
title = {On the structure of delegation networks},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1997},
type = {Research Report},
number = {A48},
address = {Espoo, Finland},
month = dec,
pages = {53},
keywords = {
certificates, delegation network, access control,
formal model of distributed trust management.
},
abstract = {
In new distributed, key-oriented access control systems access rights
are delegated by a freely formed network of certificates. For example,
the SPKI public-key infrastructure is being designed for this kind
of distributed trust management on the Internet.
We formalize the concept of a delegation network and present a
formal semantics for the delegation of access rights with
certificates. The certificates can have multiple subjects who must
jointly use the authority. Some fundamental properties of the system
are proven, alternative techniques for authorization decisions are
compared and their equivalence is shown rigorously. In particular,
we prove that certificate reduction is a sound and complete decision
technique. We also suggest a new type of threshold certificates and
prove its properties. The formal model is used to develop efficient
algorithms for access control decisions from a database of
certificates.
},
file = {A48.ps.gz}
}
@string{a49title = "Non-Monotonic Systems: A Framework for Analyzing Semantics and Structural Properties of {NMR}"}
@TechReport{A49,
author = {Tomi Janhunen},
title = a49title,
institution = {Helsinki University of Technology,
Digital Systems Laboratory},
year = {1998},
type = {Research Report},
number = {A49},
address = {Espoo, Finland},
month = mar,
pages = {211},
keywords = {non-monotonic reasoning, semantics,
cumulativity, computational complexity},
abstract = {
Non-monotonic systems are introduced as a framework for analyzing
non-monotonic reasoning. Such systems are defined as parametrized
inference operators in a way that is compatible with Tarski's
characterization of classical reasoning. The generality of the
framework is demonstrated by presenting non-monotonic systems for
the leading non-monotonic logics such as circumscription, default
logic and autoepistemic logic.
Various translations between non-monotonic logics are studied within
the framework. Non-monotonic systems associated with the non-monotonic
logics under consideration are shown to be preserved by these
translations - including new translations between default logic and
bimodal autoepistemic logic presented in the work.
The standard semantics of non-monotonic reasoning - stable and
stationary semantics - are generalized for all non-monotonic
systems. Various properties of the semantics such as cumulativity and
computational complexity are addressed. Moreover, it is established
that the translation functions presented preserve these semantics.
Finally, a new semantics called cautious semantics is obtained as a
systematic refinement of stationary semantics. Cautious semantics is
analyzed using the methodology developed in the work. A comparison is
made with similar approaches in the literature. Applications of
cautious semantics are considered in the fields of logic programming
and consistency-based diagnosis.
},
file = {A49.ps.gz}
}
@TechReport{A50,
author = {Ilkka Niemelä (Ed.)},
title = {Proceedings of the {HeCSE} Workshop on
Emerging Technologies in Distributed Systems},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1998},
type = {Research Report},
number = {A50},
address = {Espoo, Finland},
month = mar,
pages = {46},
keywords = {
distributed systems, agents, Java, CORBA, DCOM, RMI, WAP, Internet routers
},
abstract = {This is the proceedings of a workshop on
emerging technologies in distributed systems organized by
the Helsinki Graduate School in Computer Science and
Engineering (HeCSE) held in Lammi on Jan 12--13, 1998.
The program of the workshop consisted of invited
talks, technical papers, and short poster presentations
on a variety of topics concerning open distributed
systems.
},
file = {A50abstract.html}
}
@string{a51title = "On the Stubborn Set Method in Reduced State Space Generation"}
@TechReport{A51,
author = {Kimmo Varpaaniemi},
title = a51title,
institution = {Helsinki University of Technology,
Digital Systems Laboratory},
year= {1998},
type = {Research Report},
number = {A51},
address = {Espoo, Finland},
month = may,
pages = {105},
keywords = {reachability analysis, reduced state space generation,
stubborn sets, verification of LTL formulas},
abstract = {
Reachability analysis is a powerful formal method for analysis of
concurrent and distributed finite state systems. It suffers from the
state space explosion problem, however, i.e. the state space of a
system can be far too large to be completely generated.
This thesis is concentrated on the application and theory of the stubborn
set method which is one of the methods
that try to relieve the state space explosion problem.
A central topic in the thesis is the verification of nexttime-less
LTL (linear time temporal logic) formulas. It is shown how the structure
of a formula can be utilized when there is no fairness assumption.
Another central topic is the basic problem how stubborn sets
should be computed in order to get the best possible result
w.r.t. the total time and space consumed in the
state search. An algorithm for computing
cardinality minimal or almost cardinality minimal (w.r.t. the
number of enabled transitions) stubborn sets is presented,
together with experiments that indicate that
the algorithm is worth of consideration whenever one wants to
get proper advantage of the stubborn set method.
The thesis also considers how to cut down on space consumption
in the stubborn set method and how well the method
can be combined with another reduction technique,
the sleep set method.
},
file = {A51.ps.gz}
}
@TechReport{A52,
author = {Ilkka Niemelä and Torsten Schaub (Eds.)},
title = {Proceedings of the Workshop on
Computational Aspects of Nonmonotonic Reasoning},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1998},
type = {Research Report},
number = {A52},
address = {Espoo, Finland},
month = may,
pages = {46},
keywords = {
nonmonotonic reasoning, default logic, circumscription, logic programs, abduction, diagnosis
},
abstract = {
This is the proceedings of a workshop on computational aspects of
nonmonotonic reasoning which was organized as one of the five special
workshops at the Seventh International Workshop on Nonmonotonic
Reasoning held in Trento, Italy, May 30--June~1, 1998 in
conjunction with the Sixth International Conference on Principles of
Knowledge Representation and Reasoning (KR'98). The program of the
workshop consisted of 10 papers accepted for presentation, a panel and
system demonstrations.
},
file = {A52abstract.html}
}
@techreport{A53,
author = {Stefan Rönn},
title = {Semantics of Semaphores},
institution = {Helsinki University of Technology, Digital Systems Laboratory},
year = {1998},
type = {Research Report},
number = {A53},
address = {Espoo, Finland},
pages = {10},
keywords = {semaphores, process synchronization, mutual exclusion, weakest preconditions},
abstract = {
We present a formal definition of semaphores using weakest preconditions. With the definition we prove the mutual exclusion
algorithm and show that the semaphore axioms given by Martin and de~Snepscheut are implied by the invariant relation of the proof.
We further demonstrate how a general k-semaphore can be realised with the help of a split binary semaphore. To this end, we
introduce a program construct that facilitates the usage of the split binary semaphore.},
file = {A53abstract.html}
}
@techreport{A54,
author = {Antti Huima},
title = {Analysis of Cryptographic Protocols via Symbolic State Space Enumeration},
institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
month = aug,
year = {1999},
type = {Research Report},
number = {A54},
address = {Espoo, Finland},
ADDLATERpages = {},
ADDLATERkeywords = {},
ADDLATERabstract = {
},
file = {A54abstract.html}
}
@techreport{A55,
author = {Tommi Syrjänen},
title = {A Rule-Based Formal Model For Software Configuration},
institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
month = dec,
year = {1999},
type = {Research Report},
number = {A55},
address = {Espoo, Finland},
pages = { 74},
keywords = {Configuration management, stable model semantics, logic
programming, Debian, Linux, diagnostics},
abstract = {In this work we examine the software configuration management problem.
We give a short introduction to the current state of the art and
present a declarative rule-based formal language for representation of
configuration knowledge. As a novel feature, the rule language allows
finite existential quantification over the configuration components.
We show a translation from the rule language to normal logic programs
with stable model semantics. As a case study we examine the
configuration management problem for the Debian GNU/Linux system which
consists of over 2000 distinct software packages. We examine the
current practice to identify the main components of the problem and
present a way to formalize them using the rule language. We construct
two formal models: one for finding valid configurations and one for
diagnosing unsatisfiable user requirements. We show that the decision
problem for the configuration model is NP-complete. We present a
translator that reads a high-level description of the Debian
configuration system and produces the corresponding set of rules. We
evaluate the configuration model by using actual data from Debian
version 2.1 and a set of randomly generated user requirements. The
evaluation shows that the model is computationally feasible.},
file = {A55abstract.html}
}
@techreport{A56,
author = {Keijo Heljanko},
title = {Deadlock and Reachability Checking with Finite Complete Prefixes},
institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
month = dec,
year = {1999},
type = {Research Report},
number = {A56},
address = {Espoo, Finland},
pages = {70},
keywords = {Computer aided verification, Petri nets,
finite complete prefixes, net unfoldings, model checking, deadlocks,
reachability, logic programs, stable model semantics, computational
complexity
},
abstract = {
McMillan has presented a verification method for finite-state Petri
nets based on finite complete prefixes of net unfoldings.
Computational complexity of using finite complete prefixes as a
symbolic representation of the state space is discussed. In addition
a novel way of deadlock and reachability checking using the finite
complete prefix approach is devised.
More specifically, the main contributions are:
(i) The possible extensions calculation subroutine of the prefix
generation algorithm is proved NP-complete.
(ii) Model checking a fixed size CTL formula with finite complete
prefixes is proved PSPACE-complete.
(iii) The translations of the problems of deadlock and reachability
checking using finite complete prefixes into the problem of finding a
stable model of a logic program are devised.
(iv) The implementation of the above mentioned translations in the
{\tt mcsmodels} tool is presented, with experimental results
supporting the feasibility of the approach.
The implementation combines the prefix generator of the PEP-tool, the
translations, and an implementation of a constraint-based logic
programming framework, the {\tt smodels} system. The experiments show
that the proposed approach is quite competitive when compared to
previous prefix based deadlock checking algorithms.
},
file = {A56abstract.html}
}
@techreport{A57,
author = {Junttila, Tommi},
title = {Detecting and Exploiting Data Type Symmetries of
Algebraic System Nets during Reachability Analysis},
institution = {Helsinki University of Technology,
Laboratory for Theoretical Computer Science},
month = dec,
year = {1999},
type = {Research Report},
number = {A57},
address = {Espoo, Finland},
pages = {67},
keywords = {Symmetry, reachability analysis, Petri nets,
algebraic system nets},
abstract = {
The symmetry reduction method is a technique designed
to alleviate the combinatorial state space explosion problem
by exploiting the symmetries of state spaces.
This work describes a way how state space symmetries of a high-level
Petri net formalism, algebraic system nets,
can be detected and exploited during the reachability analysis.
The main idea is that permuting the domains of data types used in nets
produces corresponding permutations to the state space level.
As the main result a sufficient condition is defined for data type domain
permutations ensuring that the produced state space permutations are
actually automorphisms i.e.~symmetries.
Since verification of the condition is shown to be a co-NP-complete problem,
an approximation rule for the condition is also given.
Use of the developed theory is illustrated by defining
the class of extended well-formed nets and
by examining data type symmetries of such nets.
It is shown that checking the symmetricity of two markings of a net
in this class is equivalent to checking whether two graphs are isomorphic.
},
file = {A57abstract.html}
}
@techreport{A58,
author = {Simons, Patrik},
title = {Extending and Implementing the Stable Model Semantics},
institution = {Helsinki University of Technology,
Laboratory for Theoretical Computer Science},
month = apr,
year = {2000},
type = {Research Report},
number = {A58},
address = {Espoo, Finland},
pages = {91},
keywords = {Stable model semantics, logic programming, nonmonotonic reasoning, automatic theorem proving},
abstract = {
An algorithm for computing the stable model semantics of logic
programs is developed. It is shown that one can extend the semantics
and the algorithm to handle new and more expressive types of rules.
Emphasis is placed on the use of efficient implementation
techniques. In particular, an implementation of lookahead that
safely avoids testing every literal for failure and that makes the
use of lookahead feasible is presented. In addition, a good
heuristic is derived from the principle that the search space should
be minimized.
Due to the lack of competitive algorithms and implementations for
the computation of stable models, the system is compared with three
satisfiability solvers. This shows that the heuristic can be
improved by breaking ties, but leaves open the question of how to
break them. It also demonstrates that the more expressive rules of
the stable model semantics make the semantics clearly preferable
over propositional logic when a problem has a more compact logic
program representation. Conjunctive normal form representations are
never more compact than logic program ones.
},
file = {A58abstract.html}
}
@techreport{A59,
author = {Junttila, Tommi},
title = {Computational Complexity of the Place/Transition-Net Symmetry
Reduction Method},
institution = {Helsinki University of Technology,
Laboratory for Theoretical Computer Science},
month = apr,
year = {2000},
type = {Research Report},
number = {A59},
address = {Espoo, Finland},
pages = {17},
keywords = {Petri nets, symmetry},
abstract = {
Computational complexity of the sub-tasks appearing in the
symmetry reduction method for Place/Transition-nets is studied.
The first task of finding the automorphisms (symmetries)
of a net is shown to be polynomial time many-one equivalent
to the problem of finding the automorphisms of a graph.
The problem of deciding whether two markings are symmetric is shown to be
equivalent to the graph isomorphism problem.
Surprisingly, this remains to be the case even if the generators
for the automorphism group of the net are known.
The problem of constructing the lexicographically greatest marking
symmetric to a given marking (a canonical representative for the marking)
is classified to belong to the lower levels of the polynomial hierarchy,
namely to somewhere between FP^NP[log n] and FP^NP.
It is also discussed how the self-symmetries of a marking can be
exploited.
Calculation of such symmetries is classified to be as hard as
computing graph automorphism groups.
Furthermore,
the coverability version of testing marking symmetricity is shown to
be an NP-complete problem.
It is shown that unfortunately canonical representative markings and
the symmetric coverability problem cannot be combined in a straightforward
way.
}
}
@techreport{A60,
author = {Javier Esparza and Keijo Heljanko},
title = {A New Unfolding Approach to {LTL} Model Checking},
institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
month = apr,
year = {2000},
type = {Research Report},
number = {A60},
address = {Espoo, Finland},
pages = {32},
keywords = {Net unfoldings, model checking, tableau
systems, LTL, Petri nets},
abstract = {
A new unfolding approach to LTL model checking
is presented, in which the model checking problem can be solved by
direct inspection of a certain finite prefix. The techniques
presented so far required to run an elaborate algorithm on the prefix.
},
file = {A60abstract.html}
}
@TechReport{A61,
author = {Tuomas Aura and Carl Ellison},
title = {Privacy and accountability in certificate systems},
institution = {Helsinki University of Technology,
Laboratory for Theoretical Computer Science},
year = 2000,
number = {A61},
type = {Research Report},
address = {Espoo, Finland},
pages = {17},
month = apr,
abstract = {
Discretionary access right management on the Internet and in other
distributed communications systems is increasingly based on public-key
identity and authorization certificates. The certificates pose a
threat to privacy because they identify the owners and reveal the
authorization relations between them. This paper overviews the privacy
concerns and describes techniques for minimizing the amount of
confidential information leaked about individuals and organizations.
We also show how identity escrow certificates can ensure individual
accountability without identity authentication. All the techniques can
be implemented with SPKI certificates.
},
keywords = {privacy, anonymity, PKI, certificates, SPKI}
}
@techreport{A62,
author = {Kari J. Nurmela and Patric R. J. Östergård},
title = {Covering a Square with up to 30 Equal Circles},
institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
month = jun,
year = {2000},
type = {Research Report},
number = {A62},
address = {Espoo, Finland},
pages = {14},
keywords = {circle covering, equidistant graph, square},
abstract = {
A computational method for finding good coverings of a square with
equal circles is presented. The algorithm uses a quasi-Newton method
with BFGS secant update to minimize the uncovered area by moving the
circles. The radius of the circles is further adapted to find
locally optimal coverings, and the algorithm is applied repeatedly
to random initial configurations. The structures of the coverings
are determined and the coordinates of each circle are calculated
with high precision using a mathematical model for an idealized
physical structure consisting of tensioned bars and frictionless pin
joints. Best found coverings of a square with up to 30 circles are
displayed, 17 of which are new or improve on earlier published
coverings.
},
file = {A62abstract.html}
}
@techreport{A63,
author = {Nisse Husberg and Tomi Janhunen and Ilkka Niemelä (Eds.)},
title = {Leksa Notes in Computer Science},
institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
month = oct,
year = {2000},
type = {Research Report},
number = {A63},
address = {Espoo, Finland},
pages = {140},
keywords = {},
abstract = {
October 31, 2000, is a memorable day in the history of
the Laboratory for Theoretical Computer Science: the day of retirement
of the founder and the first Head of the Laboratory, professor Leo
``Leksa'' Ojala. To honour the occassion, this festscrift has been
prepared as a collection of articles from Leo's former and present
students. It is cordially dedicated to Leo for all his efforts to
educate us during the last 30 years.},
file = {A63abstract.html}
}
@techreport{A64,
author = {Tuomas Aura},
title = {Authorization and availability -
aspects of open network security},
institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
month = nov,
year = {2000},
type = {Research Report},
number = {A64},
address = {Espoo, Finland},
pages = {42},
keywords = {open network security, authorization certificates,
cryptographic protocols, denial of service},
abstract = {
The world is becoming increasingly dependent on secure, reliable
access to services on the Internet and in other open communications
networks. Since the administration and authority on these networks
are completely distributed, it is not possible to set or enforce
global security policies. While security and confidentiality of data
are still significant concerns, access control and resistance to
denial-of-service (DOS) attacks have become at least as significant
security goals. Traditional methods for access-right management and
resource allocation, which were defined for centrally administered
systems, are not applicable on the open networks. Consequently, new
techniques for access control and DOS prevention are needed.
This dissertation addresses several aspects of the security of open,
distributed systems: decentralized access control, design of
key-establishment protocols, and denial-of-service resistance. We
suggest technical solutions both for extending the scope of
applications that can securely be run on the networks and for
improving the reliability of the underlying infrastructure for all
applications.
We define a formal model of key-oriented access control and use this
model to develop algorithms for access-control decisions from a
certificate database. We survey privacy protection in public-key
infrastructures, introduce a new kind of threshold certificate, and
present novel certificate-based solutions for access control between
mutually distrusting software packages on intelligent-network
routers and for software license management with smartcards. We also
describe novel design principles for cryptographic protocols to
improve their robustness against common replay attacks at a low cost
and to protect on-line services against denial-of-service attacks
that attempt to exhaust server memory and computational resources.
Additionally, we develop a method for analyzing the vulnerability of
network topologies to denial of service by the destruction of
communications links.
Throughout, the emphasis is on security issues critical for the
commercial and private use of the Internet and other open
communications systems where mutually distrusting entities must share
resources and co-operate.
}
}
@techreport{A65,
author = {Harri Haanpää},
title = {Computational Methods for {R}amsey Numbers},
institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
month = nov,
year = {2000},
type = {Research Report},
number = {A65},
address = {Espoo, Finland},
pages = {50},
keywords = {{R}amsey numbers, graph theory, tabu search},
abstract = {
The Ramsey number R(k,l) is the least integer n such that all graphs on n or
more vertices contain a clique of k vertices or an independent set of l
vertices as a subgraph. In this work we investigate computational methods
for finding lower bounds for Ramsey numbers. Some constructions of lower
bounds for multicolor Ramsey numbers, a generalization of Ramsey numbers,
are also considered.
Several methods that have been used for finding lower bounds for Ramsey
numbers are surveyed. Specifically, constructions which correspond to the
structure of finite fields are examined, using local search methods is
discussed, and using symmetrical graph colorings are investigated. The main
emphasis in this work is on using local search methods for finding lower
bounds for Ramsey numbers. By a construction found by using tabu search, we show
that R(5,9) is greater than 120.
Evaluating Ramsey numbers is very difficult due to the combinatorial nature
of the problem, and exact values are only known for the smallest values of
the parameters. Some recent results concerning the computational complexity
of related problems are summarized.
}
}
@techreport{A66,
author = {Heikki Tauriainen},
title = {Automated Testing of {B}\"uchi Automata Translators for Linear
Temporal Logic},
institution = {Helsinki University of Technology, Laboratory for Theoretical
Computer Science},
month = dec,
year = {2000},
type = {Research Report},
number = {A66},
address = {Espoo, Finland},
pages = {86},
keywords = {Model checking, linear temporal logic, {B}\"uchi automata,
algorithm testing},
abstract = {
The formal verification of finite-state reactive and concurrent
systems against temporal logical requirements can be done by
model checking, which has the advantage of being well suited for
automation. However, reasoning about the correctness of systems
using automated techniques places high demands for ensuring the
reliability of the model checking tools themselves.
This work describes testing methods for detecting implementation
errors in a specific class of algorithms required in the
automata-theoretic model checking procedure for propositional linear
temporal logic (LTL). These algorithms are used for translating temporal
requirements into B\"uchi automata, which are used in the model checking
process. Most of the test methods can be easily integrated into an automatic
testing tool for translation algorithm implementations. Experimental results
using a randomized tool for testing the correctness of several
implementations included in real model checkers are presented. This testing
has proved to be an effective method for finding implementation errors in the
translators.
This work also presents a restricted LTL model checking algorithm designed to
work in a very simple subclass of systems, on which the analysis of test
failures is based. This algorithm can be used to automatically confirm the
incorrectness of a translation algorithm implementation.
}
}
@techreport{A67,
author = {Timo Latvala},
title = {Model Checking Linear Temporal Logic Properties of Petri Nets with
Fairness Constraints},
institution = {Helsinki University of Technology, Laboratory for Theoretical
Computer Science},
month = jan,
year = {2001},
type = {Research Report},
number = {A67},
address = {Espoo, Finland},
pages = {40+iii},
keywords = {Computer aided verification, Petri nets,
model checking, fairness, Streett automata, counterexamples},
abstract = {
Verification of liveness properties of systems requires in many cases
fairness constraints to be imposed on the system. In the
context of modeling and analysis with Petri nets, fairness constraints
have been defined but the results have not been extended
to model checking.
In this work Coloured Petri nets are extended with fairness constraints
on the transitions. The semantics of the fairness constraints are defined
with a fair Kripke structure. Model checking linear temporal logic (LTL)
properties of the Petri net is facilitated
by introducing a new LTL model checking procedure. The procedure employs
Streett automata to cope with the fairness constraints
efficiently. Also, new algorithms for the emptiness checking problem of
Streett automata and counterexample generation are presented.
The new procedure has been implemented in the M{\footnotesize ARIA} analyzer.
Some experiments are performed to test the implementation and compare
it with other ways of coping with fairness constraints. The results
show that the procedure scales well when compared to alternative approaches.
}
}
@techreport{A68,
author = {Javier Esparza and Keijo Heljanko},
title = {Implementing {LTL} Model Checking with Net Unfoldings},
institution = {Helsinki University of Technology, Laboratory for Theoretical
Computer Science},
month = mar,
year = {2001},
type = {Research Report},
number = {A68},
address = {Espoo, Finland},
pages = {29},
keywords = {Net unfoldings, model checking, tableau
systems, LTL, Petri nets},
abstract = {We report on an implementation of the unfolding approach
to model-checking LTL-X recently presented by the authors.
Contrary to that work, we consider an state-based version
of LTL-X, which is more used in practice. We improve on the
checking algorithm; the new version allows to reuse
code much more efficiently. We present results on a set of
case studies.
},
file = {A68abstract.html}
}
@techreport{A69,
author = {Marko Mäkelä},
title = {A Reachability Analyser for Algebraic System Nets},
institution = {Helsinki University of Technology, Laboratory for Theoretical
Computer Science},
month = jun,
year = {2001},
type = {Research Report},
number = {A69},
address = {Espoo, Finland},
pages = {85},
keywords = {Many-sorted algebras, algebraic system nets, distributed
systems, reachability analysis},
abstract = {Concurrent and distributed systems are difficult to manage
without using formal analysis methods. The user of formal methods
has to find a balance between expressive power and tractability. A
formalism with small expressive power may not suit well to describing
all real-life systems, but on the other hand, performing exhaustive
reachability analysis on a system defined using a highly expressive
formalism may be an unsolvable problem.
Using extended many-sorted algebras, this work defines the data
type system and the set of algebraic operations that the author has
implemented in a reachability analyser intended for modelling
computer software based communications protocols. The work also
introduces the modelling formalism of the analyser, algebraic system
nets.
The report discusses some implementation details of the
reachability analyser both from a theoretical and from a software
technology point of view. Finally, the work shows how some
constructs difficult for other tools can be modelled using the new
formalism, and describes how different programming language
constructs can be transformed to parts of a model by a semi-automated
compiler.},
file = {A69abstract.html}
}
@techreport{A70,
author = {Petteri Kaski},
title = {Isomorph-Free Exhaustive Generation of Combinatorial Designs},
institution = {Helsinki University of Technology, Laboratory for Theoretical
Computer Science},
month = dec,
year = {2001},
type = {Research Report},
number = {A70},
address = {Espoo, Finland},
pages = {125},
keywords ={Balanced incomplete block design, error-correcting code,
exhaustive search, group action, isomorph rejection, orderly algorithm,
resolution, resolvable design},
abstract = {This thesis investigates algorithmic isomorph-free
exhaustive generation of balanced incomplete block designs (BIBDs),
resolvable balanced incomplete block designs (RBIBDs), and the
corresponding resolutions. In particular, three algorithms for
isomorph-free exhaustive generation of $(v,k,\lambda)$-BIBDs and
resolutions are described and applied to settle existence and
classification problems.
The first algorithm generates BIBDs point by point using an orderly
algorithm in combination with a maximum clique algorithm. The second
and third algorithm generate resolutions of BIBDs by utilizing a
correspondence between resolutions and certain optimal $q$-ary
error-correcting codes. The second algorithm generates the
corresponding codes codeword by codeword, and is analogous in
structure to the first algorithm. The third algorithm generates codes
coordinate by coordinate, and is based on the recent isomorph-free
exhaustive generation framework of Brendan McKay.
The main result of this thesis is a proof of nonexistence for a
(15,5,4) RBIBD by exhaustive computer search. Other new
classification results include the classifications of the $(13,6,5)$-
and $(14,7,6)$-BIBDs and the $(16,4,2)$-, $(14,7,12)$-, and
$(24,12,11)$-RBIBDs together with their resolutions, which correspond
to classifications of the $(10,16,8)_4$, $(26,14,14)_2$, and
$(23,24,12)_2$ error-correcting $(n,M,d)_q$-codes, respectively.
Additionally, a number of earlier classification results are
corroborated.},
file = {A70abstract.html}
}
@techreport{A71,
author = {Keijo Heljanko},
title = {Combining Symbolic and Partial Order Methods
for Model Checking 1-Safe Petri Nets},
institution = {Helsinki University of Technology, Laboratory for Theoretical
Computer Science},
month = feb,
year = {2002},
type = {Research Report},
number = {A71},
address = {Espoo, Finland},
pages = {55+112},
keywords = {Verification, model checking, Petri nets, complete finite
prefixes, partial order methods, symbolic methods, bounded model checking},
abstract = {In this work, methods are presented for model checking
finite state asynchronous systems, more specifically 1-safe Petri
nets, with the aim of alleviating the state explosion
problem. Symbolic model checking techniques are used, combined with
two partial order semantics known as net unfoldings and processes.
We start with net unfoldings and study deadlock and reachability
checking problems, using complete finite prefixes of net unfoldings
introduced by McMillan. It is shown how these problems can be
translated compactly into the problem of finding a stable model of a
logic program. This combined with an efficient procedure for finding
stable models of a logic program, the Smodels system, provides the
basis of a prefix based model checking procedure for deadlock and
reachability properties, which is competitive with previously
published procedures using prefixes.
This work shows that, if the only thing one can assume from a prefix
is that it is complete, nested reachability properties are relatively
hard. Namely, for several widely used temporal logics which can
express a violation of a certain fixed safety property, model checking
is PSPACE-complete in the size of the complete finite prefix.
A model checking approach is devised for the linear temporal logic
LTL-X using complete finite prefixes. The approach makes the complete
finite prefix generation formula specific, and the prefix completeness
notion application specific. Using these ideas, an LTL-X model checker
has been implemented as a variant of a prefix generation algorithm.
The use of bounded model checking for asynchronous systems is
studied. A method to express the process semantics of a 1-safe Petri
net in symbolic form as a set of satisfying truth assignments of a
constrained Boolean circuit is presented. In the experiments the BCSat
system is used as a circuit satisfiability checker. Another
contribution employs logic programs with stable model semantics to
develop a new linear size bounded LTL-X model checking translation
that can be used with step semantics of 1-safe Petri nets.},
file = {A71abstract.html}
}