Formal Methods Forum

Spring 2002

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.2.2002 Toni Jussila: Bounded Model Checking for Verifying Concurrent Programs

  Abstract: A simple, parallel programming language is introduced and an operational semantics for it is developed. The language combines the syntax of C and Java together with the communication primitives taken from PROMELA. A verification method for specifications given in the language is developed for detecting the violation of temporal reachability and safety properties. The method is known as Bounded Model Checking (BMC) where the idea is to reduce the model checking problem to propositional satisfiability. A compact boolean encoding of parallel programs is devised, together with the proofs of its soundness and completeness. Encoding of the reachability and safety properties is developed and finally semantical models for strengthening the encoding are discussed.

• 15.2.2002 Keijo Heljanko: Bounded Reachability Checking with Process Semantics

  Abstract: Bounded model checking has been recently introduced as an efficient verification method for reactive systems. In this work we apply bounded model checking to asynchronous systems. More specifically, we translate the bounded reachability problem for 1-safe Petri nets into constrained Boolean circuit satisfiability. We consider three semantics: process, step, and interleaving semantics. We show that process semantics has often the best performance for bounded reachability checking.

• 1.3.2002 Petteri Kaski: The Steiner triple systems of order 19

  Abstract: A Steiner triple system of order v, briefly STS(v), is a set of 3-element subsets, called blocks, of a v-set of points, such that every unordered pair of points occurs in exactly one block. An STS(v) exists if and only if either v = 1 (mod 6) or v = 3 (mod 6). For example, the blocks of an STS(7) are 123 145 167 246 257 347 356. Up to isomorphism, that is, relabeling of the points in the blocks, this STS(7) is unique. Similarly, the STS(9) is unique. There are two nonisomorphic STS(13), and 80 nonisomorphic STS(15). Until recently, these were all the nontrivial values of v for which the exact number of nonisomorphic STS(v) was known. In this talk we describe the computer-aided classification approach that we used to settle the case v = 19. Namely, after a search that required approximately two years total CPU time, we were able to completely classify the 11,084,874,829 nonisomorphic STS(19).

  (Joint work with Patric Östergård)

• 13.3.2002 Prof. Gerd Brewka (University of Leipzig): Logic Programs with Ordered Disjunction

  Abstract: In a recent paper (Brewka, Benferhat, Le Berre, KR-2002) Qualitative Choice Logic (QCL), a propositional logic with a new connective called ordered disjunction, was introduced. Ordered disjunction, intuitively, allows context dependent preferences among different options to be expressed. A x B stands for: if possible A, otherwise B. The paper shows that QCL has interesting applications, for instance in design and configuration. In this talk we show how ordered disjunction can be added to extended logic programs under answer set semantics. We consider logic programs with orderd disjunction in the heads of rules (LPODs). Answer sets can satisfy such rules to certain degrees. The degrees in turn are used to define a preference relation on answer sets. LPODs allow us to represent defeasible knowledge together with context dependent preferences among intended properties of problem solutions. Under certain assumptions reasoning from most preferred answer sets provides the best possible solutions for a problem. LPODs can also be used as the basis of a qualitative decision theory if the literals representing possible choices of the agent are distinguished and a decision making strategy based on the preference ordering among answer sets is fixed.

• 15.3.2002 Prof. Alessandro Provetti (Universita' di Milano-Universita` di Messina): Consistency Monitors in Condition-Event-Action Systems: Preliminary Thoughts

  Abstract: At the highest level of abststraction, management of communication networks can be described by event-condition-action rules (with slight modifications). This is the approach used by Chomicki, Lobo et al. in their work on PDL. A consistency monitor is a set of constraints that are applied in order to avoid executing a set of actions that are hazardous or physically impossible. When a set of actions to be executed violates the monitor, remedial steps have to be taken, e.g., cancelling some action so as to "go down" to a consistent set. Yet, one would like to maximize the number of actions actually served. Writing consistency monitors is a knowledge representation task. Applying consitency monitors, exp. in the real-time scenario of network management, is a complex (potentially intractable) task. This talk speculates on how complex consistency monitors can get, and reconsiders the application of ASP solvers such as smodels and DLV to consistency mainteinance.

• 9.4.2002 Prof. Paul Vitanyi (CWI & Universiteit van Amsterdam): Time and Space Bounds on Reversible Computing

  Abstract: We give an introduction to reversible computing theory, and prove a new general upper bound on the tradeoff between time and space that suffices for the reversible simulation of irreversible computation. Previously, only simulations using exponential time or quadratic space were known. The tradeoff shows for the first time that we can simultaneously achieve subexponential time and subquadratic space. The boundary values are the exponential time with hardly any extra space required by the Lange-McKenzie-Tapp method and the (log 3)th power time with square space required by the Bennett method. We also give the first general lower bound on the extra storage space required by general reversible simulation. This lower bound is optimal in that it is achieved by some reversible simulations.

  See Journal of Physics A: Mathematical and General, 34(2001), 6821-6830 or http://arXiv.org/abs/quant-ph/0101133 . The talk is based on joint work with Ming Li, John Tromp, Harry Buhrman.

• 12.4.2002 Alan Franzi and Fabrizio Magni (Universita degli Studi di Milano): An Efficient Way to Calculate Stable Models for Kernel Programs

  Abstract: Needing a new approach to the computation of stable models for kernel programs we are modifying the SMODELS algorithms in order to achieve better performances and studying the behavior of the resolution flow-chart. The results show an improvement under the condition of the presence of stable models even if the efficiency is guaranteed in every circumstance. Benchmarks are being implemented using SAT semantic and random generating procedures. Main test of the efficiency of the new algorithms will be the ASP world.

  Unfortunately, each team who develop one specific ASP implementation creates respective benchmark. As a result we found a lot of programs that works with different, and sometimes incomparable, type of logic programs. We can also know that generic random programs offer an unlimited number of test cases generated by changing some parameters of the data. Thus these programs are flexible but have often proprieties that rarely occur in real (and useful) logic program. In our work we are designing (an developing also) one program (BASP) with all in one feature. We will able to test simultaneously with one logic problem all ASP implementation. We are trying to split the program into two different parts, data information and problem description to obtain one benchmark suite as flexible as possible. We will briefly show the results and the current stage of our work.

• 19.4.2002 Prof. Javier Esparza (University of Edinburgh, Lab. for Foundations of Computer Science): Model checking pushdown processes

  Abstract: Pushdown processes are pushdown automata seen under a different light: we are not interested in the languages they recognise, but in the transitions systems they generate. These are infinite transition systems with pairs of the form (control state, stack content) as states. In the first part of the talk we study the problem of checking if all the infinite executions of a pushdown process satisfy a formula of Linear Temporal Logic (LTL), and derive efficient algorithms. In the second part, we show how a variety of problems in different areas (dataflow analysis, security models, verification) can be solved applying these algorithms.

  This is joint work with Stefan Schwoon

• 23.4.2002 Prof. Phillip Rogaway (University of California at Davis): A Block-Cipher Mode of Operation for Parallelizable Message Authentication

  Abstract: We define and analyze a simple and fully parallelizable block-cipher mode of operation for message authentication. Parallelizability does not come at the expense of serial efficiency: in a conventional, serial environment, the algorithm's speed is within a few percent of the (inherently sequential) CBC MAC. The new mode, PMAC, is deterministic, resembles a standard mode of operation (and not a Carter-Wegman MAC), works for strings of any bit length, employs a single block-cipher key, and uses just $\max\{1,\lceil |M|/n\rceil\}$ block-cipher calls to MAC a string $M\in{0,1}^*$ using an $n$-bit block cipher. We prove PMAC secure, quantifying an adversary's forgery probability in terms of the quality of the block cipher as a pseudorandom permutation.

• 24.4.2002 Dr. Charles Lakos (University of Adelaide, Computer Science Department): Towards the Analysis of Object-Oriented Petri Nets
  Note: The talk is at 13:15 in room TB353

  Abstract: This talk will introduce the notion of Object-Oriented Petri Nets and the motivation for having such a formalism. This variety of Petri Nets has been around for some years, but progress in analysing such nets has been slow. The talk will discuss the aspects which need to be addressed in order to analyse such nets, namely symmetry analysis and modular analysis. The talk will also present the work that has been done with one particular dialect of Object-Oriented Petri Nets. This will cover the translation of these nets into a folded version suitable for analysis with the Maria tool. It will also cover the results achieved via incremental analysis, as reported in the PhD thesis of Glenn Lewis.

• 17.5.2002 Dr. Manfred Jaeger (Max-Planck-Institut für Informatik, Saarbrücken): Probabilistic Relational Models: Meaning, Representation & Inference

  Abstract: Probabilistic Models are increasingly used in many areas of computer science. Classical models like Markov chains or random graphs are often insufficient for complex probabilistic dependencies in richly structured domains. In this talk I will present the semantically defined class of probabilistic relational models, which provides useful models in areas like artificial intelligence, reliability analysis or bioinformatics. For the formal representation of probabilistic relational models I introduce the language of relational Bayesian networks, and show how certain inference problems can be solved on the basis of this representation.

• 21.5.2002 Prof. V.A. Nepomniaschy (Institute of Informatics Systems Russian Academy of Sciences, Siberian Division, Novosibirsk, Russia): Basic-REAL: Integrated Approach for Design, Specification and Verification of Distributed Systems

  Abstract: Abstract: We suggest a three layers integrated approach for design, specification and verification of distributed system. The approach is based on especially designed high-level specification language Basic-REAL (bREAL) and comprises (I) a translation of a high-level design of distributed systems to executional specifications of bREAL, (II) a presentation of a high-level properties of distributed systems as logical specifications of bREAL, (III) problem-oriented compositional deductive reasoning coupled with model checking.

• 31.5.2002
  Dr. Leila Kallel (Paris): Genetic Algorithms : convergence bounds from simple functions to long paths

  Abstract: A landscape can be seen as a collection of basins of attraction. Along this idea, we propose a methodology for identifying the distribution of the sizes of basins of attraction and their number. This methodology is based on statistical tests applied to sampled data from a landscape. It can be used to compare different neighbouring relations (or mutation operators). We finally present an overview of some convergence times on known landscapes, showing that monotone functions can also be difficult to optimise.

  Dr. Dirk Arnold (University of Dortmund): Theoretical aspects of evolutionary optimization in continuous search spaces

  Abstract: Evolutionary algorithms are general, nature-inspired heuristics for search and optimization. With their emphasis on populations and on (self-)adaptation, they differ from many conventional optimization strategies. Supported both by empirical evidence and by theoretical findings, there is a widespread belief that evolutionary algorithms are robust and reliable, and frequently they are the method of choice if neither derivatives of the objective function are at hand nor differentiability or numerical accuracy can be assumed. Theoretical analyses of evolution strategies in continuous search spaces frequently focus on the behavior on simple fitness landscapes. On such landscapes, results can be obtained that describe how the performance of the strategies scales with both parameters of the problem and of the strategies considered. Such scaling laws offer insights useful for the understanding of the robustness that is observed. Based on those findings, recommendations with respect to the sizing of the parameters and to the choice of strategy variants can be made.