Formal Methods Forum

Autumn 2001

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

• 17.8.2001 Prof. Moshe Y. Vardi (Rice University): The Design of a Formal Property-Specification Language
  Note: The talk is held at 3.00 p.m. in hall T2.

  Abstract: In recent years, the need for formal specification languages is growing rapidly as the functional validation environment in semiconductor design is changing to include more and more validation engines based on formal verification technologies. In particular, the usage of Formal Equivalence Verification and Formal Property Verification is growing, new symbolic simulation engines are introduced and hybrid environments of scalar and symbolic simulators are developed. To facilitate the use of these new-generation validation engines - properties, checkers and reference models need to be developed in a formal language.

  In this talk we describe the design of the ForSpec Temporal Logic (FTL), the new temporal logic of ForSpec, Intel's new formal property-specification language. The key features of FTL are: it is a linear temporal logic, based on Pnueli's LTL, it enables the user to define temporal connectives over time windows, it enables the user to define regular events, which are regular sequences of Boolean events, and then relate such events via special connectives, and it contains constructs that enable the user to model multiple clock and reset signals, which is useful in the verification of globally asynchronous and locally synchronous hardware designs.

  The focus of the talk is on design rationale, rather than a detailed language description.

• 22.8.2001 Prof. Mirek Truszczynski (Department of Computer Science, University of Kentucky): Fixed-Parameter Complexity of Semantics for Logic Programs
  Note: The talk is held at 10.15 a.m. in hall T2.

  Abstract: A decision problem is called parameterized if its input is a pair of strings. One of these strings is referred to as a parameter. The problem: given a propositional logic program P and a non-negative integer k, decide whether P has a stable model of size no more than k, is an example of a parameterized decision problem with k serving as a parameter. Parameterized problems that are NP-complete often become solvable in polynomial time if the parameter is fixed. The problem to decide whether a program P has a stable model of size no more than k, where k is fixed and not a part of input, can be solved in time O(mn^k), where m is the size of P and n is the number of atoms in P. Thus, this problem is in the class P. However, algorithms with the running time given by a polynomial of order k are not satisfactory even for relatively small values of k.

  The key question then is whether significantly better algorithms (with the degree of the polynomial not dependent on k) exist. To tackle it, we use the framework of fixed-parameter complexity. We establish the fixed-parameter complexity for several parameterized decision problems involving models, supported models and stable models of logic programs. We also establish the fixed-parameter complexity for variants of these problems resulting from restricting attention to Horn programs and to purely negative programs. Most of the problems considered in the paper have high fixed-parameter complexity. Thus, it is unlikely that fixing bounds on models (supported models, stable models) will lead to fast algorithms to decide the existence of such models.

  (Joint work with Zbigniew Lonc.)

• 21.9.2001 Petteri Kaski: Kombinatoristen sommitelmien tuottaminen hakualgoritmien avulla

  Tiivistelmä: Kombinatorinen (v,k,\lambda)-lohkosommitelma (engl. block design) on diskreetti rakenne, jonka avulla voidaan toteuttaa esimerkiksi seuraavanlainen koejärjestely: Halutaan vertailla v kahvilaatua keskenään käyttäen koemaistajia. Jotta kaikkien koemaistajien mielipiteiden painoarvo olisi yhtä suuri, saa jokainen koemaistaja arvioitavakseen täsmälleen k kahvilaatua. Lisäksi mitä tahansa kahta kahvilaatua arvioi täsmälleen \lambda koemaistajaa, jotta kahvilaatujen keskinäinen vertailu olisi tehty samalla tarkkuudella. Esimerkiksi tapauksessa v = 7, k = 3, \lambda = 1 koejärjestely voidaan toteuttaa käyttäen seitsemää koemaistajaa, joista kukin saa arvioitavakseen yhden seuraavista kahvilaatukokoelmista:

  123 145 167 246 257 347 356 Kiinnostavan alaluokan (v,k,\lambda)-lohkosommitelmille muodostavat osituksiin jakautuvat (engl. resolvable) sommitelmat, joiden osituksiin jakoja (engl. resolution) voidaan käyttää mm. erilaisten peliturnauksien suunnitteluun. Lohkosommitelmien teoriassa on useita avoimia ongelmia, joihin on mahdollista löytää ratkaisu tietokonehaun avulla. Diplomityössäni tutkitaan hakualgoritmeja, joita voidaan käyttää (v,k,\lambda)-lohkosommitelmien ja näiden osituksiin jakojen luokitteluun isomorfiaa vaille. Työn päätuloksena ratkaistaan eräs avoin ongelma osoittamalla täydellisen haun avulla, että osituksiin jakautuvaa (15,5,4)-lohkosommitelmaa ei ole olemassa.

• 12.10.2001 Prof. Pekka Orponen: The Computational Power of Continuous-Time Neural Networks

  Abstract: We prove that any function computed by a discrete-time network of n threshold gates ("perceptrons") can also be computed by a continuous-time system of 18n+7 symmetrically-coupled "saturated-linear" analog neurons. The result appears at first sight counterintuitive, because the dynamics of any system of the latter type is constrained by a Liapunov, or "energy" function defined on its state space. In particular, such a system always converges from any initial state towards some stable equilibrium state, and hence cannot exhibit nondamping oscillations, i.e. strictly speaking cannot simulate even a single alternating bit. However, we show that if one only considers terminating computations, then the Liapunov constraint can be overcome, and one can in fact embed arbitrarily complicated computations in the dynamics of Liapunov systems with only a modest cost in the system's dimensionality. In terms of standard discrete computation models, our result implies that any polynomially space-bounded Turing machine can be simulated by a polynomial-size family of continuous-time symmetric neural networks.

  (Joint work with Jiri Sima, Czech Academy of Science.)

• 9.11.2001 Dr. Kimmo Varpaaniemi: Minimizing the Number of Successor States in the Stubborn Set Method

  Abstract: Combinatorial explosion which occurs in parallel compositions of LTSs can be alleviated by letting the stubborn set method construct on-the-fly a reduced LTS that is CFFD- or CSP-equivalent to the actual parallel composition. This paper considers the problem of minimizing the number of [[immediate]] successor states of a given state in the reduced LTS. The problem can be solved by constructing an and/or-graph with weighted vertices and by finding a set of vertices that satisfies a certain constraint such that no set of vertices satisfying the constraint has a smaller sum of weights. Without weights, the and/or-graph can be constructed in low-degree polynomial time w.r.t.\ the ``length of the input of the problem''. However, since actions can be nondeterministic and transitions can share target states, it is not known whether the weights are generally computable in polynomial time. [[Computing such a weight basically means computing the number of successor states of a state in the parallel composition of a subcollection of the LTSs. The parallel composition operation being considered is much like in the ARA tool which was developed by VTT in the beginning of the 90's.]] Consequently, it is an open problem whether minimizing the number of successor states is as ``easy'' as minimizing the number of successor transitions.

• 16.11.2001 Markku-Juhani Saarinen (Nokia Corporation): LILI Exposed

  Abstract: LILI-128 is a fast stream cipher proposed by Simpson, Dawson, Golic and Millan (ISRC/QUT, Australia) in 2000. LILI-128 is based on irregularly clocked linear feedback shift registers and a nonlinear mixing function. LILI-128 strikes a cryptanalyst as a very traditional stream cipher design, resembling the A5 cipher of GSM handsets and the E0 cipher of Bluetooth in many respects. The designers of LILI have used theory that has its roots in the work of Berkelekamp and Massey (late 1960's) and was widely discussed in the open cryptographic literature in 1980's. Based on this research, Simpson et al. have showed that LILI-128 exhibits many desirable statistical and security properties. Despite its conservative design, we have discovered a major "loophole" in the clocking subsystem of LILI-128. In this talk we show how this loophole can be exploited in an attack that breaks LILI-128 with significantly less effort than expected by its authors.

• 30.11..2001 Olli-Matti Penttinen: Modeling Continuous and Hybrid Systems with Stochastic Petri Nets

  Abstract: A novel method is given for representing systems of ordinary differential equations as a generalized stochastic Petri net (GSPN). The stochastic marking process of this net is studied. It is viewed as a multi-dimensional increment-decrement process (definition given) that has the property that its time-dependent state distribution has an expectation that exactly coincides with the solution of the differential equation system (proof given). Thus, it is shown how to model exactly a set of continuous deterministic phenomena with a discrete Petri net in continuous time. A simple example (multi-phase radioactive decay) is treated in detail.

  The material has been submitted to ICATPN 2002.

• 5.12.2001 Dr. Tuomas Aura (Microsoft Research): Mobile IP Security
  Note: The talk is held on Wed at 15.15 p.m. in room TB353.

  Abstract: Mobile IPv6 is a mobility protocol for the IPv6 Internet. The mobile node has a fixed IP address and the protocol allows it to always communicate using this address. In the basic protocol, a home agent forwards packets from this address to wherever the mobile currently is. The mobile may also notify its correspondents about its current address, so that they can send data directly there. It does this by send a binding update (BU) message to the correspondent. Unfortunately, malicious parties can send false BU messages and, thus, redirect data to a wrong destination. This talk will overview attacks that exploit false BU messages, and related defense mechanisms. Several of the attacks were recently discovered at Microsoft Research Cambridge and we are actively working in the IETF to develop a more secure protocol.