@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} }