Formal Methods Forum

Spring 1998

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

• 30.01.98 Tommi Junttila: On Symmetries and Bisimulation in State Space Analysis
• 06.02.98 Kari Nurmela: Laskennallinen menetelmä ympyräpeittojen hakemiseen

  Tiivistelmä: Diskreetissä geometriassa on tutkittu melko paljon ympyröiden (tai pallojen) pakkaamista erilaisiin alueisiin. Duaaliongelma - alueen peittäminen ympyröillä - on sen sijaan jäänyt vähemmälle tarkastelulle aina viime vuosiin saakka. Tutkimusryhmämme on onnistunut kehittämään peittojen hakemiseen uusia algoritmeja jotka ovat osoittautuneet selvästi tehokkaammiksi kuin aikaisemmat menetelmät. Näillä menetelmillä on haettu oletettavasti optimaalisia neliön ja kolmion peittoja 27 ja 30 ympyrään asti, kun julkaistut tulokset yltävät vain 11 ja 18 ympyrään.

• 13.02.98 Antti Huima: Formal Models of Cryptographic Protocols

  Abstract: Cryptographic protocols lie at the heart of the emerging information society. They form the link between strong cryptographic algorithms and security-critical applications in open networks - such as electronic cash or confidential information transactions. A subtle failure in a cryptographic protocol can lead to monumental economical and social losses. For this reason, there is high interest towards analysing the protocols formally, aiming at to prove that they are "secure". Unfortunately, cryptographic protocols are surprisingly hard to model. The presentation gives an overview of the area and describes some of the work being done relating to my [hopely] upcoming Master's Thesis and PhD.

• 27.02.98 Patric Östergård: Optimal Packings of Equal Circles in a Square

  Abstract: We consider the problem of finding the maximum radius of n non-overlapping equal circles in a unit square. An equivalent problem is that of spreading n points in a unit square so as to maximize the least distance between any two points. In the computer-aided proofs, the square is first divided into rectangles that are so small that they cannot contain two points (using a bound from a known packing of n points). Then all possible combinations of n rectangles that contain a point are considered (taking symmetries into account), and combinations that do not lead to an optimal packing are rejected using an elimination procedure. An elimination procedure is also utilized in the last step of the proof, where optimality is established. Optimal packings of up to 27 circles are obtained.

• 06.03.98 Nisse Husberg: Reachability Analysis: From Theory to Industrial Application

  Abstract: Reachability analysis theory is discussed from the point of view of industrial applications. The focus of theoretical research must be shifted from low level nets to high level nets and the efficiency of algorithms - both with respect to time and space. The integration of partial methods (testing) with the traditional complete reachability analysis will be needed. New methods avoiding unfolding are required and on-the-fly techniques are going to be important. In addition, front-ends and back-ends adapting the analyzers to existing environments will be discussed together with interfacing of different tools and the integration of design and verification tools.

• 13.03.98 Tuomas Aura: Modelling Mobile Code Security

  Abstract: Java applets and ActiveX components are pieces of code distributed over the Internet and executed automatically by the operating system or web browser at the client computer. The automatic downloading and execution of software creates obvious security concerns that have been addressed by defining clear rules for the authentication and sandbox execution of the code. The Java and ActiveX security models have, however, been designed for their specific applications and they are too restrictive for more complex systems with mobile objects. In this talk, I sketch a framework for modelling and verifying the integrity and confidentiality of mobile objects in a very general setting. The same framework can be used to describe and compare the security models of existing systems and to aid the design of new security architectures. The goal at this point is to device a highly visual engineering technique that can be easily formalized and augmented by automatic verification tools.

• 20.03.98 Kimmo Varpaaniemi: On the Stubborn Set Method in Reduced State Space Generation

  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.

  Keywords: reachability analysis, reduced state space generation, stubborn sets, verification of LTL formulas

• 27.03.98 Keijo Heljanko: Practical On-the-fly Model Checking for CTL* - A Variation on a Theme by Tarjan

  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* (Full Branching Time Logic). The process of checking whether the behavior of the system fulfills the specified property is called model checking. We have developed a new on-the-fly algorithm for model checking CTL*, which is currently under implementation. We will discuss temporal logic, and the use of automata in temporal logic model checking.

• 17.04.98 Patrik Simons: Extending Smodels and Whatnot

  Abstract: Ground logic programs containing rules of the form `a :- b, not c' can not compactly describe certain combinatorial problems such as choosing k elements out of n. More expressive rules are needed.

• 24.04.98 Eero Lassila: Lindenmayer Systems and Other Frameworks for Parallel Rewriting

  Abstract: Phrase structure grammars (such as context-free and context-sensitive grammars) and Lindenmayer systems, or L systems, are two major examples of formal rewriting frameworks. Phrase structure grammars and L systems are mainly used for language recognition and language generation tasks, respectively; the rewriting processes defined by these two frameworks are inherently serial and parallel, respectively. More specifically, the parallelism in L systems is strictly synchronous. Our thesis work includes the development of a generation-oriented rewriting scheme that possesses both context-sensitivity (it might be noted that L systems may be either context-free or context-sensitive) and asynchronous parallelism. Requiring tolerance for asynchrony helps us to ensure that the rewriting rules are highly modular, and declarative rather than procedural (in addition, the asynchrony should enable more efficient implementations). In their basic form, both phrase structure grammars and L systems (as well as conventional macro processors) are simple string manipulation frameworks whose essence is easily understood, even if their practical applications often involve higher-level abstractions; in contrast, our more complicated approach fully ignores the primitive string manipulation level in favor of conceptually higher processing levels with domain-specific abstractions.

• 08.05.98 Tomi Janhunen: On the Expressive Power of Non-Monotonic Logics

  Abstract: We concentrate on comparing the relative expressive power of five non-monotonic logics that have appeared in the literature. The results on the computational complexity of these logics suggest that these logics have very similar expressive power that exceeds that of classical monotonic logic. A refined classification of non-monotonic logics by their expressive power can be obtained using translation functions that satisfy certain properties such as faithfulness and modularity used by Gottlob. Basically, we adopt Gottlob's framework for our analysis, but propose a weaker notion of faithfulness. Consequently, a surprising result is deduced in light of Gottlob's results: Moore's autoepistemic logic is less expressive than Reiter's default logic and Marek and Truszczynski's strong autoepistemic logic. The expressive power of priority logic is also analyzed and shown to coincide with that of default logic. An exact classification of the expressive power of the non-monotonic logics under consideration is provided in the framework proposed.