Formal Methods Forum

Autumn 2000

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

• 1.9.2000 Petteri Kaski: Enumeration of Balanced Ternary Designs

  Abstract: A (V, B; \rho_1, \rho_2, R; K, \Lambda) balanced ternary design is a pair (X, Y), where X is a set of cardinality V, and Y is a multiset of B multisets, or blocks, each consisting of K elements of X. Each element of X must appear exactly R times in the blocks of the design, \rho_1 times with multiplicity one, and \rho_2 times with multiplicity two. Additionally, every pair of distinct elements of X must appear exactly \Lambda times in the blocks of the design.

  Determining the number of nonisomorphic designs in a given class of designs and explicitly constructing these designs are central problems in design theory. The talk describes a backtrack search algorithm with isomorph rejection that was used to carry out a constructive enumeration for all but 12 of the 155 balanced ternary design classes in the range V<=10, B<=30, R<=15.

  (Joint work together with Patric Östergård).

• 15.9.2000 Timo Latvala: Model Checking Linear Temporal Logic Properties of Petri Nets with Fairness Constraints

  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 MARIA 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.

• 6.10.2000 Marko Mäkelä: Applying Compiler Techniques to Reachability Analysis of High-Level Models

  Abstract: Using a tool for high-level Petri nets as an example, we show how techniques familiar from compilers can make reachability analysers more powerful. Syntax transformations can be applied to extend the modelling language with convenient short-hand notations, such as universal and existential quantification and multi-set summation. The process of reachability analysis can be dramatically sped up by compiling models to executable machine code that performs all model-dependent tasks, such as computing the successors of a state. This work describes some principal ideas behind code generation and shows how generated code and static code can be linked together.

• 11.10.2000 Jussi Rintanen (Albert-Ludwigs-Universität Freiburg): Automated Reasoning with Quantified Boolean Formulae
  room TB357, at 3.00 p.m.

  Abstract: Quantified Boolean formulae (QBF) are an extension of the classical propositional logic with universal and existential quantification over truth-values. Interest in QBF stems from the fact that for bounded-length prefixes they represent computational problems that are complete for the levels of the polynomial hierarchy. The representation of many computational problems between NP and PSPACE is exponentially more concise in QBF than in the propositional logic. In this talk I discuss techniques for automating reasoning with quantified Boolean formulae. The main approach is to extend the Davis-Putman-Logemann-Loveland with universal quantification. We discuss this extension, additional inference rules made possible by universal variables, problems arising from the more concise representation, and preliminary solutions to these problems.

• 13.10.2000 Heikki Tauriainen: Automated Testing of Büchi Automata Translators for Linear Temporal Logic

  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üchi 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.

• 27.10.2000 Silja Mäki: Robust Membership Management for Ad-hoc Groups

  Abstract: In ad-hoc networks, the network nodes or users often form peer groups. A group may share an application, a physical location, or administrative tasks. Defining who is a member of the group is also the first step towards establishing a shared secret key for secure communication. Group membership management involves adding and removing nodes in the group, as well as a method for authenticating the group members. In this paper, we present a fully distributed, certificate-based system for group membership management. It is designed to suit highly dynamic ad-hoc networks where communications is sporadic and nodes often fail unexpectedly.

• 24.11.2000 Harri Haanpää: Sets in Z_n with Distinct Sums of Pairs

  Abstract: A subset S of an abelian group is a subset with distinct sums of pairs, if for all i,j,m,n in S with i != j, m != n, and {i,j} != {m,n}, it holds that i+j != m+n. Let v_gamma(k) denote the least n such that there exists a k-element subset of Z_n, the integers modulo n, with distinct sums of pairs (modulo n). An orderly algorithm for computing values of v_gamma(k) is presented, values of v_gamma for k <= 14 are given, and the connection to constant weight error-correcting codes is discussed.

• 1.12.2000 Harriet Beaver and Teemu Tynjälä: Modelling Feynman's Quantum Computer Using High-Level Petri Nets - A Computational Approach

  Abstract: Petri Nets have been succesfully used to model systems based on classical physics. The aim of our study is to model Feynman's quantum computer, one of the first quantum computers suggested, using High-Level Petri Nets. Feynman's quantum computer is based on a circuit of quantum logic gates in a similar way as classical computers are based on boolean gates and circuits. At the time of invention, Feynman could not give a time bound for the completion of his computer's computation; a periodical measuring procedure was needed. The periodical measurement allows us to use a computational approach. We model the use and operation of Feynman's computer using Predicate/Transition nets; the quantum mechanical background of the operation is also described using the same formalism. Naturally, in order to carry out the task of modelling quantum mechanical phenomena, we had to extend Predicate/Transition net formalism with complex numbers.

• 8.12.2000 Pierre-Olivier Ribet (LAAS, Toulouse): Some LAAS Tools related to Petri Nets

  Abstract: This presentation gives an overview about two tools, TINA and Move.net, which are related to Petri Nets and are currently under development at LAAS. TINA is a sofware for the analysis of untimed and timed Petri Nets. With respect to untimed systems, TINA allows the construction of the Karp & Miller's covering tree and the check of the general reachability properties (liveness, reversibility, absence of deadlock, strong connected components, ....). The step approach has been also implemented. With respect to timed systems, TINA allows the construction of the so-called state class graph - that is a graph where timed states are symbolically represented by a marking and a firing domain. Move.net is an automatic graph displayer, which was written in Java, and can display a mutable graph or Petri Net.

• 14.12.2000 Helger Lipmaa (Helsinki University of Technology, Telecommunications Software and Multimedia Laboratory): Efficient Algorithms for Differential Probability of Addition modulo 2^n and Related Problems

  Abstract: Differential attacks against the block cipher work with respect to XOR, or with respect to addition modulo $2^n$, for a fixed $n>1$. In the case where a block cipher uses both XOR and addition modulo $2^n$, it is important to know how these two operations relate to each other. We present efficient algorithms for calculating the differential properties of addition with respect to XOR. The first algorithm computes, for a given differential $\delta=(\DX,\DY\mapsto\DZ)$, the differential probability $\DPA{n}(\delta):= \mathbf{PR}_{x,y}[(x+y)\oplus((x\oplus\DX)+(y\oplus\DY))=\DZ]$ in the worst-case time $\Theta(\log n)$ and in the average-case time $\Theta(1)$. Next, we prove that the probability $\DPA{n}(\delta)\neq 0$, taken all differentials $\delta$, is $(1/2)\cdot (7/8)^{n-1}$, which shows that addition has many easily found impossible differentials. Additionally, we give formulas for other statistical properties of $\DPA{n}$. Finally, we show how to find the maximal differential probabilities of addition in the time $\Theta(\log n)$. The previously known algorithms for computing the probabilities above are na{\"\i}ve, requiring almost exhaustive computation.