Model Checking Birth and Death
University of Twente, Holland
In this talk we propose Allocational Temporal Logic (AllTL) as a formalism
to express properties concerning the dynamic allocation (birth) and
de-allocation (death) of entities, such as the objects in an object-based
system. The logic is interpreted on History-Dependent B"uchi Automata,
extended with a symbolic representation for certain cases of unbounded
allocation. We also present a simple imperative language with primitive
statements for (de)allocation, and provide it with a finite-state
semantics, to demonstrate the kind of behaviour that can be modelled.
The main result that we will present is a tableau-based model-checking
algorithm for AllTL, along the lines of Lichtenstein and Pnueli's algorithm
Place: Information technology, Uppsala University
Time: 13.15-14.00 (+ discussions)
Room 1113 is in building 1, floor 1, room 13
(in the southern part of the building).
Help on how to find ASTEC Seminars.
There will be an extended period for discussions after the seminar.
Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 14.00.
Everyone is welcome !
Updated 29-May-2002 08:48 by Roland Grönroos
e-mail: info -at- astec.uu.se