|
Formal Methods Forum
Spring 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
- 4.2.2000 Keijo Heljanko:
Complexity of Model Checking with Finite Complete Prefixes
Abstract:
McMillan has presented a verification method for finite-state Petri nets
based on finite complete prefixes of net unfoldings. We discuss the
computational complexity of some model checking questions when a finite
complete prefix is used as a symbolic representation of the state space
of a net system.
Previously deadlock and reachability checking have been shown to be
NP-complete in the size of the finite complete prefix. We show that
there are prefixes for which model checking temporal formulas containing
nested temporal modalities is PSPACE-complete in the size of the prefix.
We also discuss the relevance of the result to the design of practical
prefix-based verification algorithms.
- 11.2.2000 Tommi Syrjänen:
A Rule-Based Formal Model for Software Configuration
Abstract:
A rule-based approach for software configuration is
presented. The configuration knowledge is stored in two distinct
models: a configuration model that encodes rules to form valid
configurations and a diagnostic model that can be used to find errors
in user requirements. As a case study, a subset of the configuration
problem of the Debian GNU/Linux system is formalized.
- 18.2.2000 Tommi Junttila:
Detecting and Exploiting Data Type Symmetries of Algebraic System Nets
During Reachability Analysis
Abstract:
The symmetry reduction method is a technique designed
to alleviate the combinatorial explosion problem
occurring in state-space based verification.
We present a way how state space symmetries of a high-level
Petri net formalism, algebraic system nets,
can be detected and exploited during the state-space analysis.
The main idea is that permuting the domains of data types used in nets
produces corresponding permutations to the state space level.
As the main result a sufficient condition is defined for data type domain
permutations ensuring that the produced state space permutations are
actually automorphisms i.e. symmetries.
Since verification of the condition is shown to be a co-NP-complete
problem,
an approximation rule for the condition is also given.
Use of the developed theory is illustrated by defining
the class of extended well-formed nets and
by examining data type symmetries of such nets.
- 25.2.2000 Prof. Pierre Azema (LAAS-CNRS, Toulouse, France):
Protocol Specification and Debugging by Message Sequences.
Abstract:
The framework of this talk is the protocol design by means of high
level Petri nets. The basic idea is to study a protocol behavior by
taking into account operational input/output sequences, such as
message sequence charts (MSC). These sequences are used for debugging
purpose.
A prototyping environment is introduced. This environment is based
upon communicating agents, whose behavior is depicted by Petri
nets. Furthermore, the agent number and their interactions may change
on line.
A distributed channel allocation algorithm for mobile computing is
used as illustrative example.
- 10.3.2000 Nisse Husberg:
A Uniform Approach to Petri Nets and Transition Systems
Abstract:
In addition to several different approaches to formalisms for
concurrent systems the development of many different Petri net classes
has created a situation where it is difficult to understand and apply
concepts defined for one specific class. There is, however, work going
on to create a uniform approach using abstract formalisms. Typically
the net structure and the data parts are separated and parameterised
in these approaches. This talk is mainly about the uniform approach
developed in Berlin (Padberg and Ehrig) and the distributed transition
systems defined by the author. Both approaches use category theory and
abstract data types to model both high-level and low-level nets.
Some examples from the net description language of the Maria analyser are
also presented.
- 24.3.2000 Tuomas Aura:
Denial-of-Service Resistant Authentication
Abstract:
Denial of service by server resource exhaustion has become a primary
security threat in open communications networks. Public-key
authentication does not completely protect against the attacks because
the authentication protocols often leave ways for an unauthenticated
client to consume a server's memory space and computational resources
by beginning a large number of protocol runs and leaving them in some
middle state. We show how stateless authentication protocols and the
client puzzles of Juels and Brainard can be used to prevent such
attacks.
The talk is based on a joint work with Pekka Nikander and
Jussipekka Leiwo.
- 2.5.2000 Prof. Mirek Truszczynski (Univ. of Kentucky):
Answer Set Programming and DATALOG with Constraints
Abstract:
Answer-set programming (ASP) has emerged recently as a viable
programming paradigm well attuned to search problems in AI,
constraint satisfaction, combinatorial optimization and combinatorics.
In the talk we give a brief overview of the roots of ASP and comment
on its potential. The bulk of the talk is devoted to a discussion of
a recently introduced ASP system - DATALOG with constraints (DC, in
short). Informally, $\datac$ theories consist of propositional clauses
(constraints) and of Horn rules. The semantics is a simple and
natural extension of the semantics of the propositional logic.
We describe the syntax and semantics of DC, and study its properties.
We discuss an implementation of DC and present results of experimental
study of the effectiveness of DC, comparing it with the csat
satisfiability checker and smodels2.
(joint work with Deborah East)
- 5.5.2000 Patric Östergård:
Isomorph-Free Generation of Combinatorial Objects
Abstract:
In the study of combinatorial objects, one is
often facing the problems of counting the number of
nonisomorphic (or nonequivalent, depending on
the terminology used) objects with given parameters or
of constructing these. We shall look at some fundamental
methods for such isomorph-free construction of various
types of objects; in particular, so-called orderly
generation of t-designs is considered. For example,
a recent computation shows that there are 242,995,846
2-(12,3,2) designs. Classification of various other objects,
for example, Petri nets, will also be discussed.
- 19.5.2000 Kari Nurmela:
Peittävien taulukoiden (covering arrays) muodostamisesta
Abstract:
Peittävät taulukot ovat tietyntyyppisiä kombinatorisia sommitelmia, joita
voidaan käyttää mm. järjestelmien testauksessa. Tavoitteena on muodostaa
mahdollisimman pieni sellainen testitapauksien joukko, johon jokainen
parametrien arvopari (tai t-monikko) sisältyy ainakin kerran. Jos kukin
parametri voi saada vain kaksi eri arvoa ja t=2, optimaaliset taulukot
tunnetaan. Muissa tapauksissa tunnetaan vain ylä- ja alarajoja
optimaalisten taulukoiden koolle.
Tässä esitelmässä näytetään, miten tabuhakua voidaan käyttää peittävien
taulukoiden etsimiseen ja esitetään joitakin uusia peittävien taulukoiden
konstruktioita. Myös joitain uusia alarajoja on saavutettu täydellisellä
haulla; yksi uusi peittävä taulukko tiedetään nyt optimaaliseksi.
- 26.5.2000 Tommi A. Junttila:
Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking
Abstract:
Boolean circuits offer a natural, structured, and compact
representation of Boolean functions for many application domains. In
this talk a tableau method for solving satisfiability problems for
Boolean circuits is devised. The method employs a direct cut rule
combined with deterministic deduction rules. Simplification rules for
circuits and a search heuristic attempting to minimize the search space
are developed. Experiments in symbolic model checking domain indicate
that the method is competitive against state-of-the-art satisfiability
checking techniques and a promising basis for further work.
- 9.6.2000 Harri Haanpää:
Alarajoja Ramseyn luvuille
Abstract:
Miten tahansa m solmun täydellisen graafin kaaret väritetäänkin kahdella
värillä, jos m vain on riittävän suuri, värityksestä löytyy aina k solmun
täydellinen graafi, jonka kaikki kaaret ovat samanvärisiä. Pienimpiä
riittävän suuria m:n arvoja kutsutaan Ramseyn luvuiksi.
Ramseyn lukujen määrittäminen on varsin vaikeaa. Tässä esitelmässä
esitellään menetelmiä, joilla on todistettu alarajoja Ramseyn luvuille.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 09 January 2005.
|