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.)