[kisoron-ml] JAIST Logic Seminar Series

[Hajime Ishihara]

皆様

ジェノヴァ大学のEugenio Moggi先生の特別集中講演のお知らせです。
どうぞふるってご参加ください。

問合せ先：
石原　哉
北陸先端科学技術大学院大学 情報科学系
e-mail: ishihara at jaist.ac.jp
-----------------------------------------------

* JAIST Logic Seminar Series *

* This series of lectures is held as a part of JSPS Core-to-Core Program,
A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES 
project CORCON.
(http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/)

Dates: Tuesday 2 August, 2016, 13:30-15:10
          Thursday 4 August, 2016, 13:30-15:10
          Friday 5 August, 2016, 10:50-12:30

Place: JAIST, Collaboration room 7 (I-56)
(Access: http://www.jaist.ac.jp/english/location/access.html)

Speaker: Eugenio Moggi (University of Genova)

*Tuesday 2 August, 2016, 13:30-15:10*

LECTURE 1: Categories of Classes for Collection Types

ABSTRACT. Collection types have been proposed by Buneman and others (in 
the '90) as a way to
capture database query languages in a typed setting. In 1998 Manes 
introduced the notion of collection
monad on the category S of sets as a suitable semantics for collection 
types. The canonical example of
collection monad is the finite powerset monad Pf.
In order to account for the algorithmic aspects of database languages, 
the category S is unsuitable, and
should be replaced with other categories, whose arrows are maps 
computable by "low complexity"
algorithms. We propose "realizability for DSL" (Domain Specific 
Languages), where the starting point
is a monoid C of endomaps on a set D, instead of a combinatory algebra 
on D, as a way to get such
categories by constructions like the category A[C] of "assemblies".
To get Pf in a systematic way we borrow ideas from AST (Algebraic Set 
Theory, started by Joyal and
Moerdijk in the '90), where they fix a notion of "small" map in a 
category of "classes", and read "small"
as "finite".

*Thursday 4 August, 2016, 13:30-15:10*

LECTURE 2: Hybrid System Trajectories as Partial Continuous Maps

ABSTRACT. Hybrid systems (HS) are dynamic systems that exhibit both 
continuous and discrete
dynamic behavior: they can flow (according to a differential equation) 
and jump (according to a
transition relation). HS can be used for modeling rigid body dynamics 
with impacts, and more
generally Cyber-Physical Systems.
HS can exhibit Zeno behaviors, that arise naturally in rigid body 
dynamics with impacts, but are absent
from purely discrete or purely continuous systems. Dealing properly with 
these behaviors is a
prerequisite to give sound definitions of concepts such as reachability.
We propose the use of partial continuous maps (PCM) as trajectories that 
describe how a HS evolves
over time. PCMs enable a notion of trajectory that can go beyond Zeno 
points.

*Friday 5 August, 2016, 10:50-12:30*

LECTURE 3: Models, Over-approximations and Robustness

ABSTRACT. Hybrid systems, and related formalisms, have been successfully 
used to model Cyber-
Physical Systems. The usual definition of "reachability", in terms of 
the reflexive and transitive closure
of a transition relation, is unsound for Zeno systems. We propose "safe 
reachability", which gives an
over-approximation of the set of states that are "reachable in finite 
time" from a set of initial states.
Moreover, mathematical models are always a simplification of the system 
they are meant to describe,
and one must be aware of this mismatch, when using these models for 
system analyses.
In safety analysis it is acceptable to use over-approximations of the 
system behavior, indeed they are
the bread and butter of counterexample guided abstraction refinement 
(CEGAR).
We propose a notion of safe (time-bounded) reachability, which is also 
robust wrt arbitrary small overapproximations,
and argue that it is particularly appropriate for safety analysis.