Model Checking Birth and Death

Dino Distefano, University of Twente, the Netherlands
http://wwwhome.cs.utwente.nl/~ddino/


Model checking birth and death


ABSTRACT
--------
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 operational
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 for LTL.
(This is a joint work with Arend Rensink and Joost-Pieter Katoen.)