Formal Methods Forum

Spring 1999

This is a seminar on formal methods in computer science and engineering organized by the Laboratory for Theoretical Computer Science at HUT. We meet usually on Fridays at 2 p.m. in room B353 in the Computer Science building.

For further information, please contact Ilkka Niemelä.

Program

• 8.1.99 Tuomas Aura: Distributed Access Control with Certificates

  Abstract: A central goal in computer security is access control: giving access to services and data only to those who have sufficient access rights. In distributed, open systems with no globally trusted authorities or globally enforced policies, authenticated messages are the only widely available technique for access right management. Other mechanisms such as reference monitors, trusted computing base (TCB), and immediate revocation of rights can be implemented in closed high-security environments but not on open networks like the Internet. A certificate is an authenticated message about the rights or attributes of some entity. It must be issued by someone with sufficient authority so that those reading it will trust its contents. In this presentation, we explain how certificates can express local trust relationships and policies, and how a global access control system is formed by local authorities delegating rights to each other. We also describe work in progress on a new, generalized way of controlling redelegation of access rights.

• 29.1.99 Dr. Karsten Schmidt (Humboldt-Universität zu Berlin): Low Level Symmetries
  Time: 10.15
  Room: Y427A (Main building)

  Abstract: Low level symmetries are faster than many people think. But it is necessary to use the right techniques. The low level symmetry approach provides techniques to find the symmetries and techniques for integrating the symmetries into, say reachability, analysis. For both problems, solutions are presented and compared.

• 29.1.99 Dr. Karsten Schmidt (Humboldt-Universität zu Berlin): Stubborn Sets for Preserving States
  Time: 14.15
  Room: T3 (Computer Science building)

  Abstract: Most stubborn set approaches (beyond the basic method that preserves the dead states) preserve certain paths of a system. In this lecture, the potential of stubborn sets to preserve different kinds of states is discussed. This view to stubborn sets can be applied to the analysis of several Petri net standard properties as well as to model checking for a small branching time logic (the EF/AG fragment of CTL).

• 5.2.99 Ismo Kangas (Nokia Research Center): Reliable Data Transmission between Mobile Station and Packet-switched Digital GSM Mobile Network

  Abstract: Digital mobile phones have recently established their position in personal communications. At the same time the Internet has become very common, and is nowadays a general-purpose source for all sorts of information and services. It is already possible to use mobile phones for connecting to the Internet, but the method is very expensive and the connection slow. At the present time a standardization work is underway, which will define the new packet-switched GPRS-system (General Packet Radio Service) in conjunction with the global digital GSM-network. GPRS will provide faster, more efficient and economical interface to general packet data networks, especially to the Internet. The main topic of this thesis is the reliable data transmission between mobile station and GPRS-network. The telecommunication protocols used for data transmission are presented, and their importance for the reliability is discussed. In addition to this, other important issues that have to do with reliability are also discussed. The use of GPRS as a method for connecting to the Internet is examined especially from the point of view of reliability. In this thesis one specific telecommunication protocol between the mobile station and the GPRS-network is studied in detail. The protocol studied is the Logical Link Control (LLC). An implementation of the LLC is also presented. The tools used for the implementation are introduced, and the experiences obtained are enounced. The specification of the LLC-protocol is evaluated briefly.

• 12.2.99 Matti Nykänen (University of Helsinki): Kohdistuslogiikka ja sen kyselyjen turvallisuus

  Tiivistelmä: Tietokantojen uudet sovellusalueet tuovat usein mukanaan myös tarpeen käsitellä uudenlaisia tietotyyppejä. Esimerkiksi bioinformatiikan - biologisen informaation käsittelyn - eräs keskeinen osa-alue on hallita perimäaineksesta eristettyjä DNA-sekvenssejä. Nämä sekvenssit voidaan puolestaan esittää merkkijonoina. Tällaista merkkijonotietoa sisältävän tietokannan kyselykielen täytyy näin ollen pystyä käsittelemään jonoja ei vain perinteisinä jakamattomina tietoalkioina vaan myös merkki merkiltä. Tämä käsittely on luontevaa määritellä loogisin operaatioin modernien kyselykielten tapaan. Esityksessä kuvataan ensin "kohdistuslogiikka" (Alignment Calculus), Helsingin yliopiston tietojenkäsittelytieteen laitoksella kehitetty temporaalilogiikkaan perustuva merkkijonokyselykieli. Sitten tarkastellaan sen toteutukseen liittyvää ns. "turvallisuusongelmaa" (safety problem): voidaanko annetun kohdistuslogiikan kaavan ilmaisemaan kyselyyn vastata äärellisin laskentaresurssein? Tähän tietokantateorian vanhaan ongelmaan tuo uusia piirteitä kielen mahdollisuus luoda uusia jonoja, joita ei löydy itse tietokannasta: esimerkiksi kysely "anna kaikki jonot jotka esiintyvät jonkin tietokannassa olevan jonon alkuosana" luo uusia jonoja turvallisesti, kun taas kysely "anna kaikki jonot joiden alkuosa esiintyy tietokannassa" luo niitä turvattomasti. Loogisesti kyse on samasta merkkijonojen relaatiosta "jono 1 on jonon 2 alkuosa"; edellinen kysely pyysi tuottamaan kullekin tietokannan jonolle 2 kaikki vastaavat jonot 1, jälkimmäinen taas päinvastoin. Algoritmiseksi ongelmaksi tulee siten tunnistaa mihin suuntiin käyttäjän kirjoittamaa loogista merkkijonorelaation kuvausta saa käyttää ja mihin taas ei.

• 19.2.99 Keijo Heljanko: Deadlock Checking Using Prefixes and Smodels

  Abstract: McMillan has presented a deadlock detection method for Petri nets based on finite complete prefixes (i.e. net unfoldings). The approach transforms the PSPACE-complete deadlock detection problem for a 1-safe Petri net into a potentially exponentially larger NP-complete problem of deadlock detection for a finite complete prefix. McMillan devised a branch-and-bound algorithm for deadlock detection in prefixes. Recently, Melzer and Römer have presented another approach, which is based on solving mixed integer programming problems. In this work it is shown that instead of using mixed integer programming, a constraint-based logic programming framework can be employed, and a linear-size translation from deadlock detection in prefixes into the problem of finding a stable model of a logic program is presented. Experimental results are given from an implementation combining the prefix generator of the PEP-tool, the translation, and an implementation of a constraint-based logic programming framework, the smodels system. The experiments show the proposed approach to be quite competitive, when compared to the approaches of McMillan and Melzer/Römer.

• 12.3.99 Patrik Simons: Implementing the Stable Model Semantics

  Abstract: An efficient implementation of the stable model semantics is only possible through a careful choice of data structures and algorithms. Implementation choices are highlighted and extensions to the basic algorithm are discussed.

• 19.3.99 Antti Huima: Efficient Infinite-State Analysis of Cryptographic Protocols

  Abstract: Nowadays the most common method for analyzing cryptographic protocols seems to be state space enumeration. Most of the current methods analyze a finite state space. This means that only a part of a security protocol's state space is examined, because such a state space is almost always infinite. The infiniteness stems from the intruder's ability to send an unlimited number of distinct messages. Some of the methods are able to analyze infinite state space, but they require user interaction, partially because they try solve a too generic problem that is undecidable.

  In my Master's Thesis I develop a new method for analyzing cryptographic protocols. It is able to completely enumerate an infinite state space as long as the number of participants taking part in a protocol is bounded and the executions of single participants are of finite length. As far as I know, this is a new result and a considerable enchancement.

  The method is based on symbolic state space enumeration. The method includes step transitions, a symmetry method, a method for detecting symbolic state subsumption relations, and on-the-fly verification of the security properties in conjunction with their dynamic simplification as the analysis progresses. There is a higher-level procedural language that can be used to describe security protocols.

  My talk is an overview of this Thesis work.

• 26.3.99 Harri Haanpää: Ramseyn luvuista

  Abstract: Ramseyn luvut määritellään seuraavasti. Olkoon G_1, ..., G_m joukko graafeja. Ramseyn luku R(G_1, ..., G_m) on pienin kokonaisluku n, jolla ei ole mahdollista värittää täydellisen graafin K_n kaaria m värillä ilman, että tähän väritykseen sisältyy G_i värillä i jollakin i:n arvolla. Esitelmässä esitetään pari tunnettua Ramseyn lukua ja käsitellään menetelmiä alarajojen etsimiseksi Ramseyn luvuille.

• 9.4.99 Patric Östergård: A Fast Algorithm for the Maximum Clique Problem

  Abstract: We present an exact branch-and-bound algorithm for the maximum clique problem - which is computationally equivalent to the maximum independent set problem - with a new, effective pruning strategy. Comparisons carried out with previously published algorithms show a performance that is clearly better for random graphs, and considerably better for some special graphs.

  The algorithm works particularly well in the search for binary error-correcting codes when the words of a Hamming space are listed in lexicographic order (these words are the vertices of the graph, and two vertices are adjacent exactly when they are at Hamming distance greater than or equal to d - which is fixed - apart). The algorithm played a central role when we recently proved that the maximum sizes of binary one-error-correcting codes of length 10 and 11 are 72 and 144, respectively.

  We finally show how the algorithm can be generalized to find maximum-weight cliques in weighted graphs.

• 16.4.99 Tommi Syrjänen: Using Local Grounding with Smodels

  Abstract: The smodels system is an efficient implementation of the stable model semantics for variable-free logic programs. In this presentation a front-end, lparse, for smodels is introduced. The lparse takes as its input a logic program which has variables and produces the corresponding ground logic program. The lparse works with strongly range restricted logic programs. In strongly range restricted programs the predicates are divided to two sets, domain and non-domain predicates. The domain predicates are used determine the ranges of the variables occuring in the rules. This makes it possible to ground rules locally one at a time without having to store the whole program in memory at the same time. The lparse supports and extends the new rule types of the smodels version 2, namely constraint, weight, and choice rules. Other features include:

  • Basic arithmetic functions using integers.
  • Symbolic constants that get their values at runtime.
  • Local domains for literals in new rules.
  • Notational shortcuts (ranges, multiple argument lists, etc.)
  • Support for user defined functions.

• 23.4.99 Alfred Wassermann (Universität Bayreuth): Computer construction of t-designs

  Abstract: In the last few years there has been much progress in the computer construction of t-designs with small parameters. t-designs are combinatorial objects which are strongly related with coverings, packings and codes. The most successful approach to construct these objects is to prescribe a symmetry group and solve the resulting diophantine linear system.

• 7.5.99 Kari Nurmela: Tabuhaku diskreeteissä peitto- ja pakkausongelmissa

  Abstract: Monet paljon tutkitut matemaattiset ongelmat voidaan esittää diskreetteinä peitto- tai pakkausongelmina. Esimerkkejä näistä ovat erilaisten sommitelmien ja koodien muodostamiset, graafien värityksien ja klikkien hakeminen sekä eräät lukuteorian ongelmat. Joissain tapauksissa, kun täydellinen haku ei onnistu, tällaisiin ongelmiin voidaan etsiä menestyksekkäästi ratkaisuja paikalliseen hakuun perustuvilla heuristisilla algoritmeilla, esim. tabuhaulla. Esitelmässä annetaan esimerkkejä ongelmista, jotka voidaan muuntaa diskreeteiksi peitto- tai pakkausongelmiksi ja kuvaillaan työn alla olevaa ohjelmistoa paikallisen haun käyttämiseen ratkaisujen etsinnässä.

• 28.5.99 Marko Mäkelä: A Reachability Analyzer for Many-Sorted Petri Nets

  Abstract: Theoretical Computer Science Laboratory has long tradition in developing reachability analyzers. Our flagship Prod is getting old, and much work has been invested in developing a new analyzer that should have more expressive power and be easier to use, both for humans and for compiler writers who wish to write model generators for other formalisms.

  In this presentation I will shortly describe the net description language, the abstract data type system and the expression syntax. I will show some details of the expression evaluator and the quantification process. Last but not least, I will describe how the reachability graph is stored and how the space consumption can be reduced further.

• 4.6.99 Timo Soininen (TAI Research Centre): Product Configuration: Concepts, Problems and a Logic Program Based Approach

  Abstract: Configurable products have become an important way of satisfying widely varying customer requirements. Such products are specified for each order as a combination of predefined components. This approach aims at providing a competitive trade-off between the flexibility of one-of-a-kind products in satisfying different requirements and the cost effectiveness of standard, mass-produced products. However, efficient configuration, i.e. specification of the product for a customer, requires information system support when the set of predefined components and their dependencies is large or complex enough that it cannot be effectively carried out by humans. This support is offered by knowledge based systems called product configurators. Commercial product configurators have, despite their theoretical limitations, in the past five years become a major success, one of the few practical successes of artificial intelligence technology.

  In this presentation the main concepts and computational problems in the product configuration domain are first discussed. We briefly outline the typical configuration related processes and tasks from the industrial perspective and introduce at an abstract level the notions of configuration model, configuration, customer requirements and product configuration problem. We then go on to briefly describe an approach to representing configuration models, configurations and requirements and solving configuration problems. The approach is based on extending normal logic programs and their stable model semantics with constructs useful in the configuration domain. It differs from most of the other approaches to configuration in that it directly captures the intuition that a configuration should not contain anything superfluous, i.e. that every component needs to have a justification for being included in a configuration.