皆様
ジェノヴァ大学のEugenio Moggi先生の特別集中講演のお知らせです。
どうぞふるってご参加ください。
問合せ先：
石原 哉
北陸先端科学技術大学院大学 情報科学系
e-mail: ishihara(a)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.
皆様
オークランド大学のBakhadyr Khoussainov先生の講演のお知らせです。
どうぞふるってご参加ください。
問合せ先：
石原 哉
北陸先端科学技術大学院大学 情報科学系
e-mail: ishihara(a)jaist.ac.jp
-----------------------------------------------
* JAIST Logic Seminar Series *
Date: Monday 20 June, 2016, 15:20-17:00
Place:JAIST, Collaboration room 7 (I-56)
(Access: http://www.jaist.ac.jp/english/location/access.html)
Speaker: Bakhadyr Khoussainov (University of Auckland)
Title: Computably Enumerable Structures: Domain dependency
Abstract:
Computably enumerable structures arise naturally in algebra
and computer science. In algebra examples include finitely
presented universal algebras such as finitely presented groups.
In computer science, these are abstract data types
defined by equational or quasi-equational specifications.
The domains of these algebraic structures are quotient sets
of the form $\omega/E$, where $\omega$ is the set of
natural numbers and $E$ is a computably enumerable (c.e.)
equivalence relations. We consider c.e. structures whose
domains are of the form $\omega/E$ and study various properties
of these structures and their dependence on the domain $\omega/E$
