|
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.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 09 January 2005.
|