Models for interactive systems based on space-time  duality;
Agapia programming language
-----------------------------------
          
ABSTRACT
-----------------------------------
We present a model, a core programming language, specification
andanalysis techniques appropriate for modeling, programming
andreasoning about interactive computing systems.The model consists
of "rv-systems" ("interactive systems withregisters and voices");
it includes register machines, is space-timeinvariant, is compositional,
may describe computations extending inboth time and space, and
is applicable to open, interactivesystems. To achieve modularity
in space the model uses "voices" (avoice is the time dual of
a register) - they provide a high levelorganization of temporal
data and are used to describe interactioninterfaces of processes.The
programming language uses novel techniques for syntax andsemantics
to support computation in space paradigm.  We describe"rv-programs"
and base their syntax and operational semantics on FISs("finite
interactive systems") and their grid languages (a FIS is akind
of 2-dimensional automaton specifying both control andinteraction
used in rv-programs).A structured programming version and a kernel
language AGAPIA v0.1 aredescribed, as well.  The operational
semantics for structuredrv-programs is described in terms of
running scenarios. We present atranslation from structured rv-programs
to rv-programs and a proof ofthe correctness of the translation.Finally,
we present a framework for developing a Floyd-Hoareverification
logic for (structured) rv-programs.As a case study, we include
a detailed analysis of a terminationdetection protocol for a
pool of distributed processes, logicallyorganized into a ring.
We develop an implementation for the coreactivity of the processes
and for their interactions using structuredrv-programs. Then,
we present a formal proof of the correctness of theprotocol using
the Hoare-like logic for structured rv-programs.
          
SPEAKER(S)
-----------------------------------
Prof.dr. Gheorghe STEFANESCU
Universitatea din Bucuresti, Facultatea de Matematica si Informatica
Bucuresti
Romania
-----------------------------------
Professor Gheorghe Stefanescu received his BSc (Honors & Diploma
of Merit), MSc, and PhD from the University of Bucharest in 1979,
1980, and 1991, respectively. He was a Junior Research Fellow/Senior
Research Fellow at Institute of Mathematics of the Romanian Academy
(IMAR) from 1980 to 1995 and Associate Professor/Professor of
Computer Science at University of Bucharest from 1995 to present.He
has held Visiting Professor positions at Kyushu University in
1997, Graduate School for Logic in Computer Science, Munich in
1998, and National University of Singapore in 2001/2002. He was
often visiting scholar at Technical University Munich from 1994
to present and at University of Amsterdam / CWI / Utrecht University
from 1990 to 1996. He was Chief of Computer Science Section of
IMAR from 1990 to 1992 and Director of Centre of Logic and Informatics,
Bucharest from its beginning (December, 2000).Professor Stefanescu's
main current research interests are in network algebra and concurrent,
object-oriented systems (models, theory, verification, mobility,
programming languages).In 1986 he discovered an algebraic structure
called "biflow" (later renamed as BNA, "Basic Network Algebra").
After their introduction in the context of control flowcharts
setting, the BNA axioms were rediscovered in various fields ranging
from circuit theory to action calculi, from data-flow networks
to knot theory (traced monoidal categories), from process graphs
to functional programming. An extended presentation is included
in his recent "Network Algebra" book, Springer-Verlag, 2000.
In the last years he discovered "finite interactive systems",
a two-dimensional extension of finite automata, well-suited for
modeling concurrent, object-oriented systems. He is the author
of more than 80 research papers published in journals, conference
proceedings, or as technical reports.He has served on the program
committee of certain international conferences, including ICALP
or IFIP/TCS conferences and as external evaluator for many well-know
international journals and conferences. He is guest editor for
two special issues of "Electronic Notes in Theoretical Computer
Science" (Elsevier) and "Journal of Universal Computer Science"
(Springer). He is member of the European Association for Theoretical
Computer Science, American Mathematical Society, and European
Association for Computer Science Logic.
-----------------------------------