%A Kari J. Nurmela and Patric R. J. Östergård
%T Constructing covering designs by simulated annealing
%R Technical Report B10
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D January 1993
%K Combinatorial optimization, covering design, simulated annealing
%X A t-(v,m,k,\lambda) covering design is a pair (X,A), where X is a set of v
  elements (called points) and A is a multiset of k-subsets of X (called
  blocks), such that every m-subset of X intersects at least \lambda members of
  A in at least t points. It is required that v >= k >= t and v >= m >= t. Such
  a covering design gives an upper bound on C_\lambda(v,m,k,t), the number of
  blocks in a minimal t-(v,m,k,\lambda ) covering design. In this work it is
  shown how simulated annealing can be used in searches for covering designs. A
  cost function and a neighborhood structure needed by the algorithm are
  presented. The space complexity of the implementation and the time complexity
  of the cost change calculation are also given. Several options to increase
  the performance of the algorithm are tested. A performance comparison to
  local optimization is carried out. Finally, a description how to obtain,
  compile and use the computer program cover, which has been developed during
  the research, is given.
%X B10.ps.Z

%A Kimmo Varpaaniemi
%T On computing symmetries and stubborn sets
%R Technical Report B12
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D April 1994
%K reachability analysis, symmetry method, stubborn set method, CFFD-semantics,
  place/transition nets
%X In this report, we consider two promising methods for alleviating the state
  space explosion problem in reachability analysis: the symmetry method and the
  stubborn set method. We concentrate on the computation of symmetries and
  stubborn sets. The new algorithms presented in this report help us to save
  time and space in the symmetry method and to avoid inspecting redundant
  states in the so called CFFD-preserving stubborn set method. SEE ALSO
  http://saturn.hut.fi/pub/reports/B12errata.ps.Z.
%X B12.ps.Z

%A Kimmo Varpaaniemi, Jaakko Halme, Kari Hiekkanen, and Tino Pyssysalo
%T PROD reference manual
%R Technical Report B13
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D August 1995
%K Pr/T-nets, on-the-fly verification, stubborn sets
%X PROD is a Pr/T-net reachability analysis tool that supports on-the-fly
  verification of linear time temporal properties with the aid of the stubborn
  set method. Branching time temporal properties can be verified, too. SEE ALSO
  http://saturn.hut.fi/pub/reports/B13errata.ps.Z and
  http://saturn.hut.fi/pub/reports/B13changes.ps.Z.
%X B13.ps.Z

%A Tuomas Aura
%T Modelling the Needham-Schröder authentication protocol with high level Petri
  nets
%R Technical Report B14
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D September 1995
%K Cryptographic protocols, Needham-Schröder, formal model, Petri nets, Pr/T
  nets, PROD
%X In this paper, security of the Needham-Schröder key distribution protocol is
  modelled and analyzed with predicate/transition nets, and along that, a
  methodology for modelling cryptographic protocols with high level Petri nets
  is developed. The main goal is clarity of the model and its feasibility for
  automated analysis. The intruder and the communication channels are modelled
  as one entity that has complete control over all messages in the system. The
  intruder model is based on the concepts of memory and learning. Special care
  is taken that the model captures all possible actions of the intruder.
  Guidelines are given for finding the minimal number of model parts that
  represents a system with an arbitrary number of entities and concurrent
  protocol runs. Techniques of coping with state space explosion in
  reachability analysis, the stubborn set method and prioritizing of
  transitions, are discussed. Introduction of set type places or negative arcs
  in the net formalism is proposed as a solution for reducing the storage space
  requirements of the reachability graph. In experiments with the reachability
  analysis tool PROD, the model proved efficient in detecting protocol
  failures. Further optimization of the formalism and tools is necessary for
  the presented methods to be useful in full verification of real size
  protocols.
%X B14.ps.Z

%A Eero Lassila
%T ReFlEx --- an experimental tool for special-purpose processor code
  generation
%R Technical Report B15
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D March 1996
%K
%X
%X B15.ps.Z

%A Tommi Syrjänen
%T Implementation of local grounding for logic programs with stable model
  semantics
%R Technical Report B18
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D October 1998
%K logic programming, stable models, smodels, grounding
%X The aim of this work is to define a new class of logic programs, strongly
  range restricted logic programs, and to design and implement an efficient
  algorithm for grounding them locally. A grounding transforms a function-free
  logic program into an equivalent ground logic program. A grounding is local
  if can be done one rule at a time. The implementation works with smodels, an
  implementation for stable model semantics for normal logic programs which is
  developed at Helsinki University of Technology. The implementation is
  compared with old grounder of smodels and dlv, a knowledge representation
  system developed at Vienna University of Technology.
%X B18.ps.gz

%A Marko Mäkelä, Jani Lahtinen, and Leo Ojala
%T Performance analysis of a traffic control system using stochastic petri nets
%R Technical Report B19
%I Helsinki University of Technology, Digital Systems Laboratory
%C Espoo, Finland
%D December 1998
%K performance analysis, traffic control, {S}tochastic {P}etri {N}ets
%X This paper discusses the modelling and performance analysis of signalized
  traffic control systems using the Deterministic and Stochastic Petri Net
  (DSPN) formalism. We develop a formal DSPN model for a group of
  interconnected signalized traffic intersections and present performance
  indices obtained from simulation runs of example systems.
%X B19.ps.gz

