Forecast :
Philadelphia, Pa
__________________________________________________
Max Kanovich
(
maxkanov@math.upenn.edu )
From
http://www.cis.upenn.edu/~lc/seminar.html:
What logic is good for CS ?
or
"The Drinking Philosophers"
in the mirror of Horn linear logic
Max Kanovitch
University of Pennsylvania
Monday, May 1, 2000, 4:30 PM
University of Pennsylvania, Moore 554
The aim of this research is
to develop adequate and comprehensive logical systems
capable of handling important properties of real-time systems,
The basic step in understanding a given timed system S is to
show that its `reachability' predicate:
``There exists a trajectory that leads to a given state s'',
is partial recursive.
After that, for any reasonably expressive logical system L,
one could immediately conclude that
the above `reachability problem' is equivalent to the problem
whether the corresponding sequent is provable in L or not.
The real challenge is to establish that
a proposed logical system L is `fully adequate':
that there is a direct correspondence
between trajectories in S and proofs in L.
We will consider real-time systems with quantitative time constraints,
within which all things may be changed during the course of actions
and events: the number of actors, the ``communication topology'',
even the numerical bounds in the time constraints.
A number of obstructions to a fully adequate logical analysis
are figured out:
-
A global continuous time implies an over-complicated set
of trajectories.
- Potentially unbounded number of actors
and dynamically configured topology of actors push us out
beyond the finite automaton paradigm.
- Global quantitative time constraints push us out beyond
the Markov processes property (that is,
the Present determines the Future);
whereas the proofs are always ``Markovian''.
- Besides, a common user is used to describe actions and events
in his own terms by means of a Horn-like format: if ... then ... .
The aim of the talk is to show that the Horn fragment of linear
logic provides us with a fully adequate logical formalism
for the real-time systems under consideration.
The ``non-Markovian'' problem is circumvented by introducing hidden
variables recorded by ``time-guards''.
For the underlying trajectories with time-guards we introduce
an exact bisimulation equivalence
(together with a high-school proof of its correctness,
based on the combination:
a coarse hour-glass + a precise one-hand watch).
Slides pdf.file ps.file
Teaching 
Spring'00 : Math 141
Fall'99 : Math 360 and Math 361
Click at here to get more