%A Marko Rauhamaa
%T A comparative study of the methods for efficient reachability analysis
%R Research Report A14
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D September 1990
%K reachability analysis, distributed systems, Petrisystems
%X 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.
%X A14.ps.Z

%A Johan Lilius
%T On the compositionality and analysis of algebraic high-level nets
%R Research Report A16
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D October 1991
%K net theory, category theory, algebraic specification,linear logic, Petri
  nets, high-level nets, compositionality
%X 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.
%X A16.ps.Z

%A Patric R. J. Östergård
%T Constructions of mixed covering codes
%R Research Report A18
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D December 1991
%K Covering code, covering radius, football pool problem,mixed code, simulated
  annealing
%X 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.
%X A18.ps.Z

%A Jussi Rintanen
%T Stratification and tractability in nonmonotonic reasoning
%R Research Report A20
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D November 1992
%K nonmonotonic reasoning, autoepistemic logic, tractability, stratification
%X 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.
%X A20.ps.Z

%A Tomi Janhunen
%T Weakened negative introspection in autoepistemic reasoning
%R Research Report A21
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D February 1993
%K autoepistemic logic, nonmonotonic reasoning, weakened negative introspection
%X 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.
%X A21.ps.Z

%A Patric R. J. Östergård and Heikki O. Hämäläinen
%T New upper bounds for binary/ternary mixed covering codes
%R Research Report A22
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D March 1993
%K Code construction, covering code, covering radius, football pool problem,
  mixed code, simulated annealing
%X 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.
%X A22.ps.Z

%A Johan Lilius
%T A sheaf semantics for Petri nets
%R Research Report A23
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D June 1993
%K
%X 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.
%X A23.ps.Z

%A Ilkka Niemelä
%T Autoepistemic logic as a unified basis for nonmonotonic reasoning
%R Research Report A24
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D August 1994
%K Nonmonotonic reasoning, autoepistemic logic, computational complexity,
  automated theorem proving
%X 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.
%X A24.ps.Z

%A Patric R. J. Östergård
%T Construction methods for covering codes
%R Research Report A25
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D September 1993
%K
%X 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.
%X A25.ps.Z

%A Kimmo Varpaaniemi
%T Efficient detection of deadlocks in Petri nets
%R Research Report A26
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D October 1993
%K reachability analysis, Petri nets, deadlocks, stubborn set method, sleep set
  method
%X 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.
%X A26.ps.Z

%A Kari J. Nurmela
%T Constructing combinatorial designs by local search
%R Research Report A27
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D November 1993
%K Combinatorial designs, combinatorial optimization, great deluge algorithm,
  record-to-record travel
%X 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.
%X A27.ps.Z

%A Jussi Rintanen
%T Priorities and nonmonotonic reasoning
%R Research Report A28
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D December 1993
%K Nonmonotonic logics, preferences, priorities, automated reasoning
%X 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.
%X A28.ps.Z

%A Tino Pyssysalo
%T The modelling and analysis of a high speed data bus with
  predicate/transition nets
%R Research Report A29
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D March 1994
%K concurrent and distributed systems, protocol verification,
  predicate/transition nets, reachability analysis tools, Frame Synchronized
  Ring
%X 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.
%X A29.ps.Z

%A Johan Lilius
%T On the folding of algebraic nets
%R Research Report A30
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D August 1994
%K concurrency, net theory, high-level nets
%X 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.
%X A30.ps.Z

%A Tomi Janhunen
%T Investigations on cautious autoepistemic reasoning
%R Research Report A31
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D December 1994
%K nonmonotonic reasoning, autoepistemic logic, computational complexity, logic
  programming, well-founded semantics
%X 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.
%X A31.ps.Z

%A Kari J. Nurmela
%T Constructing spherical codes by global optimization methods
%R Research Report A32
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D February 1995
%K spherical codes, spherical circle-packings, global optimization, stochastic
  optimization, combinatorial optimization.
%X 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.
%X A32.ps.Z

%A Johan Lilius
%T On the structure of high-level nets
%R Research Report A33
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D March 1995
%K net theory, category theory, algebraic specification, linear logic, petri
  nets, high-level nets
%X 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.
%X A33.ps.Z

%A Jari Juopperi
%T PrT-net based analysis of information flow security nets
%R Research Report A34
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D March 1995
%K security model, information flow model, security analysis, Information Flow
  Security Nets, Predicate/Transition nets, Petri nets, reachability analysis
%X 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.
%X A34.ps.Z

%A Patrik Simons
%T Efficient implementation of the stable model semantics for normal logic
  programs
%R Research Report A35
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D September 1995
%K stable model semantics, well-founded semantics, logic programming,
  nonmonotonic reasoning, automatic theorem proving
%X 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.
%X A35.ps.Z

%A Tuomas Aura
%T Time processes of time Petri nets
%R Research Report A38
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D August 1996
%K Time Petri nets, processes, timing analysis, partial order semantics,
  causality, net theory
%X 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.
%X A38.ps.Z

%A Karsten Schmidt
%T How to calculate symbolically siphons and traps for some algebraic petri
  nets
%R Research Report A39
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D August 1996
%K petri nets, structural analysis, symbolic analysis
%X 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.
%X A39.ps.Z

%A Jussi Rintanen
%T Lexicographic ordering as a basis of priorities in default reasoning
%R Research Report A41
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D December 1996
%K nonmonotonic logics, default logic, preferences, priorities, lexicographic
  ordering, computational complexity, inheritance networks
%X 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.
%X A41.ps.Z

%A Eero Lassila
%T Towards optimizing code generation by domain-sensitive macro expansion
%R Research Report A42
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D January 1997
%K
%X
%X A42.ps.Z

%A Kari J. Nurmela
%T Minimum-energy point charge configurations on a circular disk
%R Research Report A43
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D February 1997
%K point charge configurations, potential energy minimization
%X 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.
%X

%A Karsten Schmidt
%T Applying reduction rules to algebraic petri nets
%R Research Report A44
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D March 1997
%K petri nets, structural analysis, net reductions.
%X 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.
%X A44.ps.Z

%A Keijo Heljanko
%T Model checking the branching time temporal logic ctl
%R Research Report A45
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D May 1997
%K Model checking, temporal logic, CTL, verification, reachability analysis,
  state-space exploration, PROD.
%X 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.
%X A45.ps.Z

%A Tuomas Aura
%T Stateless connections
%R Research Report A46
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D May 1997
%K stateless connections, denial of service, cryptographic protocols, robust
  design, SYN-flooding attack
%X 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.
%X A46.ps.Z

%A Patrik Simons
%T Towards constraint satisfaction through logic programs and the stable model
  semantics
%R Research Report A47
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D August 1997
%K stable model semantics, logic programming, nonmonotonic reasoning, automatic
  theorem proving
%X 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.
%X A47.ps.gz

%A Tuomas Aura
%T On the structure of delegation networks
%R Research Report A48
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D December 1997
%K certificates, delegation network, access control, formal model of
  distributed trust management.
%X 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.
%X A48.ps.gz

%A Tomi Janhunen
%T Non-monotonic systems: A framework for analyzing semantics and structural
  properties of NMR
%R Research Report A49
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D March 1998
%K non-monotonic reasoning, semantics, cumulativity, computational complexity
%X 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.
%X A49.ps.gz

%A Ilkka Niemelä (Ed.)
%T Proceedings of the HeCSE workshop on emerging technologies in distributed
  systems
%R Research Report A50
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D March 1998
%K distributed systems, agents, Java, CORBA, DCOM, RMI, WAP, Internet routers
%X 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.
%X A50abstract.html

%A Kimmo Varpaaniemi
%T On the stubborn set method in reduced state space generation
%R Research Report A51
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D May 1998
%K reachability analysis, reduced state space generation, stubborn sets,
  verification of LTL formulas
%X 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.
%X A51.ps.gz

%A Ilkka Niemelä and Torsten Schaub (Eds.)
%T Proceedings of the workshop on computational aspects of nonmonotonic
  reasoning
%R Research Report A52
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D May 1998
%K nonmonotonic reasoning, default logic, circumscription, logic programs,
  abduction, diagnosis
%X 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.
%X A52abstract.html

%A Stefan Rönn
%T Semantics of semaphores
%R Research Report A53
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D 1998
%K semaphores, process synchronization, mutual exclusion, weakest preconditions
%X 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.
%X A53abstract.html

%A Antti Huima
%T Analysis of cryptographic protocols via symbolic state space enumeration
%R Research Report A54
%I Helsinki University of Technology, Laboratory for Theoretical Computer
  Science
%C Espoo, Finland
%D August 1999
%K
%X
%X A54abstract.html

%A Tommi Syrjänen
%T A rule-based formal model for software configuration
%R Research Report A55
%I Helsinki University of Technology, Laboratory for Theoretical Computer
  Science
%C Espoo, Finland
%D December 1999
%K Configuration management, stable model semantics, logic programming, Debian,
  Linux, diagnostics
%X 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.
%X A55abstract.html

%A Keijo Heljanko
%T Deadlock and reachability checking with finite complete prefixes
%R Research Report A56
%I Helsinki University of Technology, Laboratory for Theoretical Computer
  Science
%C Espoo, Finland
%D December 1999
%K Computer aided verification, Petri nets, finite complete prefixes, net
  unfoldings, model checking, deadlocks, reachability, logic programs, stable
  model semantics, computational complexity
%X 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.
%X A56abstract.html

%A Tommi Junttila
